fix: type, and definition, of strictlyInverseʳ

Author: jamesmckinna

CHANGELOG.md

@@ -123,7 +123,7 @@ Additions to existing modules
   inverseˡ         : Inverseˡ _≈₁_ _≈₂_ to section
   strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to section
   inverseʳ         : Inverseʳ _≈₁_ _≈₂_ to section
-  strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section to
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to section
   ```
 
 * In `Function.Bundles.LeftInverse`:
@@ -162,7 +162,7 @@ Additions to existing modules
   inverseˡ         : Inverseˡ _≈₁_ _≈₂_ f section
   strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section
   inverseʳ         : Inverseʳ _≈₁_ _≈₂_ f section
-  strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section
   ```
 
 * In `Function.Structures.IsSurjection`:

src/Function/Consequences.agda

@@ -131,9 +131,6 @@ module Section (≈₂ : Rel B ℓ₂) (surj :  Surjective {A = A} ≈₁ ≈₂
     strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section
     strictlyInverseˡ _ = inverseˡ refl
 
-    strictlyInverseʳ : StrictlyInverseʳ ≈₂ section f
-    strictlyInverseʳ = strictlyInverseˡ
-
     injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section
     injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ
 
@@ -147,6 +144,9 @@ module Section (≈₂ : Rel B ℓ₂) (surj :  Surjective {A = A} ≈₁ ≈₂
     inverseʳ : Transitive ≈₂ → Inverseʳ ≈₁ ≈₂ f section
     inverseʳ trans = inj ∘ trans (f∘section≡id _)
 
+    strictlyInverseʳ : Reflexive ≈₂ → Transitive ≈₂ → StrictlyInverseʳ ≈₁ f section
+    strictlyInverseʳ refl trans _ = inverseʳ trans refl
+
     surjective : Transitive ≈₂ → Surjective ≈₂ ≈₁ section
     surjective trans x = f x , inverseʳ trans
 

src/Function/Structures.agda

@@ -102,8 +102,8 @@ record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   inverseʳ : Inverseʳ _≈₁_ _≈₂_ f section
   inverseʳ = S.inverseʳ injective Eq₁.refl Eq₂.trans
 
-  strictlyInverseʳ : StrictlyInverseʳ _≈₂_ section f
-  strictlyInverseʳ = S.strictlyInverseʳ Eq₁.refl
+  strictlyInverseʳ : StrictlyInverseʳ _≈₁_ f section
+  strictlyInverseʳ _ = inverseʳ Eq₂.refl
 
 
 ------------------------------------------------------------------------