Change to using strict inverses

Author: alexarice

src/Function/Construct/Composition.agda

@@ -35,39 +35,33 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
               Injective ≈₁ ≈₃ (g ∘ f)
   injective f-inj g-inj = f-inj ∘ g-inj
 
-  surjective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
-               Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
+  surjective : Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
                Surjective ≈₁ ≈₃ (g ∘ f)
-  surjective trans g-cong f-sur g-sur x with g-sur x
-  ... | y , fy≈x  with f-sur y
-  ...   | z , fz≈y = z , trans (g-cong fz≈y) fy≈x
+  surjective f-sur g-sur x with g-sur x
+  ... | y , gproof with f-sur y
+  ...   | z , fproof = z , λ a a≈z → gproof (f a) (fproof a a≈z)
 
-  bijective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
-              Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
+  bijective : Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
               Bijective ≈₁ ≈₃ (g ∘ f)
-  bijective trans g-cong (f-inj , f-sur) (g-inj , g-sur) =
-    injective f-inj g-inj , surjective trans g-cong f-sur g-sur
+  bijective (f-inj , f-sur) (g-inj , g-sur) =
+    injective f-inj g-inj , surjective f-sur g-sur
 
 module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
          (f : A → B) {f⁻¹ : B → A} {g : B → C} (g⁻¹ : C → B)
          where
 
-  inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
-             Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
+  inverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
              Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
-  inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x)
+  inverseˡ f-inv g-inv x y y≈gfx = g-inv x (f y) (f-inv (g⁻¹ x) y y≈gfx)
 
-  inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ →
-             Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
+  inverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
              Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
-  inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x)
+  inverseʳ f-inv g-inv x y y≈gfx = f-inv x (g⁻¹ y) (g-inv (f x) y y≈gfx)
 
-  inverseᵇ : Transitive ≈₁ → Transitive ≈₃ →
-             Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ →
-             Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
+  inverseᵇ : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
              Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
-  inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) =
-    inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ
+  inverseᵇ (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) =
+    inverseˡ f-invˡ g-invˡ , inverseʳ f-invʳ g-invʳ
 
 ------------------------------------------------------------------------
 -- Structures
@@ -95,14 +89,14 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
                  IsSurjection ≈₁ ≈₃ (g ∘ f)
   isSurjection f-surj g-surj = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
-    ; surjective   = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective
+    ; surjective   = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective
     } where module F = IsSurjection f-surj; module G = IsSurjection g-surj
 
   isBijection : IsBijection ≈₁ ≈₂ f → IsBijection ≈₂ ≈₃ g →
                 IsBijection ≈₁ ≈₃ (g ∘ f)
   isBijection f-bij g-bij = record
     { isInjection = isInjection F.isInjection G.isInjection
-    ; surjective  = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective
+    ; surjective  = surjective ≈₁ ≈₂ ≈₃ F.surjective G.surjective
     } where module F = IsBijection f-bij; module G = IsBijection g-bij
 
 module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
@@ -114,22 +108,22 @@ module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
   isLeftInverse f-invˡ g-invˡ = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
     ; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
-    ; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ f _ G.Eq₂.trans G.cong₁ F.inverseˡ G.inverseˡ
+    ; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ f _ F.inverseˡ G.inverseˡ
     } where module F = IsLeftInverse f-invˡ; module G = IsLeftInverse g-invˡ
 
   isRightInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₃ g g⁻¹ →
                    IsRightInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
   isRightInverse f-invʳ g-invʳ = record
     { isCongruent = isCongruent F.isCongruent G.isCongruent
     ; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
-    ; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
+    ; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.inverseʳ G.inverseʳ
     } where module F = IsRightInverse f-invʳ; module G = IsRightInverse g-invʳ
 
   isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₃ g g⁻¹ →
               IsInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
   isInverse f-inv g-inv = record
     { isLeftInverse = isLeftInverse F.isLeftInverse G.isLeftInverse
-    ; inverseʳ      = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
+    ; inverseʳ      = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.inverseʳ G.inverseʳ
     } where module F = IsInverse f-inv; module G = IsInverse g-inv
 
 ------------------------------------------------------------------------
@@ -150,14 +144,14 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
   surjection surj₁ surj₂ = record
     { f          = G.f ∘ F.f
     ; cong       = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
-    ; surjective = surjective (≈ R) (≈ S) (≈ T) G.Eq₂.trans G.cong F.surjective G.surjective
+    ; surjective = surjective (≈ R) (≈ S) (≈ T) F.surjective G.surjective
     } where module F = Surjection surj₁; module G = Surjection surj₂
 
   bijection : Bijection R S → Bijection S T → Bijection R T
   bijection bij₁ bij₂ = record
     { f         = G.f ∘ F.f
     ; cong      = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
-    ; bijective = bijective (≈ R) (≈ S) (≈ T) (trans T) G.cong F.bijective G.bijective
+    ; bijective = bijective (≈ R) (≈ S) (≈ T) F.bijective G.bijective
     } where module F = Bijection bij₁; module G = Bijection bij₂
 
   equivalence : Equivalence R S → Equivalence S T → Equivalence R T
@@ -174,7 +168,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
     ; g        = F.g ∘ G.g
     ; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
     ; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
-    ; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.f _ (trans T) G.cong₁ F.inverseˡ G.inverseˡ
+    ; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.f _ F.inverseˡ G.inverseˡ
     } where module F = LeftInverse invˡ₁; module G = LeftInverse invˡ₂
 
   rightInverse : RightInverse R S → RightInverse S T → RightInverse R T
@@ -183,7 +177,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
     ; g        = F.g ∘ G.g
     ; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
     ; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
