diff --git a/src/Data/Product/Function/Dependent/Propositional.agda b/src/Data/Product/Function/Dependent/Propositional.agda
index e39ec31bdc..8bc6f71257 100644
--- a/src/Data/Product/Function/Dependent/Propositional.agda
+++ b/src/Data/Product/Function/Dependent/Propositional.agda
@@ -194,19 +194,19 @@ 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 (section-strictInverseˡ I↠J _))
+    backcast = ≡.subst B (≡.sym (strictlyInverseˡ I↠J _))
 
     section′ : Σ J B → Σ I A
     section′ = map (section I↠J) (section A↠B ∘ backcast)
 
     strictlySurjective′ : StrictlySurjective _≡_ to′
     strictlySurjective′ (x , y) = section′ (x , y) , Σ-≡,≡→≡
-      ( section-strictInverseˡ I↠J x
+      ( strictlyInverseˡ 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) ⟩
+           ≡.subst B (strictlyInverseˡ I↠J x) (to A↠B (section A↠B (backcast y)))
+             ≡⟨ ≡.cong (≡.subst B _) (strictlyInverseˡ A↠B _) ⟩
+           ≡.subst B (strictlyInverseˡ I↠J x) (backcast y)
+             ≡⟨ ≡.subst-subst-sym (strictlyInverseˡ I↠J x) ⟩
            y
              ∎)
       ) where open ≡.≡-Reasoning
@@ -254,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.section-strictInverseˡ surjection′)
+    (Surjection.strictlyInverseˡ surjection′)
     left-inverse-of
     where
     open ≡.≡-Reasoning
diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index 32c52e5944..72fdd05347 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -122,8 +122,8 @@ module _ where
 
       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ˡ _)
+        { to   = from      A⇔B ∘ cast      B (ItoJ.strictlyInverseˡ _)
+        ; cong = from-cong A⇔B ∘ cast-cong B (ItoJ.strictlyInverseˡ _)
         }
 
 ------------------------------------------------------------------------
@@ -172,11 +172,11 @@ module _ where
     func = function (Surjection.function I↠J) (Surjection.function A↠B)
 
     section′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
-    section′ (j , y) = section I↠J j , section A↠B (cast B (section-strictInverseˡ I↠J _) y)
+    section′ (j , y) = section I↠J j , section A↠B (cast B (strictlyInverseˡ I↠J _) y)
 
     strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func)
     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))
+      strictlyInverseˡ I↠J j , IndexedSetoid.trans B (strictlyInverseˡ A↠B _) (cast-eq B (strictlyInverseˡ 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