refactor: lift out strictlyInverseʳ

Author: jamesmckinna

src/Function/Consequences.agda

@@ -146,6 +146,9 @@ module Section (≈₂ : Rel B ℓ₂) (surj :  Surjective {A = A} ≈₁ ≈₂
     inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section
     inverseʳ trans = inj ∘ trans (f∘section≡id _)
 
+    strictlyInverseʳ : Transitive ≈₂ → {!StrictlyInverseʳ ≈₂ section f!}
+    strictlyInverseʳ trans = inverseʳ⇒strictlyInverseʳ ≈₂ ≈₁ refl inverseˡ
+
     surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section
     surjective trans x = f x , inverseʳ trans