-    ; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) _ G.g (trans R) F.cong₂ F.inverseʳ G.inverseʳ
+    ; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) _ G.g F.inverseʳ G.inverseʳ
     } where module F = RightInverse invʳ₁; module G = RightInverse invʳ₂
 
   inverse : Inverse R S → Inverse S T → Inverse R T
@@ -192,7 +186,7 @@ module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where
     ; f⁻¹     = F.f⁻¹ ∘ G.f⁻¹
     ; cong₁   = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
     ; cong₂   = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
-    ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ (trans R) (trans T) G.cong₁ F.cong₂ F.inverse G.inverse
+    ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ F.inverse G.inverse
     } where module F = Inverse inv₁; module G = Inverse inv₂
 
 ------------------------------------------------------------------------

src/Function/Construct/Identity.agda

@@ -32,20 +32,20 @@ module _ (_≈_ : Rel A ℓ) where
   injective : Injective id
   injective = id
 
-  surjective : Reflexive _≈_ → Surjective id
-  surjective refl x = x , refl
+  surjective : Surjective id
+  surjective x = x , λ z z≈x → z≈x
 
-  bijective : Reflexive _≈_ → Bijective id
-  bijective refl = injective , surjective refl
+  bijective : Bijective id
+  bijective = injective , surjective
 
-  inverseˡ : Reflexive _≈_ → Inverseˡ id id
-  inverseˡ refl x = refl
+  inverseˡ : Inverseˡ id id
+  inverseˡ x y y≈x = y≈x
 
-  inverseʳ : Reflexive _≈_ → Inverseʳ id id
-  inverseʳ refl x = refl
+  inverseʳ : Inverseʳ id id
+  inverseʳ x y y≈x = y≈x
 
-  inverseᵇ : Reflexive _≈_ → Inverseᵇ id id
-  inverseᵇ refl = inverseˡ refl , inverseʳ refl
+  inverseᵇ : Inverseᵇ id id
+  inverseᵇ = inverseˡ , inverseʳ
 
 ------------------------------------------------------------------------
 -- Structures
@@ -71,33 +71,33 @@ module _ {_≈_ : Rel A ℓ} (isEq : IsEquivalence _≈_) where
   isSurjection : IsSurjection id
   isSurjection = record
     { isCongruent = isCongruent
-    ; surjective  = surjective _≈_ refl
+    ; surjective  = surjective _≈_
     }
 
   isBijection : IsBijection id
   isBijection = record
     { isInjection = isInjection
-    ; surjective  = surjective _≈_ refl
+    ; surjective  = surjective _≈_
     }
 
   isLeftInverse : IsLeftInverse id id
   isLeftInverse = record
     { isCongruent = isCongruent
     ; cong₂       = id
-    ; inverseˡ    = inverseˡ _≈_ refl
+    ; inverseˡ    = inverseˡ _≈_
     }
 
   isRightInverse : IsRightInverse id id
   isRightInverse = record
     { isCongruent = isCongruent
     ; cong₂       = id
-    ; inverseʳ    = inverseʳ _≈_ refl
+    ; inverseʳ    = inverseʳ _≈_
     }
 
   isInverse : IsInverse id id
   isInverse = record
     { isLeftInverse = isLeftInverse
-    ; inverseʳ      = inverseʳ _≈_ refl
+    ; inverseʳ      = inverseʳ _≈_
     }
 
 ------------------------------------------------------------------------
@@ -118,14 +118,14 @@ module _ (S : Setoid a ℓ) where
   surjection = record
     { f          = id
     ; cong       = id
-    ; surjective = surjective _≈_ refl
+    ; surjective = surjective _≈_
     }
 
   bijection : Bijection S S
   bijection = record
     { f         = id
     ; cong      = id
-    ; bijective = bijective _≈_ refl
+    ; bijective = bijective _≈_
     }
 
   equivalence : Equivalence S S
@@ -142,7 +142,7 @@ module _ (S : Setoid a ℓ) where
     ; g        = id
     ; cong₁    = id
     ; cong₂    = id
-    ; inverseˡ = inverseˡ _≈_ refl
+    ; inverseˡ = inverseˡ _≈_
     }
 
   rightInverse : RightInverse S S
@@ -151,7 +151,7 @@ module _ (S : Setoid a ℓ) where
     ; g        = id
     ; cong₁    = id
     ; cong₂    = id
-    ; inverseʳ = inverseʳ _≈_ refl
+    ; inverseʳ = inverseʳ _≈_
     }
 
   inverse : Inverse S S
@@ -160,7 +160,7 @@ module _ (S : Setoid a ℓ) where
     ; f⁻¹     = id
     ; cong₁   = id
     ; cong₂   = id
-    ; inverse = inverseᵇ _≈_ refl
+    ; inverse = inverseᵇ _≈_
     }
 
 ------------------------------------------------------------------------

src/Function/Definitions.agda

@@ -30,17 +30,17 @@ Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y
 Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
 Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
 
-open Core₂ _≈₂_ public
-  using (Surjective)
+Surjective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+Surjective f = ∀ y → ∃ λ x → ∀ z → z ≈₁ x → f z ≈₂ y
 
 Bijective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
 Bijective f = Injective f × Surjective f
 
-open Core₂ _≈₂_ public
-  using (Inverseˡ)
+Inverseˡ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+Inverseˡ f g = ∀ x y → y ≈₁ g x → f y ≈₂ x
 
-open Core₁ _≈₁_ public
-  using (Inverseʳ)
+Inverseʳ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+Inverseʳ f g = ∀ x y → y ≈₂ f x → g y ≈₁ x
 
 Inverseᵇ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
 Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g