fix: streamlining

Author: jamesmckinna

src/Function/Consequences.agda

@@ -50,8 +50,7 @@ inverseʳ⇒injective : ∀ (≈₂ : Rel B ℓ₂) f →
                      Transitive ≈₁ →
                      Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                      Injective ≈₁ ≈₂ f
-inverseʳ⇒injective ≈₂ f refl sym trans invʳ {x} {y} fx≈fy =
-  trans (sym (invʳ refl)) (invʳ fx≈fy)
+inverseʳ⇒injective ≈₂ f refl sym trans invʳ = trans (sym (invʳ refl)) ∘ invʳ
 
 ------------------------------------------------------------------------
 -- Inverseᵇ
@@ -69,16 +68,15 @@ inverseᵇ⇒bijective {f = f} ≈₂ refl sym trans (invˡ , invʳ) =
 -- StrictlySurjective
 
 surjective⇒strictlySurjective : ∀ (≈₂ : Rel B ℓ₂) →
-                                 Reflexive ≈₁ →
-                                 Surjective ≈₁ ≈₂ f →
-                                 StrictlySurjective ≈₂ f
-surjective⇒strictlySurjective _ refl surj x =
-  Product.map₂ (λ v → v refl) (surj x)
+                                Reflexive ≈₁ →
+                                Surjective ≈₁ ≈₂ f →
+                                StrictlySurjective ≈₂ f
+surjective⇒strictlySurjective _ refl surj = Product.map₂ (λ v → v refl) ∘ surj
 
 strictlySurjective⇒surjective : Transitive ≈₂ →
-                                 Congruent ≈₁ ≈₂ f →
-                                 StrictlySurjective ≈₂ f →
-                                 Surjective ≈₁ ≈₂ f
+                                Congruent ≈₁ ≈₂ f →
+                                StrictlySurjective ≈₂ f →
+                                Surjective ≈₁ ≈₂ f
 strictlySurjective⇒surjective trans cong surj x =
   Product.map₂ (λ fy≈x z≈y → trans (cong z≈y) fy≈x) (surj x)
 
@@ -134,7 +132,7 @@ module Section (≈₂ : Rel B ℓ₂) (surj :  Surjective {A = A} ≈₁ ≈₂
     strictlyInverseˡ _ = inverseˡ refl
 
     strictlyInverseʳ : StrictlyInverseʳ ≈₂ section f
-    strictlyInverseʳ _ = inverseˡ refl
+    strictlyInverseʳ = strictlyInverseˡ
 
     injective : Symmetric ≈₂ → Transitive ≈₂ → Injective ≈₂ ≈₁ section
     injective sym trans = trans (sym (strictlyInverseˡ _)) ∘ inverseˡ

src/Function/Structures.agda

@@ -60,7 +60,7 @@ record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   open IsCongruent isCongruent public
 
 
-record IsSurjection (f : A → B ) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     isCongruent : IsCongruent f
     surjective  : Surjective _≈₁_ _≈₂_ f
@@ -75,7 +75,7 @@ record IsSurjection (f : A → B ) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
   strictlySurjective = S.strictlySurjective Eq₁.refl
 
   strictlyInverseˡ : StrictlyInverseˡ _≈₂_ f section
-  strictlyInverseˡ _ = S.inverseˡ Eq₁.refl
+  strictlyInverseˡ _ = inverseˡ Eq₁.refl
 
 
 record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -120,7 +120,7 @@ record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ 
     renaming (cong to to-cong)
 
   strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
-  strictlyInverseˡ = inverseˡ⇒strictlyInverseˡ _≈₁_ _≈₂_ Eq₁.refl inverseˡ
+  strictlyInverseˡ _ = inverseˡ Eq₁.refl
 
   isSurjection : IsSurjection to
   isSurjection = record
@@ -139,10 +139,10 @@ record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁
     renaming (cong to to-cong)
 
   strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
-  strictlyInverseʳ = inverseʳ⇒strictlyInverseʳ _≈₁_ _≈₂_ Eq₂.refl inverseʳ
+  strictlyInverseʳ _ = inverseʳ Eq₂.refl
 
   injective : Injective _≈₁_ _≈₂_ to
-  injective = inverseʳ⇒injective {f⁻¹ = from} _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ
+  injective = inverseʳ⇒injective _≈₂_ to Eq₂.refl Eq₁.sym Eq₁.trans inverseʳ
 
   isInjection : IsInjection to
   isInjection = record