fix: dependencies

Author: jamesmckinna

src/Function/Consequences.agda

@@ -133,6 +133,9 @@ module Section (≈₂ : Rel B ℓ₂) (surj :  Surjective {A = A} ≈₁ ≈₂
     strictlyInverseˡ : StrictlyInverseˡ ≈₂ f section
     strictlyInverseˡ _ = inverseˡ refl
 
+    strictlyInverseʳ : StrictlyInverseʳ ≈₂ section f
+    strictlyInverseʳ _ = inverseˡ refl
+
     injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section
     injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ
 
@@ -146,9 +149,6 @@ 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