fix: knock-ons

src/Data/Product/Function/Dependent/Propositional.agda

@@ -194,17 +194,21 @@ module _ where
     to′ = map (to I↠J) (to A↠B)
 
     backcast : ∀ {i} → B i → B (to I↠J (section I↠J i))
-    backcast = ≡.subst B (≡.sym (to∘to⁻ I↠J _))
+    backcast = ≡.subst B (≡.sym (section-strictInverseˡ I↠J _))
 
-    to⁻′ : Σ J B → Σ I A
-    to⁻′ = map (section I↠J) (Surjection.section A↠B ∘ backcast)
+    section′ : Σ J B → Σ I A
+    section′ = map (section I↠J) (section A↠B ∘ backcast)
 
     strictlySurjective′ : StrictlySurjective _≡_ to′
-    strictlySurjective′ (x , y) = to⁻′ (x , y) , Σ-≡,≡→≡
-      ( to∘to⁻ I↠J x
-      , (≡.subst B (to∘to⁻ I↠J x) (to A↠B (section A↠B (backcast y))) ≡⟨ ≡.cong (≡.subst B _) (to∘to⁻ A↠B _) ⟩
-         ≡.subst B (to∘to⁻ I↠J x) (backcast y)                      ≡⟨ ≡.subst-subst-sym (to∘to⁻ I↠J x) ⟩
-         y                                                          ∎)
+    strictlySurjective′ (x , y) = section′ (x , y) , Σ-≡,≡→≡
+      ( section-strictInverseˡ I↠J x
+      , (begin
+           ≡.subst B (section-strictInverseˡ I↠J x) (to A↠B (section A↠B (backcast y)))
+             ≡⟨ ≡.cong (≡.subst B _) (section-strictInverseˡ A↠B _) ⟩
+           ≡.subst B (section-strictInverseˡ I↠J x) (backcast y)
+             ≡⟨ ≡.subst-subst-sym (section-strictInverseˡ I↠J x) ⟩
+           y
+             ∎)
       ) where open ≡.≡-Reasoning
 
 
@@ -250,7 +254,7 @@ module _ where
   Σ-↔ {I = I} {J = J} {A = A} {B = B} I↔J A↔B = mk↔ₛ′
     (Surjection.to surjection′)
     (Surjection.section surjection′)
-    (Surjection.to∘to⁻ surjection′)
+    (Surjection.section-strictInverseˡ surjection′)
     left-inverse-of
     where
     open ≡.≡-Reasoning

src/Data/Product/Function/Dependent/Setoid.agda

@@ -94,34 +94,37 @@ module _ where
     (function (⇔⇒⟶ I⇔J) A⟶B)
     (function (⇔⇒⟵ I⇔J) B⟶A)
 
-  equivalence-↪ :
-    (I↪J : I ↪ J) →
-    (∀ {i} → Equivalence (A atₛ (RightInverse.from I↪J i)) (B atₛ i)) →
-    Equivalence (I ×ₛ A) (J ×ₛ B)
-  equivalence-↪ {A = A} {B = B} I↪J A⇔B =
-    equivalence (RightInverse.equivalence I↪J) A→B (fromFunction A⇔B)
-    where
-    A→B : ∀ {i} → Func (A atₛ i) (B atₛ (RightInverse.to I↪J i))
-    A→B = record
-      { to   = to      A⇔B ∘ cast      A (RightInverse.strictlyInverseʳ I↪J _)
-      ; cong = to-cong A⇔B ∘ cast-cong A (RightInverse.strictlyInverseʳ I↪J _)
-      }
-
-  equivalence-↠ :
-    (I↠J : I ↠ J) →
-    (∀ {x} → Equivalence (A atₛ x) (B atₛ (Surjection.to I↠J x))) →
-    Equivalence (I ×ₛ A) (J ×ₛ B)
-  equivalence-↠ {A = A} {B = B} I↠J A⇔B =
-    equivalence (↠⇒⇔ I↠J) B-to B-from
-    where
-    B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x))
-    B-to = toFunction A⇔B
+  module _ (I↪J : I ↪ J) where
+
+    private module ItoJ = RightInverse I↪J
+
+    equivalence-↪ : (∀ {i} → Equivalence (A atₛ (ItoJ.from i)) (B atₛ i)) →
+                    Equivalence (I ×ₛ A) (J ×ₛ B)
+    equivalence-↪ {A = A} {B = B} A⇔B =
+      equivalence ItoJ.equivalence A→B (fromFunction A⇔B)
+      where
+      A→B : ∀ {i} → Func (A atₛ i) (B atₛ (ItoJ.to i))
+      A→B = record
+        { to   = to      A⇔B ∘ cast      A (ItoJ.strictlyInverseʳ _)
+        ; cong = to-cong A⇔B ∘ cast-cong A (ItoJ.strictlyInverseʳ _)
+        }
+
+  module _ (I↠J : I ↠ J) where
+
+    private module ItoJ = Surjection I↠J
+
+    equivalence-↠ : (∀ {x} → Equivalence (A atₛ x) (B atₛ (ItoJ.to x))) →
+                    Equivalence (I ×ₛ A) (J ×ₛ B)
+    equivalence-↠ {A = A} {B = B} A⇔B = equivalence (↠⇒⇔ I↠J) B-to B-from
+      where
+      B-to : ∀ {x} → Func (A atₛ x) (B atₛ (ItoJ.to x))
+      B-to = toFunction A⇔B
 
-    B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.section I↠J y))
-    B-from = record
-      { to   = from      A⇔B ∘ cast      B (Surjection.to∘to⁻ I↠J _)
-      ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _)
-      }
+      B-from : ∀ {y} → Func (B atₛ y) (A atₛ (ItoJ.section y))
+      B-from = record
+        { to   = from      A⇔B ∘ cast      B (ItoJ.section-strictInverseˡ _)
+        ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.section-strictInverseˡ _)
+        }
 
 ------------------------------------------------------------------------
 -- Injections
@@ -168,12 +171,12 @@ module _ where
     func : Func (I ×ₛ A) (J ×ₛ B)
     func = function (Surjection.function I↠J) (Surjection.function A↠B)
 
-    to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
-    to⁻′ (j , y) = section I↠J j , section A↠B (cast B (Surjection.to∘to⁻ I↠J _) y)
+    section′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
+    section′ (j , y) = section I↠J j , section A↠B (cast B (section-strictInverseˡ I↠J _) y)
 
     strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func)
-    strictlySurj (j , y) = to⁻′ (j , y) ,
-      to∘to⁻ I↠J j , IndexedSetoid.trans B (to∘to⁻ A↠B _) (cast-eq B (to∘to⁻ I↠J j))
+    strictlySurj (j , y) = section′ (j , y) ,
+      section-strictInverseˡ I↠J j , IndexedSetoid.trans B (section-strictInverseˡ A↠B _) (cast-eq B (section-strictInverseˡ I↠J j))
 
     surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func)
     surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj

src/Function/Properties/Surjection.agda

@@ -45,7 +45,7 @@ mkSurjection f surjective = record
 ↠⇒⟶ = Surjection.function
 
 ↠⇒↪ : A ↠ B → B ↪ A
-↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → to∘to⁻ _ }
+↠⇒↪ s = mk↪ {from = to} λ { ≡.refl → section-strictInverseˡ _ }
   where open Surjection s
 
 ↠⇒⇔ : A ↠ B → A ⇔ B