Small changes.

Cubical/Displayed/Base.agda

@@ -40,12 +40,12 @@ record UARel (A : Type ℓA) (ℓ≅A : Level) : Type (ℓ-max ℓA (ℓ-suc ℓ
 open BinaryRelation
 
 -- another constructor for UARel using contractibility of relational singletons
-make-𝒮 : {A : Type ℓA} {ℓ≅A : Level} {_≅_ : A → A → Type ℓ≅A}
+make-𝒮 : {A : Type ℓA} {_≅_ : A → A → Type ℓ≅A}
           (ρ : isRefl _≅_) (contrTotal : contrRelSingl _≅_) → UARel A ℓ≅A
 UARel._≅_ (make-𝒮 {_≅_ = _≅_} _ _) = _≅_
 UARel.ua (make-𝒮 {_≅_ = _≅_} ρ c) = contrRelSingl→isUnivalent _≅_ ρ c
 
-record DUARel {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A)
+record DUARel {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
               (B : A → Type ℓB) (ℓ≅B : Level) : Type (ℓ-max (ℓ-max ℓA ℓB) (ℓ-max ℓ≅A (ℓ-suc ℓ≅B))) where
   no-eta-equality
   constructor duarel
@@ -70,7 +70,7 @@ record DUARel {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A)
 
 -- total UARel induced by a DUARel
 
-module _ {A : Type ℓA} {ℓ≅A : Level} {𝒮-A : UARel A ℓ≅A}
+module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
   {B : A → Type ℓB} {ℓ≅B : Level}
   (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
   where

Cubical/Displayed/Function.agda

@@ -110,34 +110,6 @@ module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
 -- SubstRel on a dependent function type
 -- from a SubstRel on the domain and SubstRel on the codomain
 
-equivΠ' : ∀ {ℓA ℓA' ℓB ℓB'} {A : Type ℓA} {A' : Type ℓA'}
-  {B : A → Type ℓB} {B' : A' → Type ℓB'}
-  (eA : A ≃ A')
-  (eB : {a : A} {a' : A'} → eA .fst a ≡ a' → B a ≃ B' a')
-  → ((a : A) → B a) ≃ ((a' : A') → B' a')
-equivΠ' {B' = B'} eA eB = isoToEquiv isom
-  where
-  open Iso
-
-  isom : Iso _ _
-  isom .fun f a' =
-    eB (secEq eA a') .fst (f (invEq eA a'))
-  isom .inv f' a =
-    invEq (eB refl) (f' (eA .fst a))
-  isom .rightInv f' =
-    funExt λ a' →
-    J (λ a'' p → eB p .fst (invEq (eB refl) (f' (p i0))) ≡ f' a'')
-      (secEq (eB refl) (f' (eA .fst (invEq eA a'))))
-      (secEq eA a')
-  isom .leftInv f =
-    funExt λ a →
-    subst
-      (λ p → invEq (eB refl) (eB p .fst (f (invEq eA (eA .fst a)))) ≡ f a)
-      (sym (commPathIsEq (eA .snd) a))
-      (J (λ a'' p → invEq (eB refl) (eB (cong (eA .fst) p) .fst (f (invEq eA (eA .fst a)))) ≡ f a'')
-        (retEq (eB refl) (f (invEq eA (eA .fst a))))
-        (retEq eA a))
-
 module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
   {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
   {C : Σ A B → Type ℓC} (𝒮ˢ-C : SubstRel (∫ˢ 𝒮ˢ-B) C)

Cubical/Displayed/Properties.agda

@@ -21,7 +21,7 @@ private
 
 -- induction principles
 
-module _ {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A) where
+module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) where
   open UARel 𝒮-A
   𝒮-J : {a : A}
         (P : (a' : A) → (p : a ≡ a') → Type ℓ)
@@ -44,7 +44,7 @@ module _ {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A) where
     = subst (λ r → P a' r) (Iso.leftInv (uaIso a a') p) g
     where
       g : P a' (≡→≅ (≅→≡ p))
-      g = J (λ y q → P y (≡→≅ q)) d (≅→≡ p)
+      g = 𝒮-J (λ y q → P y (≡→≅ q)) d p
 
 
 -- constructors
@@ -81,11 +81,9 @@ module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
     -- constructor that reduces univalence further to contractibility of relational singletons
 
     𝒮ᴰ-make-2 : (ρᴰ : {a : A} → isRefl _≅ᴰ⟨ ρ a ⟩_)
-                (contrTotal : (a : A) → contrRelSingl _≅ᴰ⟨ UARel.ρ 𝒮-A a ⟩_)
+                (contrTotal : (a : A) → contrRelSingl _≅ᴰ⟨ ρ a ⟩_)
                 → DUARel 𝒮-A B ℓ≅B
-    DUARel._≅ᴰ⟨_⟩_ (𝒮ᴰ-make-2 ρᴰ contrTotal) = _≅ᴰ⟨_⟩_
-    DUARel.uaᴰ (𝒮ᴰ-make-2 ρᴰ contrTotal)
-      = 𝒮ᴰ-make-aux (contrRelSingl→isUnivalent _ ρᴰ (contrTotal _))
+    𝒮ᴰ-make-2 ρᴰ contrTotal = 𝒮ᴰ-make-1 (contrRelSingl→isUnivalent _ ρᴰ (contrTotal _))
 
 -- relational isomorphisms
 

Cubical/Displayed/Subst.agda

@@ -54,7 +54,7 @@ DUARel.uaᴰ (Subst→DUA {𝒮-A = 𝒮-A} {B = B} 𝒮ˢ-B) b p b' =
     ≃⟨ invEquiv (compPathlEquiv (sym (SubstRel.uaˢ 𝒮ˢ-B p b))) ⟩
   subst B (≅→≡ p) b ≡ b'
     ≃⟨ invEquiv (PathP≃Path (λ i → B (≅→≡ p i)) b b') ⟩
-  PathP (λ i → B (UARel.≅→≡ 𝒮-A p i)) b b'
+  PathP (λ i → B (≅→≡ p i)) b b'
   ■
   where
   open UARel 𝒮-A

Cubical/Foundations/Equiv.agda

@@ -230,35 +230,42 @@ equiv→Iso h k .Iso.leftInv f = funExt λ a → retEq k _ ∙ cong f (retEq h a
 equiv→ : (A ≃ B) → (C ≃ D) → (A → C) ≃ (B → D)
 equiv→ h k = isoToEquiv (equiv→Iso h k)
 
-equivΠ : ∀ {ℓA ℓA' ℓB ℓB'} {A : Type ℓA} {A' : Type ℓA'}
+
+equivΠ' : ∀ {ℓA ℓA' ℓB ℓB'} {A : Type ℓA} {A' : Type ℓA'}
   {B : A → Type ℓB} {B' : A' → Type ℓB'}
   (eA : A ≃ A')
-  (eB : (a : A) → B a ≃ B' (eA .fst a))
+  (eB : {a : A} {a' : A'} → eA .fst a ≡ a' → B a ≃ B' a')
   → ((a : A) → B a) ≃ ((a' : A') → B' a')
-equivΠ {B' = B'} eA eB = isoToEquiv isom
+equivΠ' {B' = B'} eA eB = isoToEquiv isom
   where
   open Iso
 
   isom : Iso _ _
   isom .fun f a' =
-    subst B' (secEq eA a') (eB _ .fst (f (invEq eA a')))
+    eB (secEq eA a') .fst (f (invEq eA a'))
   isom .inv f' a =
-    invEq (eB _) (f' (eA .fst a))
+    invEq (eB refl) (f' (eA .fst a))
   isom .rightInv f' =
     funExt λ a' →
-    cong (subst B' (secEq eA a')) (secEq (eB _) _)
-    ∙ fromPathP (cong f' (secEq eA a'))
+    J (λ a'' p → eB p .fst (invEq (eB refl) (f' (p i0))) ≡ f' a'')
+      (secEq (eB refl) (f' (eA .fst (invEq eA a'))))
+      (secEq eA a')
   isom .leftInv f =
     funExt λ a →
-    invEq (eB a) (subst B' (secEq eA _) (eB _ .fst (f (invEq eA (eA .fst a)))))
-      ≡⟨ cong (λ t → invEq (eB a) (subst B' t (eB _ .fst (f (invEq eA (eA .fst a))))))
-           (commPathIsEq (snd eA) a) ⟩
-    invEq (eB a) (subst B' (cong (eA .fst) (retEq eA a)) (eB _ .fst (f (invEq eA (eA .fst a)))))
-      ≡⟨ cong (invEq (eB a)) (fromPathP (λ i → eB _ .fst (f (retEq eA a i)))) ⟩
-    invEq (eB a) (eB a .fst (f a))
-      ≡⟨ retEq (eB _) (f a) ⟩
-    f a
-    ∎
+    subst
+      (λ p → invEq (eB refl) (eB p .fst (f (invEq eA (eA .fst a)))) ≡ f a)
+      (sym (commPathIsEq (eA .snd) a))
+      (J (λ a'' p → invEq (eB refl) (eB (cong (eA .fst) p) .fst (f (invEq eA (eA .fst a)))) ≡ f a'')
+        (retEq (eB refl) (f (invEq eA (eA .fst a))))
+        (retEq eA a))
+
+equivΠ : ∀ {ℓA ℓA' ℓB ℓB'} {A : Type ℓA} {A' : Type ℓA'}
+  {B : A → Type ℓB} {B' : A' → Type ℓB'}
+  (eA : A ≃ A')
+  (eB : (a : A) → B a ≃ B' (eA .fst a))
+  → ((a : A) → B a) ≃ ((a' : A') → B' a')
+equivΠ {B = B} {B' = B'} eA eB = equivΠ' eA (λ {a = a} p → J (λ a' p → B a ≃ B' a') (eB a) p)
+
 
 equivCompIso : (A ≃ B) → (C ≃ D) → Iso (A ≃ C) (B ≃ D)
 equivCompIso h k .Iso.fun f = compEquiv (compEquiv (invEquiv h) f) k

Cubical/Foundations/HLevels.agda

@@ -593,11 +593,11 @@ isOfHLevel→isOfHLevelDep 0 h {a} =
   (h a .fst , λ b' p → isProp→PathP (λ i → isContr→isProp (h (p i))) (h a .fst) b')
 isOfHLevel→isOfHLevelDep 1 h = λ b0 b1 p → isProp→PathP (λ i → h (p i)) b0 b1
 isOfHLevel→isOfHLevelDep (suc (suc n)) {A = A} {B} h {a0} {a1} b0 b1 =
-  isOfHLevel→isOfHLevelDep (suc n) (λ p → helper a1 p b1)
+  isOfHLevel→isOfHLevelDep (suc n) (λ p → helper p)
   where
-  helper : (a1 : A) (p : a0 ≡ a1) (b1 : B a1) →
+  helper : (p : a0 ≡ a1) →
     isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1)
-  helper a1 p b1 = J (λ a1 p → ∀ b1 → isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1))
+  helper p = J (λ a1 p → ∀ b1 → isOfHLevel (suc n) (PathP (λ i → B (p i)) b0 b1))
                      (λ _ → h _ _ _) p b1
 
 isContrDep→isPropDep : isOfHLevelDep 0 B → isOfHLevelDep 1 B

Cubical/Foundations/Prelude.agda

@@ -457,7 +457,7 @@ isPropIsContr (c0 , h0) (c1 , h1) j .snd y i =
          c0
 
 isContr→isProp : isContr A → isProp A
-isContr→isProp (x , p) a b = sym (p a) ∙∙ refl ∙∙ p b
+isContr→isProp (x , p) a b = sym (p a) ∙ p b
 
 isProp→isSet : isProp A → isSet A
 isProp→isSet h a b p q j i =

Cubical/Relation/Binary/Base.agda

@@ -99,7 +99,7 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
       Iso.rightInv i = J (λ y p → cong fst (h aρa (y , J Q (ρ a) p)) ≡ p)
                          (J (λ q _ → cong fst (h aρa (a , q)) ≡ refl)
                            (J (λ α _ → cong fst α ≡ refl) refl
-                             (isContr→isProp (isProp→isContrPath h aρa aρa) refl (h aρa aρa)))
+                             (isProp→isSet h _ _ refl (h _ _)))
                            (sym (JRefl Q (ρ a))))
       Iso.leftInv i r = J (λ w β → J Q (ρ a) (cong fst β) ≡ snd w)
                           (JRefl Q (ρ a)) (h aρa (a' , r))