Some more helpful functions. (#730)

agda · Mar 10, 2022 · 17c2725 · 17c2725
1 parent e93eec9
commit 17c2725
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 2 deletions.
diff --git a/Cubical/Foundations/HLevels.agda b/Cubical/Foundations/HLevels.agda
@@ -454,6 +454,9 @@ isProp→ pB = isPropΠ λ _ → pB
 isSetΠ : ((x : A) → isSet (B x)) → isSet ((x : A) → B x)
 isSetΠ = isOfHLevelΠ 2
 
+isSetImplicitΠ : (h : (x : A) → isSet (B x)) → isSet ({x : A} → B x)
+isSetImplicitΠ h f g F G i j {x} = h x (f {x}) (g {x}) (λ i → F i {x}) (λ i → G i {x}) i j
+
 isSetΠ2 : (h : (x : A) (y : B x) → isSet (C x y))
         → isSet ((x : A) (y : B x) → C x y)
 isSetΠ2 h = isSetΠ λ x → isSetΠ λ y → h x y

diff --git a/Cubical/HITs/SetQuotients/Properties.agda b/Cubical/HITs/SetQuotients/Properties.agda
@@ -35,8 +35,8 @@ open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂ ; ∣_∣
 private
   variable
     ℓ ℓ' ℓ'' : Level
-    A B C : Type ℓ
-    R S T : A → A → Type ℓ
+    A B C Q : Type ℓ
+    R S T W : A → A → Type ℓ
 
 elimProp : {P : A / R → Type ℓ}
   → (∀ x → isProp (P x))
@@ -67,6 +67,14 @@ elimProp3 prop f =
   elimProp (λ x → isPropΠ2 (prop x)) λ a →
   elimProp2 (prop [ a ]) (f a)
 
+elimProp4 : {P : A / R → B / S → C / T → Q / W → Type ℓ}
+  → (∀ x y z t → isProp (P x y z t))
+  → (∀ a b c d → P [ a ] [ b ] [ c ] [ d ])
+  → ∀ x y z t → P x y z t
+elimProp4 prop f =
+  elimProp (λ x → isPropΠ3 (prop x)) λ a →
+  elimProp3 (prop [ a ]) (f a)
+
 -- sometimes more convenient:
 elimContr : {P : A / R → Type ℓ}
   → (∀ a → isContr (P [ a ]))