From c9a31ec39687fc669abf459902dc45a7ac67d063 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Thu, 28 Dec 2023 17:09:52 -0500 Subject: [PATCH] Revert "change definition of function sets equality to not build-in cong (see agda-stdlib issue #1467 for further information). Fix everything that needed fixed because of that - a lot." This reverts commit c0b266180f6f6df7d3229d0034547b1adbc65639. This is because this shouldn't have been done on master, but through a branch (which it now is) and will get a proper review. --- src/Categories/Adjoint.agda | 8 +- src/Categories/Adjoint/Equivalents.agda | 40 ++--- .../Adjoint/Instance/0-Truncation.agda | 13 +- .../Adjoint/Instance/PosetCore.agda | 12 +- src/Categories/Adjoint/Mate.agda | 14 +- src/Categories/Adjoint/Relative.agda | 16 +- .../Construction/Spans/Properties.agda | 14 +- .../Category/Concrete/Properties.agda | 37 ++-- .../Properties/Presheaves/Cartesian.agda | 26 +-- .../Presheaves/CartesianClosed.agda | 85 ++++----- .../Presheaves/FromCartesianCCC.agda | 137 ++++++++------- .../Category/Instance/FamilyOfSetoids.agda | 12 +- .../Instance/Properties/Setoids/CCC.agda | 16 +- .../Instance/Properties/Setoids/Choice.agda | 6 +- .../Properties/Setoids/Cocomplete.agda | 19 +- .../Instance/Properties/Setoids/Complete.agda | 16 +- .../Instance/Properties/Setoids/Exact.agda | 94 ++++++---- .../Properties/Setoids/Extensive.agda | 31 ++-- .../Instance/Properties/Setoids/LCCC.agda | 79 ++++----- .../Properties/Setoids/Limits/Canonical.agda | 10 +- src/Categories/Category/Instance/Setoids.agda | 16 +- .../Instance/SimplicialSet/Properties.agda | 28 +-- .../Category/Monoidal/Instance/Setoids.agda | 14 +- .../Category/Species/Constructions.agda | 25 ++- src/Categories/CoYoneda.agda | 85 +++++---- src/Categories/Enriched/Over/Setoids.agda | 19 +- .../Functor/Construction/LiftSetoids.agda | 8 +- src/Categories/Functor/Hom.agda | 34 +++- .../Functor/Hom/Properties/Contra.agda | 8 +- .../Functor/Hom/Properties/Covariant.agda | 14 +- .../Functor/Instance/0-Truncation.agda | 11 +- .../Functor/Instance/ConnectedComponents.agda | 25 ++- .../Functor/Instance/SetoidDiscrete.agda | 8 +- src/Categories/Functor/Profunctor.agda | 166 +++++++----------- .../Functor/Profunctor/Cograph.agda | 25 ++- .../Functor/Profunctor/FormalComposite.agda | 20 ++- src/Categories/NaturalTransformation/Hom.agda | 18 +- .../NaturalIsomorphism/Properties.agda | 4 +- .../NaturalTransformation/Properties.agda | 2 +- src/Categories/Yoneda.agda | 78 ++++---- src/Categories/Yoneda/Continuous.agda | 40 ++--- src/Categories/Yoneda/Properties.agda | 43 +++-- src/Function/Construct/Setoid.agda | 13 +- 43 files changed, 723 insertions(+), 666 deletions(-) diff --git a/src/Categories/Adjoint.agda b/src/Categories/Adjoint.agda index ee3b290f4..f42782e54 100644 --- a/src/Categories/Adjoint.agda +++ b/src/Categories/Adjoint.agda @@ -185,18 +185,18 @@ record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ leve { to = λ f → lift (Ladjunct (lower f)) ; cong = λ eq → lift (Ladjunct-resp-≈ (lower eq)) } - ; commute = λ _ → lift $ Ladjunct-comm D.Equiv.refl + ; commute = λ _ eq → lift $ Ladjunct-comm (lower eq) } ; F⇐G = ntHelper record { η = λ _ → record { to = λ f → lift (Radjunct (lower f)) ; cong = λ eq → lift (Radjunct-resp-≈ (lower eq)) } - ; commute = λ _ → lift $ Radjunct-comm C.Equiv.refl + ; commute = λ _ eq → lift $ Radjunct-comm (lower eq) } ; iso = λ X → record - { isoˡ = lift RLadjunct≈id - ; isoʳ = lift LRadjunct≈id + { isoˡ = λ eq → let open D.HomReasoning in lift (RLadjunct≈id ○ lower eq) + ; isoʳ = λ eq → let open C.HomReasoning in lift (LRadjunct≈id ○ lower eq) } } diff --git a/src/Categories/Adjoint/Equivalents.agda b/src/Categories/Adjoint/Equivalents.agda index 9e05b755c..a36e5fcd7 100644 --- a/src/Categories/Adjoint/Equivalents.agda +++ b/src/Categories/Adjoint/Equivalents.agda @@ -50,15 +50,15 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : Hom-NI′ = record { F⇒G = ntHelper record { η = λ _ → record { to = Hom-inverse.to ; cong = Hom-inverse.to-cong } - ; commute = λ _ → Ladjunct-comm D.Equiv.refl + ; commute = λ _ eq → Ladjunct-comm eq } ; F⇐G = ntHelper record { η = λ _ → record { to = Hom-inverse.from ; cong = Hom-inverse.from-cong } - ; commute = λ _ → Radjunct-comm C.Equiv.refl + ; commute = λ _ eq → Radjunct-comm eq } ; iso = λ _ → record - { isoˡ = RLadjunct≈id - ; isoʳ = LRadjunct≈id + { isoˡ = λ eq → let open D.HomReasoning in RLadjunct≈id ○ eq + ; isoʳ = λ eq → let open C.HomReasoning in LRadjunct≈id ○ eq } } @@ -88,10 +88,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : { η = λ X → unitη X ⟨$⟩ D.id ; commute = λ {X} {Y} f → begin (unitη Y ⟨$⟩ D.id) ∘ f ≈⟨ introˡ R.identity ⟩ - R.F₁ D.id ∘ (unitη Y ⟨$⟩ D.id) ∘ f ≈˘⟨ ⇒.commute (f , D.id) ⟩ + R.F₁ D.id ∘ (unitη Y ⟨$⟩ D.id) ∘ f ≈˘⟨ ⇒.commute (f , D.id) D.Equiv.refl ⟩ ⇒.η (X , L.F₀ Y) ⟨$⟩ (D.id D.∘ D.id D.∘ L.F₁ f) ≈⟨ cong (⇒.η (X , L.F₀ Y)) (D.Equiv.trans D.identityˡ D.identityˡ) ⟩ ⇒.η (X , L.F₀ Y) ⟨$⟩ L.F₁ f ≈⟨ cong (⇒.η (X , L.F₀ Y)) (MR.introʳ D (MR.elimʳ D L.identity)) ⟩ - ⇒.η (X , L.F₀ Y) ⟨$⟩ (L.F₁ f D.∘ D.id D.∘ L.F₁ id) ≈⟨ ⇒.commute (C.id , L.F₁ f) ⟩ + ⇒.η (X , L.F₀ Y) ⟨$⟩ (L.F₁ f D.∘ D.id D.∘ L.F₁ id) ≈⟨ ⇒.commute (C.id , L.F₁ f) D.Equiv.refl ⟩ R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id) ∎ } @@ -107,10 +107,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : { η = λ X → counitη X ⟨$⟩ C.id ; commute = λ {X} {Y} f → begin (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f) ≈˘⟨ identityˡ ⟩ - id ∘ (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f) ≈˘⟨ ⇐.commute (R.F₁ f , D.id) ⟩ + id ∘ (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f) ≈˘⟨ ⇐.commute (R.F₁ f , D.id) C.Equiv.refl ⟩ ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ R.F₁ f) ≈⟨ cong (⇐.η (R.F₀ X , Y)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩ ⇐.η (R.F₀ X , Y) ⟨$⟩ R.F₁ f ≈⟨ cong (⇐.η (R.F₀ X , Y)) (MR.introʳ C C.identityˡ) ⟩ - ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ f C.∘ C.id C.∘ C.id) ≈⟨ ⇐.commute (C.id , f) ⟩ + ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ f C.∘ C.id C.∘ C.id) ≈⟨ ⇐.commute (C.id , f) C.Equiv.refl ⟩ f ∘ (counitη X ⟨$⟩ C.id) ∘ L.F₁ C.id ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩ f ∘ (counitη X ⟨$⟩ C.id) ∎ } @@ -129,10 +129,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : open MR D in begin η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ identityˡ ⟩ - id ∘ η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ ⇐.commute (η unit A , id) ⟩ + id ∘ η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ ⇐.commute (η unit A , id) C.Equiv.refl ⟩ ⇐.η (A , L.F₀ A) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ η unit A) ≈⟨ cong (⇐.η (A , L.F₀ A)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩ - ⇐.η (A , L.F₀ A) ⟨$⟩ η unit A ≈⟨ isoˡ ⟩ + ⇐.η (A , L.F₀ A) ⟨$⟩ η unit A ≈⟨ isoˡ refl ⟩ id ∎ ; zag = λ {B} → @@ -142,10 +142,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : open MR C in begin R.F₁ (η counit B) ∘ η unit (R.F₀ B) ≈˘⟨ refl⟩∘⟨ identityʳ ⟩ - R.F₁ (η counit B) ∘ η unit (R.F₀ B) ∘ id ≈˘⟨ ⇒.commute (id , η counit B) ⟩ + R.F₁ (η counit B) ∘ η unit (R.F₀ B) ∘ id ≈˘⟨ ⇒.commute (id , η counit B) D.Equiv.refl ⟩ ⇒.η (R.F₀ B , B) ⟨$⟩ (η counit B D.∘ D.id D.∘ L.F₁ id) ≈⟨ cong (⇒.η (R.F₀ B , B)) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩ - ⇒.η (R.F₀ B , B) ⟨$⟩ η counit B ≈⟨ isoʳ ⟩ + ⇒.η (R.F₀ B , B) ⟨$⟩ η counit B ≈⟨ isoʳ refl ⟩ id ∎ } where module i {X} = Iso (iso X) @@ -180,13 +180,13 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D lower (unitη Y ⟨$⟩ lift D.id) ∘ f ≈⟨ introˡ R.identity ⟩ R.F₁ D.id ∘ lower (unitη Y ⟨$⟩ lift D.id) ∘ f - ≈˘⟨ lower (⇒.commute (f , D.id)) ⟩ + ≈˘⟨ lower (⇒.commute (f , D.id) (lift D.Equiv.refl)) ⟩ lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (D.id D.∘ D.id D.∘ L.F₁ f)) ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (D.Equiv.trans D.identityˡ D.identityˡ))) ⟩ lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f)) ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (MR.introʳ D (MR.elimʳ D L.identity)))) ⟩ lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f D.∘ D.id D.∘ L.F₁ id)) - ≈⟨ lower (⇒.commute (C.id , L.F₁ f)) ⟩ + ≈⟨ lower (⇒.commute (C.id , L.F₁ f) (lift D.Equiv.refl)) ⟩ R.F₁ (L.F₁ f) ∘ lower (⇒.η (X , L.F₀ X) ⟨$⟩ lift D.id) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ F₁ (R ∘F L) f ∘ lower (unitη X ⟨$⟩ lift D.id) ∎ @@ -205,13 +205,13 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f) ≈˘⟨ identityˡ ⟩ id ∘ lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f) - ≈˘⟨ lower (⇐.commute (R.F₁ f , D.id)) ⟩ + ≈˘⟨ lower (⇐.commute (R.F₁ f , D.id) (lift C.Equiv.refl)) ⟩ lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ R.F₁ f)) ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩ lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f)) ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (MR.introʳ C C.identityˡ))) ⟩ lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f C.∘ C.id C.∘ C.id)) - ≈⟨ lower (⇐.commute (C.id , f)) ⟩ + ≈⟨ lower (⇐.commute (C.id , f) (lift C.Equiv.refl)) ⟩ f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id) ∘ L.F₁ C.id ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩ f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id) @@ -234,11 +234,11 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A) ≈˘⟨ identityˡ ⟩ id ∘ lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A) - ≈˘⟨ lower (⇐.commute (η unit A , id)) ⟩ + ≈˘⟨ lower (⇐.commute (η unit A , id) (lift C.Equiv.refl)) ⟩ lower (⇐.η (A , L.F₀ A) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ lower (⇒.η (A , L.F₀ A) ⟨$⟩ lift id))) ≈⟨ lower (cong (⇐.η (A , L.F₀ A)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩ lower (⇐.η (A , L.F₀ A) ⟨$⟩ (⇒.η (A , L.F₀ A) ⟨$⟩ lift id)) - ≈⟨ lower (isoˡ) ⟩ + ≈⟨ lower (isoˡ (lift refl)) ⟩ id ∎ ; zag = λ {B} → let open C @@ -249,11 +249,11 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id) ≈˘⟨ refl⟩∘⟨ identityʳ ⟩ R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id) ∘ id - ≈˘⟨ lower (⇒.commute (id , η counit B)) ⟩ + ≈˘⟨ lower (⇒.commute (id , η counit B) (lift D.Equiv.refl)) ⟩ lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id) D.∘ D.id D.∘ L.F₁ id)) ≈⟨ lower (cong (⇒.η (R.F₀ B , B)) (lift (MR.elimʳ D (MR.elimʳ D L.identity)))) ⟩ lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id))) - ≈⟨ lower isoʳ ⟩ + ≈⟨ lower (isoʳ (lift refl)) ⟩ id ∎ } where open NaturalTransformation diff --git a/src/Categories/Adjoint/Instance/0-Truncation.agda b/src/Categories/Adjoint/Instance/0-Truncation.agda index 38b609338..248abef27 100644 --- a/src/Categories/Adjoint/Instance/0-Truncation.agda +++ b/src/Categories/Adjoint/Instance/0-Truncation.agda @@ -5,18 +5,19 @@ module Categories.Adjoint.Instance.0-Truncation where -- The adjunction between 0-truncation and the inclusion functor from -- Setoids to Categories/Groupoids. +open import Level using (Lift) +open import Data.Unit using (⊤) open import Function.Base renaming (id to id→) open import Function.Bundles using (Func) import Function.Construct.Identity as Id open import Relation.Binary using (Setoid) open import Categories.Adjoint using (_⊣_) -open import Categories.Category.Core using (Category) open import Categories.Category.Construction.0-Groupoid using (0-Groupoid) open import Categories.Category.Groupoid using (Groupoid) open import Categories.Category.Instance.Groupoids using (Groupoids) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) +open import Categories.Functor renaming (id to idF) open import Categories.Functor.Instance.0-Truncation using (Trunc) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Categories.NaturalTransformation.NaturalIsomorphism using (refl) @@ -33,8 +34,8 @@ Inclusion {c} {ℓ} e = record let module S = Setoid S module T = Setoid T in record - { F⇒G = record { η = λ _ → f≗g } - ; F⇐G = record { η = λ _ → T.sym f≗g } + { F⇒G = record { η = λ _ → f≗g S.refl } + ; F⇐G = record { η = λ _ → T.sym (f≗g S.refl) } } } where open Func @@ -45,7 +46,7 @@ TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e TruncAdj {o} {ℓ} {e} = record { unit = unit ; counit = counit - ; zig = λ {A} → Category.id (category A) + ; zig = id→ ; zag = refl } where @@ -60,4 +61,4 @@ TruncAdj {o} {ℓ} {e} = record } counit : NaturalTransformation (Trunc ∘F Inclusion e) idF - counit = ntHelper record { η = Id.function; commute = λ {_} {Y} _ → Setoid.refl Y } + counit = ntHelper record { η = Id.function; commute = λ f → cong f } diff --git a/src/Categories/Adjoint/Instance/PosetCore.agda b/src/Categories/Adjoint/Instance/PosetCore.agda index 4961a7673..9bd939375 100644 --- a/src/Categories/Adjoint/Instance/PosetCore.agda +++ b/src/Categories/Adjoint/Instance/PosetCore.agda @@ -40,7 +40,7 @@ Forgetful = record ; F₁ = λ f → mkPosetHomo _ _ (to f) (cong f) ; identity = λ {S} → refl S ; homomorphism = λ {_ _ S} → refl S - ; F-resp-≈ = λ {S _} f≗g → f≗g + ; F-resp-≈ = λ {S _} f≗g → f≗g (refl S) } where Forgetful₀ : ∀ {c ℓ} → Setoid c ℓ → Poset c ℓ ℓ @@ -72,9 +72,9 @@ Core : ∀ {c ℓ₁ ℓ₂} → Functor (Posets c ℓ₁ ℓ₂) (Setoids c ℓ Core = record { F₀ = λ A → record { isEquivalence = isEquivalence A } ; F₁ = λ f → record { to = ⟦ f ⟧ ; cong = cong f } - ; identity = λ {A} → Eq.refl A - ; homomorphism = λ {_ _ Z} → Eq.refl Z - ; F-resp-≈ = λ f≗g → f≗g + ; identity = Function.id + ; homomorphism = λ {_ _ _ f g} → cong (Comp.posetHomomorphism f g) + ; F-resp-≈ = λ {_ B} {f _} f≗g x≈y → Eq.trans B (cong f x≈y) f≗g } where open Poset @@ -82,10 +82,10 @@ Core = record CoreAdj : ∀ {o ℓ} → Forgetful ⊣ Core {o} {ℓ} {ℓ} CoreAdj = record - { unit = ntHelper record { η = unit ; commute = λ {_} {Y} _ → Setoid.refl Y} + { unit = ntHelper record { η = unit ; commute = cong } ; counit = ntHelper record { η = counit ; commute = λ {_ B} _ → Eq.refl B } ; zig = λ {S} → Setoid.refl S - ; zag = λ {B} → Eq.refl B + ; zag = Function.id } where open Poset diff --git a/src/Categories/Adjoint/Mate.agda b/src/Categories/Adjoint/Mate.agda index 5b670afbd..c70894499 100644 --- a/src/Categories/Adjoint/Mate.agda +++ b/src/Categories/Adjoint/Mate.agda @@ -8,7 +8,7 @@ open import Level open import Data.Product using (Σ; _,_) open import Function.Bundles using (Func; _⟨$⟩_) open import Function.Construct.Composition using (function) -open import Function.Construct.Setoid using () renaming (setoid to _⇨_) +open import Function.Construct.Setoid using () renaming (function to _⇨_) open import Relation.Binary using (Setoid; IsEquivalence) open import Categories.Category @@ -135,13 +135,13 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C} mate-commute₁ : function D⟶C (F₁ Hom[ C ][-,-] (C.id , β.η Y)) ≈ function (F₁ Hom[ D ][-,-] (α.η X , D.id)) D⟶C′ - mate-commute₁ {f} = begin + mate-commute₁ {f} {g} f≈g = begin β.η Y ∘ (F₁ R′ f ∘ L′⊣R′.unit.η X) ∘ C.id ≈⟨ refl⟩∘⟨ identityʳ ⟩ β.η Y ∘ F₁ R′ f ∘ L′⊣R′.unit.η X ≈⟨ pullˡ (β.commute f) ⟩ (F₁ R f ∘ β.η (F₀ L′ X)) ∘ L′⊣R′.unit.η X ≈˘⟨ pushʳ commute₁ ⟩ F₁ R f ∘ F₁ R (α.η X) ∘ L⊣R.unit.η X ≈˘⟨ pushˡ (homomorphism R) ⟩ - F₁ R (f D.∘ α.η X) ∘ L⊣R.unit.η X ≈⟨ F-resp-≈ R (DH.⟺ D.identityˡ) ⟩∘⟨refl ⟩ - F₁ R (D.id D.∘ f D.∘ α.η X) ∘ L⊣R.unit.η X ∎ + F₁ R (f D.∘ α.η X) ∘ L⊣R.unit.η X ≈⟨ F-resp-≈ R (D.∘-resp-≈ˡ f≈g DH.○ DH.⟺ D.identityˡ) ⟩∘⟨refl ⟩ + F₁ R (D.id D.∘ g D.∘ α.η X) ∘ L⊣R.unit.η X ∎ module _ {X : C.Obj} {Y : D.Obj} where open D hiding (_≈_) @@ -173,13 +173,13 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C} mate-commute₂ : function C⟶D (F₁ Hom[ D ][-,-] (α.η X , D.id)) ≈ function (F₁ Hom[ C ][-,-] (C.id , β.η Y)) C⟶D′ - mate-commute₂ {f} = begin + mate-commute₂ {f} {g} f≈g = begin D.id ∘ (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X ≈⟨ identityˡ ⟩ (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X ≈˘⟨ pushʳ (α.commute f) ⟩ L′⊣R′.counit.η Y ∘ α.η (F₀ R′ Y) ∘ F₁ L f ≈˘⟨ pushˡ commute₂ ⟩ (L⊣R.counit.η Y ∘ F₁ L (β.η Y)) ∘ F₁ L f ≈˘⟨ pushʳ (homomorphism L) ⟩ - L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f) ≈⟨ refl⟩∘⟨ F-resp-≈ L (C.∘-resp-≈ʳ (CH.⟺ C.identityʳ)) ⟩ - L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f C.∘ C.id) ∎ + L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ f) ≈⟨ refl⟩∘⟨ F-resp-≈ L (C.∘-resp-≈ʳ (f≈g CH.○ CH.⟺ C.identityʳ)) ⟩ + L⊣R.counit.η Y ∘ F₁ L (β.η Y C.∘ g C.∘ C.id) ∎ -- alternatively, if commute₃ and commute₄ are shown, then a Mate can be constructed. diff --git a/src/Categories/Adjoint/Relative.agda b/src/Categories/Adjoint/Relative.agda index fbfea6e65..3036b4eeb 100644 --- a/src/Categories/Adjoint/Relative.agda +++ b/src/Categories/Adjoint/Relative.agda @@ -66,7 +66,7 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record ; unit = λ {c} → ⇐.η (c , F₀ L c) ⟨$⟩ D.id {F₀ L c} ; extend = λ {X} {Y} k → F₁ R (⇒.η (X , F₀ L Y) ⟨$⟩ k) ; identityʳ = idʳ - ; identityˡ = R.F-resp-≈ (iso.isoʳ _) ○ R.identity + ; identityˡ = R.F-resp-≈ (iso.isoʳ _ D.Equiv.refl) ○ R.identity ; assoc = a ; sym-assoc = sym a ; extend-≈ = λ k≈h → F-resp-≈ R (Func.cong (⇒.η _) k≈h) @@ -88,9 +88,9 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record idʳ {x} {y} {k} = begin R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id) ≈⟨ introʳ J.identity ⟩ (R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id)) ∘ J.₁ E.id ≈⟨ assoc ⟩ - R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id) ∘ J.₁ E.id ≈⟨ ⇐.sym-commute (E.id , ⇒.η (x , L.₀ y) ⟨$⟩ k) ⟩ + R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id) ∘ J.₁ E.id ≈⟨ ⇐.sym-commute (E.id , ⇒.η (x , L.₀ y) ⟨$⟩ k) (D.Equiv.refl) ⟩ ⇐.η (x , L.₀ y) ⟨$⟩ ((⇒.η (x , L.₀ y) ⟨$⟩ k) D.∘ D.id D.∘ L.F₁ E.id) ≈⟨ Func.cong (⇐.η _) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩ - ⇐.η (x , L.₀ y) ⟨$⟩ (⇒.η (x , L.₀ y) ⟨$⟩ k) ≈⟨ iso.isoˡ (x , _) ⟩ + ⇐.η (x , L.₀ y) ⟨$⟩ (⇒.η (x , L.₀ y) ⟨$⟩ k) ≈⟨ iso.isoˡ (x , _) Equiv.refl ⟩ k ∎ a : {x y z : E.Obj} {k : J.₀ x ⇒ R.₀ (L.₀ y)} {l : J.₀ y ⇒ R.₀ (L.₀ z)} → R.₁ (⇒.η (x , L.₀ z) ⟨$⟩ R.₁ (⇒.η (y , L.₀ z) ⟨$⟩ l) ∘ k) ≈ @@ -107,7 +107,7 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record lemma : ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k D.≈ (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k) lemma = DR.begin ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k DR.≈⟨ Func.cong (⇒.η xz) (refl⟩∘⟨ introʳ J.identity ) ⟩ - ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ (k ∘ J.₁ E.id) DR.≈⟨ ⇒.commute (E.id , ⇒.η yz ⟨$⟩ l) ⟩ + ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ (k ∘ J.₁ E.id) DR.≈⟨ ⇒.commute (E.id , ⇒.η yz ⟨$⟩ l) Equiv.refl ⟩ (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k) D.∘ L.₁ E.id DR.≈⟨ D.sym-assoc ⟩ ((⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k)) D.∘ L.₁ E.id DR.≈⟨ MR.elimʳ D L.identity ⟩ (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k) DR.∎ @@ -119,15 +119,15 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record ; Hom-NI = record { F⇒G = ntHelper record { η = λ _ → record { to = Radjunct ; cong = ∘-resp-≈ʳ ∙ L.F-resp-≈ } - ; commute = λ _ → Radjunct-comm C.Equiv.refl + ; commute = λ _ x≈y → Radjunct-comm x≈y } ; F⇐G = ntHelper record { η = λ _ → record { to = Ladjunct ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈ } - ; commute = λ _ → Ladjunct-comm Equiv.refl + ; commute = λ _ x≈y → Ladjunct-comm x≈y } ; iso = λ X → record - { isoˡ = LRadjunct≈id - ; isoʳ = RLadjunct≈id + { isoˡ = λ eq → LRadjunct≈id ○ eq + ; isoʳ = Equiv.trans RLadjunct≈id } } } diff --git a/src/Categories/Bicategory/Construction/Spans/Properties.agda b/src/Categories/Bicategory/Construction/Spans/Properties.agda index e7160b68d..5c66582d1 100644 --- a/src/Categories/Bicategory/Construction/Spans/Properties.agda +++ b/src/Categories/Bicategory/Construction/Spans/Properties.agda @@ -61,8 +61,8 @@ module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where id⇒ : (X : Carrier T.C) → Hom X X id⇒ X = record { hom = arr T.η ⟨$⟩ X - ; dom-eq = commute-dom T.η - ; cod-eq = commute-cod T.η + ; dom-eq = commute-dom T.η (refl T.C) + ; cod-eq = commute-cod T.η (refl T.C) } _×ₚ_ : ∀ {A B C} → (f : Hom B C) → (g : Hom A B) → FiberProduct (Span.cod T.T) (Span.dom T.T) @@ -81,11 +81,11 @@ module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where _∘⇒_ {A = A} {C = C} f g = record { hom = arr T.μ ⟨$⟩ (f ×ₚ g) ; dom-eq = begin - Span.dom T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-dom T.μ {f ×ₚ g} ⟩ + Span.dom T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ (commute-dom T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl)) ⟩ Span.dom T.T ⟨$⟩ hom g ≈⟨ dom-eq g ⟩ A ∎ ; cod-eq = begin - Span.cod T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-cod T.μ {f ×ₚ g} ⟩ + Span.cod T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-cod T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl) ⟩ Span.cod T.T ⟨$⟩ hom f ≈⟨ cod-eq f ⟩ C ∎ } @@ -111,16 +111,16 @@ module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where } in begin arr T.μ ⟨$⟩ ((h ∘⇒ g) ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl)) ⟩ - arr T.μ ⟨$⟩ _ ≈⟨ T.sym-assoc {f×ₚ⟨g×ₚh⟩} ⟩ + arr T.μ ⟨$⟩ _ ≈⟨ T.sym-assoc {f×ₚ⟨g×ₚh⟩} {f×ₚ⟨g×ₚh⟩} ((HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl) ⟩ arr T.μ ⟨$⟩ _ ≈⟨ (cong (arr T.μ) (cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl)) ⟩ arr T.μ ⟨$⟩ (h ×ₚ (g ∘⇒ f)) ∎ ; identityˡ = λ {A} {B} {f} → begin arr T.μ ⟨$⟩ (id⇒ B ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.η) (ObjSetoid.sym (cod-eq f))) ⟩ - arr T.μ ⟨$⟩ _ ≈⟨ T.identityʳ ⟩ + arr T.μ ⟨$⟩ _ ≈⟨ T.identityʳ HomSetoid.refl ⟩ hom f ∎ ; identityʳ = λ {A} {B} {f} → begin arr T.μ ⟨$⟩ (f ×ₚ id⇒ A) ≈⟨ cong (arr T.μ) (cong (arr T.η) (ObjSetoid.sym (dom-eq f)) , HomSetoid.refl) ⟩ - arr T.μ ⟨$⟩ _ ≈⟨ T.identityˡ ⟩ + arr T.μ ⟨$⟩ _ ≈⟨ T.identityˡ HomSetoid.refl ⟩ hom f ∎ ; equiv = record { refl = HomSetoid.refl diff --git a/src/Categories/Category/Concrete/Properties.agda b/src/Categories/Category/Concrete/Properties.agda index 2f4724180..47b511099 100644 --- a/src/Categories/Category/Concrete/Properties.agda +++ b/src/Categories/Category/Concrete/Properties.agda @@ -7,7 +7,7 @@ open import Function.Base using (const; _∘_) open import Function.Bundles using (Func; _⟨$⟩_) import Function.Construct.Constant as Const import Function.Construct.Composition as Comp -open import Level using (Level; lift) +open import Level using (Level) open import Relation.Binary using (Setoid) import Relation.Binary.Reasoning.Setoid as SR @@ -35,36 +35,36 @@ open Func { F⇒G = ntHelper record { η = λ X → record { to = λ x → L.counit.η X C.∘ F.₁ (Const.function OneS (U.F₀ X) x) - ; cong = λ i≈j → C.∘-resp-≈ʳ (F.F-resp-≈ i≈j) + ; cong = λ i≈j → C.∘-resp-≈ʳ (F.F-resp-≈ λ _ → i≈j) } - ; commute = λ {X} {Y} f {x} → + ; commute = λ {X} {Y} f {x} {y} x≈y → let open C.HomReasoning in begin - L.counit.η Y C.∘ F.₁ (constF Y (U.₁ f ⟨$⟩ x)) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (Setoid.refl (U.₀ Y)) ⟩ - L.counit.η Y C.∘ F.₁ (Comp.function (constF X x) (U.F₁ f)) ≈⟨ pushʳ F.homomorphism ⟩ - ((L.counit.η Y C.∘ F.₁ (U.₁ f)) C.∘ F.₁ (constF X x)) ≈⟨ pushˡ (commute L.counit f) ⟩ - f C.∘ L.counit.η X C.∘ F.₁ (constF X x) ≈˘⟨ C.identityʳ ⟩ - (f C.∘ L.counit.η X C.∘ F.₁ (constF X x)) C.∘ C.id ∎ + L.counit.η Y C.∘ F.₁ (constF Y (U.₁ f ⟨$⟩ x)) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (λ _ → cong (U.₁ f) x≈y) ⟩ + L.counit.η Y C.∘ F.₁ (Comp.function (constF X y) (U.F₁ f)) ≈⟨ pushʳ F.homomorphism ⟩ + ((L.counit.η Y C.∘ F.₁ (U.₁ f)) C.∘ F.₁ (constF X y)) ≈⟨ pushˡ (commute L.counit f) ⟩ + f C.∘ L.counit.η X C.∘ F.₁ (constF X y) ≈˘⟨ C.identityʳ ⟩ + (f C.∘ L.counit.η X C.∘ F.₁ (constF X y)) C.∘ C.id ∎ } ; F⇐G = ntHelper record { η = λ c → record { to = λ 1⇒c → U.₁ 1⇒c ⟨$⟩ η1 - ; cong = λ i≈j → U.F-resp-≈ i≈j + ; cong = λ i≈j → U.F-resp-≈ i≈j (Setoid.refl (U.₀ (F.₀ OneS))) } - ; commute = λ {X} {Y} f {x} → + ; commute = λ {X} {Y} f {x} {y} x≈y → let module CH = C.HomReasoning in let open SR (U.₀ Y) in begin - U.₁ ((f C.∘ x) C.∘ C.id) ⟨$⟩ η1 ≈⟨ U.F-resp-≈ C.identityʳ ⟩ - U.₁ (f C.∘ x) ⟨$⟩ η1 ≈⟨ U.homomorphism ⟩ - U.₁ f ⟨$⟩ (U.₁ x ⟨$⟩ η1) ∎ + U.₁ ((f C.∘ x) C.∘ C.id) ⟨$⟩ η1 ≈⟨ U.F-resp-≈ (C.identityʳ CH.○ (CH.refl⟩∘⟨ x≈y)) Srefl ⟩ + U.₁ (f C.∘ y) ⟨$⟩ η1 ≈⟨ U.homomorphism Srefl ⟩ + U.₁ f ⟨$⟩ (U.₁ y ⟨$⟩ η1) ∎ } ; iso = λ X → record - { isoˡ = λ {x} → L.LRadjunct≈id {OneS} {X} {Const.function OneS (U.F₀ X) x} - ; isoʳ = λ { {1⇒x} → + { isoˡ = λ {x} {y} x≈y → Setoid.trans (U.₀ X) (L.LRadjunct≈id {OneS} {X} {Const.function OneS (U.F₀ X) x} tt) x≈y + ; isoʳ = λ {1⇒x} {1⇒y} x≈y → let open C.HomReasoning in begin - L.counit.η X C.∘ F.₁ (constF X (U.₁ 1⇒x ⟨$⟩ η1)) ≈⟨ refl⟩∘⟨ F.F-resp-≈ (cong (U.F₁ 1⇒x) (cong (L.unit.η OneS) _)) ⟩ - L.counit.η X C.∘ F.₁ (Comp.function (L.unit.η OneS) (U.₁ 1⇒x)) ≈⟨ L.RLadjunct≈id {OneS} {X} {1⇒x} ⟩ - 1⇒x ∎ } + L.counit.η X C.∘ F.₁ (constF X (U.₁ 1⇒x ⟨$⟩ η1)) ≈⟨ (refl⟩∘⟨ F.F-resp-≈ λ _ → U.F-resp-≈ x≈y Srefl) ⟩ + L.counit.η X C.∘ F.₁ (Comp.function (L.unit.η OneS) (U.₁ 1⇒y)) ≈⟨ L.RLadjunct≈id {OneS} {X} {1⇒y} ⟩ + 1⇒y ∎ } } } @@ -78,5 +78,6 @@ open Func open MR C η1 : Setoid.Carrier (U.₀ (F.₀ OneS)) η1 = L.unit.η OneS ⟨$⟩ tt + Srefl = Setoid.refl (U.₀ (F.₀ OneS)) constF : ∀ {ℓ} A → Setoid.Carrier (U.F₀ A) → Func (OneS {ℓ}) (U.F₀ A) constF A = Const.function OneS (U.F₀ A) diff --git a/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda b/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda index a8c69cd4f..11194b8e5 100644 --- a/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda +++ b/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda @@ -30,9 +30,9 @@ module _ {o′ ℓ′ o″ ℓ″} where { to = λ { (a , b) → A.₁ f ⟨$⟩ a , B.₁ f ⟨$⟩ b } ; cong = λ { (eq₁ , eq₂) → Func.cong (A.₁ f) eq₁ , Func.cong (B.₁ f) eq₂ } } - ; identity = A.identity , B.identity - ; homomorphism = A.homomorphism , B.homomorphism - ; F-resp-≈ = λ eq → A.F-resp-≈ eq , B.F-resp-≈ eq + ; identity = λ { (eq₁ , eq₂) → A.identity eq₁ , B.identity eq₂ } + ; homomorphism = λ { (eq₁ , eq₂) → A.homomorphism eq₁ , B.homomorphism eq₂ } + ; F-resp-≈ = λ { eq (eq₁ , eq₂) → A.F-resp-≈ eq eq₁ , B.F-resp-≈ eq eq₂ } } where module A = Functor A module B = Functor B @@ -73,14 +73,14 @@ module IsCartesian o′ ℓ′ where { to = λ { (fst , _) → fst } ; cong = λ { (eq , _) → eq } } - ; commute = λ f → cong (A.F₁ f) (Setoid.refl (A.F₀ _)) + ; commute = λ { f (eq , _) → cong (A.F₁ f) eq } } ; π₂ = ntHelper record { η = λ X → record { to = λ { (_ , snd) → snd } ; cong = λ { (_ , eq) → eq } } - ; commute = λ f → cong (B.F₁ f) (Setoid.refl (B.F₀ _)) + ; commute = λ { f (_ , eq) → cong (B.F₁ f) eq } } ; ⟨_,_⟩ = λ {F} α β → let module F = Functor F @@ -91,16 +91,18 @@ module IsCartesian o′ ℓ′ where { to = λ S → α.η Y ⟨$⟩ S , β.η Y ⟨$⟩ S ; cong = λ eq → cong (α.η Y) eq , cong (β.η Y) eq } - ; commute = λ f → α.commute f , β.commute f + ; commute = λ f eq → α.commute f eq , β.commute f eq } - ; project₁ = λ {F α β x} → + ; project₁ = λ {F α β x} eq → let module α = NaturalTransformation α - in cong (α.η x) (Setoid.refl (Functor.₀ F _)) - ; project₂ = λ {F α β x} → + in Func.cong (α.η x) eq + ; project₂ = λ {F α β x} eq → let module β = NaturalTransformation β - in cong (β.η x) (Setoid.refl (Functor.₀ F _)) - ; unique = λ {F α β δ} eq₁ eq₂ {x} → - Setoid.sym (A.₀ x) (eq₁ {x}) , Setoid.sym (B.₀ x) (eq₂ {x}) + in cong (β.η x) eq + ; unique = λ {F α β δ} eq₁ eq₂ {x} eq → + let module F = Functor F + in Setoid.sym (A.₀ x) (eq₁ (Setoid.sym (F.₀ x) eq)) + , Setoid.sym (B.₀ x) (eq₂ (Setoid.sym (F.₀ x) eq)) } } } diff --git a/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda b/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda index 2ccd13b4c..798b220da 100644 --- a/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda +++ b/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda @@ -49,22 +49,19 @@ module HasClosed {o ℓ e} (C : Category o ℓ e) where { to = λ where (g , S) → α.η X ⟨$⟩ (f ∘ g , S) ; cong = λ where (eq₁ , eq₂) → cong (α.η X) (∘-resp-≈ʳ eq₁ , eq₂) } - ; commute = λ { {Z} {W} g {h , x} → + ; commute = λ { {Z} {W} g {h , x} {i , y} (eq₁ , eq₂) → let open SetoidR (F.₀ W) in begin α.η W ⟨$⟩ (f ∘ C.id ∘ h ∘ g , G.₁ g ⟨$⟩ x) ≈⟨ cong (α.η W) (Equiv.trans (pullˡ id-comm) (center Equiv.refl) , Setoid.refl (G.₀ W)) ⟩ - α.η W ⟨$⟩ (C.id ∘ (f ∘ h) ∘ g , G.₁ g ⟨$⟩ x) ≈⟨ α.commute g ⟩ - F.₁ g ⟨$⟩ (α.η Z ⟨$⟩ (f ∘ h , x)) ∎ } + α.η W ⟨$⟩ (C.id ∘ (f ∘ h) ∘ g , G.₁ g ⟨$⟩ x) ≈⟨ α.commute g (∘-resp-≈ʳ eq₁ , eq₂) ⟩ + F.₁ g ⟨$⟩ (α.η Z ⟨$⟩ (f ∘ i , y)) ∎ } } - ; cong = λ eq → eq + ; cong = λ eq (eq₁ , eq₂) → eq (∘-resp-≈ʳ eq₁ , eq₂) } - ; identity = λ {A} {α} {x} → cong (η α x) (identityˡ , Setoid.refl (G.F₀ x)) - ; homomorphism = λ {_} {_} {_} {f} {g} {α} {A} → cong (η α _) (assoc , Setoid.refl (G.F₀ _)) - ; F-resp-≈ = λ eq {α} {A} {x} → cong (η α _) (∘-resp-≈ˡ eq , Setoid.refl (G.F₀ _)) - } - where - open MR C - open NaturalTransformation + ; identity = λ eq (eq₁ , eq₂) → eq (Equiv.trans identityˡ eq₁ , eq₂) + ; homomorphism = λ eq (eq₁ , eq₂) → eq (pullʳ (∘-resp-≈ʳ eq₁) , eq₂) + ; F-resp-≈ = λ where eq eq′ (eq₁ , eq₂) → eq′ (∘-resp-≈ eq eq₁ , eq₂) + } where open MR C module IsCartesianClosed {o} (C : Category o o o) where private @@ -95,22 +92,16 @@ module IsCartesianClosed {o} (C : Category o o o) where { to = λ { (α , x) → let module α = NaturalTransformation α in α.η X ⟨$⟩ (C.id , x) } - ; cong = λ { {α₁ , f₁} {α₂ , f₂} (eq₁ , eq₂) → - let module SR = SetoidR (F.F₀ X) in - let open SR - open NaturalTransformation - in begin - to (η α₁ X) (C.id , f₁) ≈⟨ eq₁ ⟩ - to (η α₂ X) (C.id , f₁) ≈⟨ cong (η α₂ X) (C.Equiv.refl , eq₂) ⟩ - to (η α₂ X) (C.id , f₂) ∎ } + ; cong = λ where (eq₁ , eq₂) → eq₁ (C.Equiv.refl , eq₂) } - ; commute = λ { {Y} {Z} f {α , x} → + ; commute = λ { {Y} {Z} f {α , x} {β , y} (eq₁ , eq₂) → let module α = NaturalTransformation α + module β = NaturalTransformation β open SetoidR (F.₀ Z) in begin - α.η Z ⟨$⟩ (f C.∘ C.id , G.₁ f ⟨$⟩ x) ≈⟨ cong (α.η Z) (C.Equiv.trans id-comm (C.Equiv.sym C.identityˡ) , Setoid.refl (G.F₀ Z)) ⟩ - α.η Z ⟨$⟩ (C.id C.∘ C.id C.∘ f , G.₁ f ⟨$⟩ x) ≈⟨ α.commute f ⟩ - F.₁ f ⟨$⟩ (α.η Y ⟨$⟩ (C.id , x)) ∎ } + α.η Z ⟨$⟩ (f C.∘ C.id , G.₁ f ⟨$⟩ x) ≈⟨ eq₁ ((C.Equiv.trans id-comm (C.Equiv.sym C.identityˡ)) , Setoid.refl (G.₀ Z)) ⟩ + β.η Z ⟨$⟩ (C.id C.∘ C.id C.∘ f , G.₁ f ⟨$⟩ x) ≈⟨ β.commute f (C.Equiv.refl , eq₂) ⟩ + F.₁ f ⟨$⟩ (β.η Y ⟨$⟩ (C.id , y)) ∎ } } ; curry = λ {F G H} α → let module F = Functor F @@ -122,44 +113,54 @@ module IsCartesianClosed {o} (C : Category o o o) where { to = λ x → ntHelper record { η = λ Y → record { to = λ where (f , y) → α.η Y ⟨$⟩ (F.₁ f ⟨$⟩ x , y) - ; cong = λ {(eq₁ , eq₂) → cong (α.η Y) ((F.F-resp-≈ eq₁) , eq₂) } + ; cong = λ where (eq₁ , eq₂) → cong (α.η _) (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ _)) , eq₂) } - ; commute = λ { {Y} {Z} f {g , y} → + ; commute = λ { {Y} {Z} f {g , y} {h , z} (eq₁ , eq₂) → let open SetoidR (H.₀ Z) open Setoid (G.₀ Z) in begin α.η Z ⟨$⟩ (F.F₁ (C.id C.∘ g C.∘ f) ⟨$⟩ x , G.F₁ f ⟨$⟩ y) - ≈⟨ cong (α.η Z) (F.F-resp-≈ C.identityˡ , refl) ⟩ + ≈⟨ cong (α.η Z) (F.F-resp-≈ C.identityˡ (Setoid.refl (F.₀ X)) , refl) ⟩ α.η Z ⟨$⟩ (F.F₁ (g C.∘ f) ⟨$⟩ x , G.F₁ f ⟨$⟩ y) - ≈⟨ cong (α.η Z) (F.homomorphism , refl) ⟩ + ≈⟨ cong (α.η Z) (F.homomorphism (Setoid.refl (F.₀ X)) , refl) ⟩ α.η Z ⟨$⟩ (F.F₁ f ⟨$⟩ (F.F₁ g ⟨$⟩ x) , G.F₁ f ⟨$⟩ y) - ≈⟨ α.commute f ⟩ - H.F₁ f ⟨$⟩ (α.η Y ⟨$⟩ (F.F₁ g ⟨$⟩ x , y)) + ≈⟨ α.commute f (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ X)) , eq₂) ⟩ + H.F₁ f ⟨$⟩ (α.η Y ⟨$⟩ (F.F₁ h ⟨$⟩ x , z)) ∎ } } - ; cong = λ eq → cong (α.η _) ((cong (F.F₁ _) eq) , (Setoid.refl (G.F₀ _))) + ; cong = λ where eq (eq₁ , eq₂) → cong (α.η _) (F.F-resp-≈ eq₁ eq , eq₂) } - ; commute = λ { {X} {Y} f {x} {A} {g , z} → - let open Setoid (F.₀ A) in - cong (NaturalTransformation.η α A) (sym (F.homomorphism) , Setoid.refl (G.F₀ A)) } + ; commute = λ { {X} {Y} f {x} {y} eq {Z} {g , z} {h , w} (eq₁ , eq₂) → + let open SetoidR (F.₀ Z) + helper : g C.≈ h → Setoid._≈_ (F.₀ X) x y → + Setoid._≈_ (F.₀ Z) (F.₁ g ⟨$⟩ (F.₁ f ⟨$⟩ x)) (F.₁ (f C.∘ h) ⟨$⟩ y) + helper eq eq′ = begin + F.₁ g ⟨$⟩ (F.₁ f ⟨$⟩ x) ≈⟨ F.F-resp-≈ eq (Setoid.refl (F.₀ Y)) ⟩ + F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ x) ≈˘⟨ F.homomorphism (Setoid.sym (F.₀ X) eq′) ⟩ + F.₁ (f C.∘ h) ⟨$⟩ y ∎ + in cong (α.η _) (helper eq₁ eq , eq₂) } } - ; eval-comp = λ {F G H} {α} → + ; eval-comp = λ {F G H} {α} → λ { (eq₁ , eq₂) → let module H = Functor H module α = NaturalTransformation α - in cong (α.η _) (H.identity , (Setoid.refl (Functor.F₀ G _))) - ; curry-unique = λ {F G H} {α β} eq {X} {x y} → λ { {f , z} → + in cong (α.η _) (H.identity eq₁ , eq₂) } + ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ → λ { {Y} {f , z} {g , w} (eq₂ , eq₃) → let module F = Functor F module G = Functor G + module H = Functor H module α = NaturalTransformation α module β = NaturalTransformation β module αXx = NaturalTransformation (α.η X ⟨$⟩ x) - open Setoid (Functor.₀ H y) - open SetoidR (G.₀ y) + open Setoid (H.₀ Y) + open SetoidR (G.₀ Y) in begin - αXx.η y ⟨$⟩ (f , z) ≈⟨ cong (αXx.η _) (C.Equiv.sym C.identityʳ , refl) ⟩ - αXx.η y ⟨$⟩ (f C.∘ C.id , z) ≈⟨ α.sym-commute f ⟩ - NaturalTransformation.η (α.η y ⟨$⟩ (F.F₁ f ⟨$⟩ x)) y ⟨$⟩ (C.id , z) ≈⟨ eq ⟩ - β.η y ⟨$⟩ (F.F₁ f ⟨$⟩ x , z) + αXx.η Y ⟨$⟩ (f , z) + ≈⟨ cong (αXx.η _) (C.Equiv.sym C.identityʳ , refl) ⟩ + αXx.η Y ⟨$⟩ (f C.∘ C.id , z) + ≈⟨ α.sym-commute f (Setoid.refl (F.₀ X)) (C.Equiv.refl , refl) ⟩ + NaturalTransformation.η (α.η Y ⟨$⟩ (F.F₁ f ⟨$⟩ x)) Y ⟨$⟩ (C.id , z) + ≈⟨ eq (F.F-resp-≈ eq₂ eq₁ , eq₃) ⟩ + β.η Y ⟨$⟩ (F.F₁ g ⟨$⟩ y , w) ∎ } } where diff --git a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda index fbc127f04..7bbf189c1 100644 --- a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda +++ b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda @@ -22,7 +22,6 @@ open import Categories.Functor.Hom using (Hom[_][_,_]) open import Categories.Functor.Properties using ([_]-resp-∘; [_]-resp-square) open import Categories.Functor.Presheaf using (Presheaf) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Categories.Object.Product.Core using (Product) -- elide open import Categories.Object.Terminal using (Terminal) import Categories.Category.Construction.Properties.Presheaves.Cartesian as Preₚ @@ -42,19 +41,19 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi Pres-exp F X = record { F₀ = λ Y → F.₀ (X × Y) ; F₁ = λ f → F.₁ (second f) - ; identity = λ {A} {x} → + ; identity = λ {A} {x y} eq → let open Setoid (F.₀ (X × A)) open SetoidR (F.₀ (X × A)) in begin - F.₁ (second C.id) ⟨$⟩ x ≈⟨ F.F-resp-≈ (id×id (product {X} {A})) ⟩ - F.F₁ C.id ⟨$⟩ x ≈⟨ F.identity ⟩ - x ∎ - ; homomorphism = λ {Y Z W} {f} {g} {x} → + F.₁ (second C.id) ⟨$⟩ x ≈⟨ F.F-resp-≈ (id×id (product {X} {A})) refl ⟩ + F.F₁ C.id ⟨$⟩ x ≈⟨ F.identity eq ⟩ + y ∎ + ; homomorphism = λ {Y Z W} {f} {g} {x y} eq → let open Setoid (F.₀ (X × Y)) open SetoidR (F.₀ (X × W)) in begin - F.₁ (second (f C.∘ g)) ⟨$⟩ x ≈˘⟨ [ F ]-resp-∘ second∘second ⟩ - F.₁ (second g) ⟨$⟩ (F.₁ (second f) ⟨$⟩ x) ∎ + F.₁ (second (f C.∘ g)) ⟨$⟩ x ≈˘⟨ [ F ]-resp-∘ second∘second (sym eq) ⟩ + F.₁ (second g) ⟨$⟩ (F.₁ (second f) ⟨$⟩ y) ∎ ; F-resp-≈ = λ {Y Z} {f g} eq → F.F-resp-≈ (⁂-cong₂ C.Equiv.refl eq) } where module F = Functor F @@ -64,21 +63,22 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi { F₀ = Pres-exp F ; F₁ = λ f → ntHelper record { η = λ X → F₁ (first f) - ; commute = λ g → [ F ]-resp-square (C.Equiv.sym first↔second) + ; commute = λ g eq → + [ F ]-resp-square (C.Equiv.sym first↔second) eq } - ; identity = λ {A B} {x} → + ; identity = λ {A B} {x y} eq → let open Setoid (F₀ (A × B)) open SetoidR (F₀ (A × B)) in begin - F₁ (first C.id) ⟨$⟩ x ≈⟨ F-resp-≈ (id×id product) ⟩ - F₁ C.id ⟨$⟩ x ≈⟨ identity ⟩ - x ∎ - ; homomorphism = λ {X Y Z} {f g} {W} {x} → + F₁ (first C.id) ⟨$⟩ x ≈⟨ F-resp-≈ (id×id product) eq ⟩ + F₁ C.id ⟨$⟩ y ≈⟨ identity refl ⟩ + y ∎ + ; homomorphism = λ {X Y Z} {f g} {W} {x y} eq → let open Setoid (F₀ (X × W)) open SetoidR (F₀ (Z × W)) in begin - F₁ (first (f C.∘ g)) ⟨$⟩ x ≈˘⟨ [ F ]-resp-∘ first∘first ⟩ - F₁ (first g) ⟨$⟩ (F₁ (first f) ⟨$⟩ x) ∎ + F₁ (first (f C.∘ g)) ⟨$⟩ x ≈˘⟨ [ F ]-resp-∘ first∘first (sym eq) ⟩ + F₁ (first g) ⟨$⟩ (F₁ (first f) ⟨$⟩ y) ∎ ; F-resp-≈ = λ {A B} {f g} eq → F-resp-≈ (⁂-cong₂ eq C.Equiv.refl) } where open Functor F @@ -96,24 +96,27 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi let module α = NaturalTransformation α in ntHelper record { η = λ X → F.₁ (first f) ∙ α.η X - ; commute = λ {X Y} g {x} → + ; commute = λ {X Y} g {x y} eq → let open SetoidR (F.₀ (B × Y)) in begin - F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ g ⟨$⟩ x)) ≈⟨ Func.cong (F.₁ (first f)) (α.commute g) ⟩ - F.₁ (first f) ⟨$⟩ (F.₁ (second g) ⟨$⟩ (α.η X ⟨$⟩ x)) ≈˘⟨ [ F ]-resp-square first↔second ⟩ - F.₁ (second g) ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η X ⟨$⟩ x)) ∎ + F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ g ⟨$⟩ x)) ≈⟨ Func.cong (F.₁ (first f)) (α.commute g eq) ⟩ + F.₁ (first f) ⟨$⟩ (F.₁ (second g) ⟨$⟩ (α.η X ⟨$⟩ y)) ≈˘⟨ [ F ]-resp-square first↔second (Setoid.refl (F.₀ (A × X))) ⟩ + F.₁ (second g) ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η X ⟨$⟩ y)) ∎ } - ; cong = λ {α} {β} eq → Func.cong (F.₁ (first f)) eq + ; cong = λ eq eq′ → Func.cong (F.₁ (first f)) (eq eq′) } - ; identity = λ {X} {α} {Y} {x} → + ; identity = λ {X} {α β} eq {Y} {x y} eq′ → let module α = NaturalTransformation α + module β = NaturalTransformation β open SetoidR (F.₀ (X × Y)) in begin - F.₁ (first C.id) ⟨$⟩ (α.η Y ⟨$⟩ x) ≈⟨ F.F-resp-≈ (id×id product) ⟩ - F.₁ C.id ⟨$⟩ (α.η Y ⟨$⟩ x) ≈⟨ F.identity ⟩ - α.η Y ⟨$⟩ x ∎ - ; homomorphism = λ {X Y Z} → Setoid.sym (F.₀ (Z × _)) ([ F ]-resp-∘ first∘first) - ; F-resp-≈ = λ eq → F.F-resp-≈ (⁂-cong₂ eq C.Equiv.refl) + F.₁ (first C.id) ⟨$⟩ (α.η Y ⟨$⟩ x) ≈⟨ F.F-resp-≈ (id×id product) (eq eq′) ⟩ + F.₁ C.id ⟨$⟩ (β.η Y ⟨$⟩ y) ≈⟨ F.identity (Setoid.refl (F.₀ (X × Y))) ⟩ + β.η Y ⟨$⟩ y ∎ + ; homomorphism = λ {X Y Z} eq {W} eq′ → + let open Setoid (F.₀ (X × W)) + in Setoid.sym (F.₀ (Z × W)) ([ F ]-resp-∘ first∘first (sym (eq eq′))) + ; F-resp-≈ = λ eq eq′ eq″ → F.F-resp-≈ (⁂-cong₂ eq C.Equiv.refl) (eq′ eq″) } module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where @@ -122,7 +125,7 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where module CH = C.HomReasoning P = Presheaves′ o o C open BinaryProducts (Cartesian.products Car) using (_×_; π₁; π₂; ⟨_,_⟩; Δ; first; second; _⁂_; Δ∘; ⁂∘Δ; second∘first; - π₁∘⁂; π₂∘⁂; project₁; project₂; η; product) + π₁∘⁂; π₂∘⁂; project₁; project₂; η) open Preₚ.IsCartesian C o o using () renaming (Presheaves-Cartesian to PC) module PPC = BinaryProducts PC.products using (π₁; π₂; _×_; project₁; project₂; ⟨_,_⟩; unique) module TPC = Terminal PC.terminal using (⊤; !; !-unique) @@ -149,22 +152,19 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where { to = λ { (α , x) → let module α = NaturalTransformation α using (η) in F.₁ Δ ⟨$⟩ (α.η X ⟨$⟩ x) } - ; cong = λ { {α , gx} {β , gx′} (eq , eq′) → cong (F.₁ Δ) ( - Setoid.trans (Functor.F₀ F (Product.A×B product)) - eq - (cong (NaturalTransformation.η β X) eq′) - )} + ; cong = λ { (eq , eq′) → cong (F.₁ Δ) (eq eq′) } } - ; commute = λ {X Y} f → λ { {α , x} → + ; commute = λ {X Y} f → λ { {α , x} {β , y} (eq , eq′) → let module α = NaturalTransformation α using (η; commute) + module β = NaturalTransformation β using (η) open Setoid (F.₀ (X × X)) using (sym; refl) open SetoidR (F.₀ Y) in begin - F.₁ Δ ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ f ⟨$⟩ x))) ≈⟨ cong (F.₁ Δ ∙ F.₁ (first f)) (α.commute f) ⟩ - F.₁ Δ ∙ (F.₁ (first f) ∙ F.₁ (second f)) ⟨$⟩ (α.η X ⟨$⟩ x) ≈⟨ cong (F.₁ Δ) ([ F ]-resp-∘ second∘first) ⟩ - F.₁ Δ ⟨$⟩ (F.₁ (f ⁂ f) ⟨$⟩ (α.η X ⟨$⟩ x)) ≈⟨ [ F ]-resp-∘ ⁂∘Δ ⟩ - F.₁ ⟨ f , f ⟩ ⟨$⟩ (α.η X ⟨$⟩ x) ≈˘⟨ [ F ]-resp-∘ Δ∘ ⟩ - F.₁ f ⟨$⟩ (F.₁ Δ ⟨$⟩ (α.η X ⟨$⟩ x)) + F.₁ Δ ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ f ⟨$⟩ x))) ≈⟨ cong (F.₁ Δ ∙ F.₁ (first f)) (α.commute f eq′) ⟩ + F.₁ Δ ∙ (F.₁ (first f) ∙ F.₁ (second f)) ⟨$⟩ (α.η X ⟨$⟩ y) ≈⟨ cong (F.₁ Δ) ([ F ]-resp-∘ second∘first refl) ⟩ + F.₁ Δ ⟨$⟩ (F.₁ (f ⁂ f) ⟨$⟩ (α.η X ⟨$⟩ y)) ≈⟨ [ F ]-resp-∘ ⁂∘Δ refl ⟩ + F.₁ ⟨ f , f ⟩ ⟨$⟩ (α.η X ⟨$⟩ y) ≈˘⟨ [ F ]-resp-∘ Δ∘ (sym (eq (Setoid.refl (G.₀ X)))) ⟩ + F.₁ f ⟨$⟩ (F.₁ Δ ⟨$⟩ (β.η X ⟨$⟩ y)) ∎ } } ; curry = λ {F G H} α → @@ -179,28 +179,31 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where { to = λ y → α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ y) ; cong = λ eq → cong (α.η (X × Y)) (Setoid.refl (F.₀ (X × Y)) , cong (G.₁ π₂) eq) } - ; commute = λ {Y Z} f {y} → + ; commute = λ {Y Z} f {y z} eq → let open SetoidR (H.₀ (X × Z)) in begin α.η (X × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ (G.₁ f ⟨$⟩ y)) - ≈˘⟨ cong (α.η (X × Z)) ( [ F ]-resp-∘ (π₁∘⁂ CH.○ C.identityˡ) - , [ G ]-resp-square π₂∘⁂) ⟩ + ≈˘⟨ cong (α.η (X × Z)) ( [ F ]-resp-∘ (π₁∘⁂ CH.○ C.identityˡ) (Setoid.refl (F.₀ X)) + , [ G ]-resp-square π₂∘⁂ (Setoid.refl (G.₀ Y))) ⟩ α.η (X × Z) ⟨$⟩ (F.₁ (second f) ∙ F.₁ π₁ ⟨$⟩ x , G.₁ (second f) ⟨$⟩ (G.₁ π₂ ⟨$⟩ y)) - ≈⟨ α.commute (second f) ⟩ - H.₁ (second f) ⟨$⟩ (α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ y)) + ≈⟨ α.commute (second f) (Setoid.refl (F.₀ (X × Y)) , cong (G.₁ π₂) eq) ⟩ + H.₁ (second f) ⟨$⟩ (α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ z)) ∎ } - ; cong = λ eq → cong (α.η _) ((cong (F.F₁ π₁) eq) , cong (G.₁ π₂) (Setoid.refl (G.F₀ _))) + ; cong = λ eq₁ eq₂ → cong (α.η _) (cong (F.F₁ π₁) eq₁ , cong (G.₁ π₂) eq₂) } - ; commute = λ {X Y} f {FX Z} {GZ} → - let open SetoidR (H.₀ (Y × Z)) in begin - α.η (Y × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ (F.₁ f ⟨$⟩ FX) , G.₁ π₂ ⟨$⟩ GZ) - ≈˘⟨ cong (α.η _) (([ F ]-resp-square π₁∘⁂) , ([ G ]-resp-∘ (π₂∘⁂ CH.○ C.identityˡ))) ⟩ - α.η (Y × Z) ⟨$⟩ (F.₁ (first f) ⟨$⟩ (F.₁ π₁ ⟨$⟩ FX) , G.₁ (first f) ⟨$⟩ (G.₁ π₂ ⟨$⟩ GZ)) - ≈⟨ α.commute (first f) ⟩ - H.₁ (first f) ⟨$⟩ (α.η (X × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ FX , G.₁ π₂ ⟨$⟩ GZ)) ∎ + ; commute = λ {X Y} f {x y} eq₁ {Z} {z w} eq₂ → + let open SetoidR (H.₀ (Y × Z)) + in begin + α.η (Y × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ (F.₁ f ⟨$⟩ x) , G.₁ π₂ ⟨$⟩ z) + ≈˘⟨ cong (α.η _) ( [ F ]-resp-square π₁∘⁂ (Setoid.refl (F.₀ X)) + , [ G ]-resp-∘ (π₂∘⁂ CH.○ C.identityˡ) (Setoid.refl (G.₀ Z))) ⟩ + α.η (Y × Z) ⟨$⟩ (F.₁ (first f) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x) , G.₁ (first f) ⟨$⟩ (G.₁ π₂ ⟨$⟩ z)) + ≈⟨ α.commute (first f) (cong (F.₁ π₁) eq₁ , cong (G.₁ π₂) eq₂) ⟩ + H.₁ (first f) ⟨$⟩ (α.η (X × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ y , G.₁ π₂ ⟨$⟩ w)) + ∎ } - ; eval-comp = λ {F G H} {α} → λ { {X} {x , y} → + ; eval-comp = λ {F G H} {α} → λ { {X} {x , y} {z , w} (eq₁ , eq₂) → let module F = Functor F module G = Functor G module H = Functor H @@ -210,14 +213,14 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where open SetoidR (F.₀ X) in begin F.₁ Δ ⟨$⟩ (α.η (X × X) ⟨$⟩ (H.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ y)) - ≈⟨ α.sym-commute Δ ⟩ - α.η X ⟨$⟩ (H.₁ Δ ⟨$⟩ (H.F₁ π₁ ⟨$⟩ x) , G.₁ Δ ⟨$⟩ (G.₁ π₂ ⟨$⟩ y)) - ≈⟨ cong (α.η X) ([ H ]-resp-∘ project₁ , [ G ]-resp-∘ project₂) ⟩ - α.η X ⟨$⟩ (H.F₁ C.id ⟨$⟩ x , G.F₁ C.id ⟨$⟩ y) - ≈⟨ cong (α.η X) (H.identity , G.identity) ⟩ - α.η X ⟨$⟩ (x , y) + ≈⟨ α.sym-commute Δ (cong (H.₁ π₁) eq₁ , cong (G.₁ π₂) eq₂) ⟩ + α.η X ⟨$⟩ (H.₁ Δ ⟨$⟩ (H.F₁ π₁ ⟨$⟩ z) , G.₁ Δ ⟨$⟩ (G.₁ π₂ ⟨$⟩ w)) + ≈⟨ cong (α.η X) ([ H ]-resp-∘ project₁ HX.refl , [ G ]-resp-∘ project₂ GX.refl) ⟩ + α.η X ⟨$⟩ (H.F₁ C.id ⟨$⟩ z , G.F₁ C.id ⟨$⟩ w) + ≈⟨ cong (α.η X) (H.identity HX.refl , G.identity GX.refl) ⟩ + α.η X ⟨$⟩ (z , w) ∎ } - ; curry-unique = λ {F G H} {α β} eq {X} {x} {Y} {z} → + ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ {Y} {z w} eq₂ → let module F = Functor F module G = Functor G module H = Functor H @@ -228,18 +231,18 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where open SetoidR (G.₀ (X × Y)) in begin αXx.η Y ⟨$⟩ z - ≈˘⟨ G.identity ⟩ + ≈˘⟨ G.identity GXY.refl ⟩ G.₁ C.id ⟨$⟩ (αXx.η Y ⟨$⟩ z) - ≈˘⟨ [ G ]-resp-∘ (⁂∘Δ CH.○ η) ⟩ + ≈˘⟨ [ G ]-resp-∘ (⁂∘Δ CH.○ η) GXY.refl ⟩ G.₁ Δ ⟨$⟩ (G.F₁ (π₁ ⁂ π₂) ⟨$⟩ (αXx.η Y ⟨$⟩ z)) - ≈˘⟨ cong (G.₁ Δ) ([ G ]-resp-∘ second∘first) ⟩ + ≈˘⟨ cong (G.₁ Δ) ([ G ]-resp-∘ second∘first GXY.refl) ⟩ G.₁ Δ ⟨$⟩ (G.₁ (first π₁) ⟨$⟩ (G.₁ (second π₂) ⟨$⟩ (αXx.η Y ⟨$⟩ z))) - ≈⟨ cong (G.₁ Δ ∙ G.₁ (first π₁)) (αXx.sym-commute π₂) ⟩ + ≈⟨ cong (G.₁ Δ ∙ G.₁ (first π₁)) (αXx.sym-commute π₂ (Setoid.refl (H.₀ Y))) ⟩ G.₁ Δ ⟨$⟩ (G.₁ (first π₁) ⟨$⟩ (αXx.η (X × Y) ⟨$⟩ (H.₁ π₂ ⟨$⟩ z))) - ≈⟨ cong (G.₁ Δ) (α.sym-commute π₁) ⟩ + ≈⟨ cong (G.₁ Δ) (α.sym-commute π₁ (Setoid.refl (F.₀ X)) (Setoid.refl (H.₀ (X × Y)))) ⟩ G.₁ Δ ⟨$⟩ (NaturalTransformation.η (α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x)) (X × Y) ⟨$⟩ (H.₁ π₂ ⟨$⟩ z)) - ≈⟨ eq ⟩ - β.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , H.₁ π₂ ⟨$⟩ z) + ≈⟨ eq (cong (F.₁ π₁) eq₁ , cong (H.₁ π₂) eq₂) ⟩ + β.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ y , H.₁ π₂ ⟨$⟩ w) ∎ } diff --git a/src/Categories/Category/Instance/FamilyOfSetoids.agda b/src/Categories/Category/Instance/FamilyOfSetoids.agda index db4021dd1..fd0a41dc6 100644 --- a/src/Categories/Category/Instance/FamilyOfSetoids.agda +++ b/src/Categories/Category/Instance/FamilyOfSetoids.agda @@ -12,7 +12,7 @@ open import Function.Base renaming (id to idf; _∘_ to _⊚_) open import Function.Bundles using (Func; _⟨$⟩_) open import Function.Construct.Identity using () renaming (function to idF) open import Function.Construct.Composition using (function) -open import Function.Construct.Setoid using (_∙_) renaming (setoid to _⇨_) +open import Function.Construct.Setoid using (_∙_) renaming (function to _⇨_) open import Function.Structures using (IsInverse) open import Relation.Binary using (Rel; Setoid; module Setoid; Reflexive; Symmetric; Transitive) @@ -66,14 +66,14 @@ module _ {a b c d : Level} where {bx : Setoid.Carrier C} → Setoid._≈_ D ((reindex Y g≈f ∙ transport F′ x) ⟨$⟩ bx) (transport F x ⟨$⟩ bx) fam-id : {A : Fam} → Hom A A - fam-id {A} = fhom (idF (U A)) (λ x → idF (T A x)) λ p → Setoid.refl (T A _) + fam-id {A} = fhom (idF (U A)) (λ x → idF (T A x)) λ p x≈y → cong (reindex A p) x≈y comp : {A B C : Fam} → Hom B C → Hom A B → Hom A C comp {B = B} {C} (fhom map₀ trans₀ coh₀) (fhom map₁ trans₁ coh₁) = fhom (map₀ ∙ map₁) (λ x → trans₀ (map₁ ⟨$⟩ x) ∙ (trans₁ x)) - λ {a} {b} p {x} → + λ {a} {b} p {x} {y} x≈y → let open Setoid (T C (map₀ ∙ map₁ ⟨$⟩ a)) renaming (trans to _⟨≈⟩_) in - cong (trans₀ (map₁ ⟨$⟩ a)) (coh₁ p) ⟨≈⟩ - coh₀ (cong map₁ p) + cong (trans₀ (map₁ ⟨$⟩ a)) (coh₁ p x≈y) ⟨≈⟩ + coh₀ (cong map₁ p) (Setoid.refl (T B (map₁ ⟨$⟩ b))) ≈≈-refl : ∀ {A B} → Reflexive (_≈≈_ {A} {B}) ≈≈-refl {B = B} = feq refl (reindex-refl B) @@ -104,7 +104,7 @@ module _ {a b c d : Level} where λ {x} → let open Setoid (T C (map (comp f g) ⟨$⟩ x)) renaming (trans to _⟨≈⟩_; sym to ≈sym) in reindex-trans C (cong (map f) g≈i) f≈h ⟨≈⟩ (cong (reindex C (cong (map f) g≈i)) t-f≈h ⟨≈⟩ - (≈sym (transport-coh {B} {C} f g≈i) ⟨≈⟩ + (≈sym (transport-coh {B} {C} f g≈i (Setoid.refl (T B (map i ⟨$⟩ x)))) ⟨≈⟩ cong (transport f (map g ⟨$⟩ x)) t-g≈i)) where open _≈≈_ diff --git a/src/Categories/Category/Instance/Properties/Setoids/CCC.agda b/src/Categories/Category/Instance/Properties/Setoids/CCC.agda index d5cae8c5c..e59fddd75 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/CCC.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/CCC.agda @@ -5,7 +5,7 @@ module Categories.Category.Instance.Properties.Setoids.CCC where open import Level open import Data.Product using (Σ ; _,_) open import Function.Bundles using (Func; _⟨$⟩_) -open import Function.Construct.Setoid using (setoid) +open import Function.Construct.Setoid using (function) open import Relation.Binary using (Setoid) open import Categories.Category.Core using (Category) @@ -33,22 +33,20 @@ module _ ℓ where ; π₁-comp = λ {_ _ f _ g} → project₁ {h = f} {g} ; π₂-comp = λ {_ _ f _ g} → project₂ {h = f} {g} ; ⟨,⟩-unique = λ {_ _ _ f g h} → unique {h = h} {f} {g} - ; _^_ = λ X Y → setoid Y X - ; eval = λ {X Y} → - let module X = Setoid X in record + ; _^_ = λ X Y → function Y X + ; eval = λ {X Y} → record { to = λ { (f , x) → f ⟨$⟩ x } - ; cong = λ { {( f₁ , x₁)} {(f₂ , x₂)} (eq₁ , eq₂) → - X.trans (eq₁ {x₁}) (Func.cong f₂ eq₂)} + ; cong = λ { (eq₁ , eq₂) → eq₁ eq₂ } } ; curry = λ {C A B} f → record { to = λ c → record { to = λ a → f ⟨$⟩ (c , a) ; cong = λ eq → Func.cong f (Setoid.refl C , eq) } - ; cong = λ eq₁ → Func.cong f (eq₁ , (Setoid.refl A)) + ; cong = λ eq₁ eq₂ → Func.cong f (eq₁ , eq₂) } - ; eval-comp = λ {C A B f} → Func.cong f (Setoid.refl B , Setoid.refl A) - ; curry-unique = λ eq → eq + ; eval-comp = λ {_ _ _ f} → Func.cong f + ; curry-unique = λ eq₁ eq₂ eq → eq₁ (eq₂ , eq) } where open Setoids-Cartesian diff --git a/src/Categories/Category/Instance/Properties/Setoids/Choice.agda b/src/Categories/Category/Instance/Properties/Setoids/Choice.agda index 9417ef5e1..f28432145 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Choice.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Choice.agda @@ -12,7 +12,7 @@ open import Data.Nat.Base using (ℕ) open import Data.Product using (∃; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_; map; zip; swap; map₂) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Function.Bundles using (Func; _⟨$⟩_) -open import Function.Construct.Setoid using () renaming (setoid to _⇨_) +open import Function.Construct.Setoid using () renaming (function to _⇨_) open import Level using (Level; Lift) open import Relation.Binary using (Setoid; Rel; REL; IsEquivalence) import Relation.Binary.PropositionalEquality.Core as P @@ -50,7 +50,7 @@ module _ ℓ where { to = λ y → let x , _ = surj y in x ; cong = λ {x}{y} x≡y → P.subst (λ z → [ X ][ proj₁ (surj x) ≈ proj₁ (surj z) ]) x≡y (refl X) } - , λ {x} → proj₂ (surj x) + , λ {x}{y} x≡y → let z , eq = surj x in P.trans eq x≡y } entire : {A B : Setoid ℓ ℓ} → (R : Relation S A B) → Set ℓ @@ -96,7 +96,7 @@ module _ ℓ where { to = λ n → let x , eq = surj n in x ; cong = λ {n}{m} eq → let x , _ = surj n; y , _ = surj m in P.subst (λ m → [ A ][ proj₁ (surj n) ≈ proj₁ (surj m) ]) eq (refl A) } - , λ {n} → proj₂ (surj n) + , λ {n}{m} n≡m → let _ , eq = surj n in P.trans eq n≡m -- principle of unique choice for setoids -- https://ncatlab.org/nlab/show/principle+of+unique+choice diff --git a/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda b/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda index 697a570a9..88589d7a4 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda @@ -40,11 +40,11 @@ module _ {o ℓ e} c ℓ′ {J : Category o ℓ e} (F : Functor J (Setoids (o ; _≲_ = coc ; isPreorder = record { isEquivalence = ≡.isEquivalence - ; reflexive = λ { {j , _} ≡.refl → J.id , identity } + ; reflexive = λ { {j , _} ≡.refl → J.id , (identity (F₀.refl j)) } ; trans = λ { {a , Sa} {b , Sb} {c , Sc} (f , eq₁) (g , eq₂) → let open RS (F₀ c) in g J.∘ f , (begin - F₁ (g J.∘ f) ⟨$⟩ Sa ≈⟨ homomorphism ⟩ + F₁ (g J.∘ f) ⟨$⟩ Sa ≈⟨ homomorphism (F₀.refl a) ⟩ F₁ g ⟨$⟩ (F₁ f ⟨$⟩ Sa) ≈⟨ cong (F₁ g) eq₁ ⟩ F₁ g ⟨$⟩ Sb ≈⟨ eq₂ ⟩ Sc ∎) } @@ -60,9 +60,9 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record ; coapex = record { ψ = λ j → record { to = j ,_ - ; cong = λ i≈k → forth (J.id , Setoid.trans (F₀ _) identity i≈k) + ; cong = λ i≈k → forth (-, identity i≈k) } - ; commute = λ {X} {Y} X⇒Y → back (X⇒Y , Setoid.refl (F₀ Y)) + ; commute = λ {X} X⇒Y x≈y → back (-, cong (F₁ X⇒Y) (F₀.sym X x≈y)) } } ; ⊥-is-initial = record @@ -73,15 +73,16 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record { to = to-coapex K ; cong = minimal (coc c ℓ′ F) K.N (to-coapex K) (coapex-cong K) } - ; commute = Setoid.refl K.N + ; commute = λ {X} x≈y → cong (Coapex.ψ (Cocone.coapex K) X) x≈y } - ; !-unique = λ { {K} f {a , Sa} → + ; !-unique = λ { {K} f {a , Sa} {b , Sb} eq → let module K = Cocone K module f = Cocone⇒ f open RS K.N in begin - K.ψ a ⟨$⟩ Sa ≈˘⟨ f.commute ⟩ - f.arr ⟨$⟩ (a , Sa) ∎ } + K.ψ a ⟨$⟩ Sa ≈˘⟨ f.commute (F₀.refl a) ⟩ + f.arr ⟨$⟩ (a , Sa) ≈⟨ cong f.arr eq ⟩ + f.arr ⟨$⟩ (b , Sb) ∎ } } } } @@ -100,7 +101,7 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record where module K = Cocone K coapex-cong : ∀ K → coc c ℓ′ F =[ to-coapex K ]⇒ (Setoid._≈_ (Cocone.N K)) coapex-cong K {X , x} {Y , y} (f , fx≈y) = begin - K.ψ X ⟨$⟩ x ≈˘⟨ K.commute f ⟩ + K.ψ X ⟨$⟩ x ≈˘⟨ K.commute f (F₀.refl X) ⟩ K.ψ Y ⟨$⟩ (F₁ f ⟨$⟩ x) ≈⟨ cong (K.ψ Y) fx≈y ⟩ K.ψ Y ⟨$⟩ y ∎ where module K = Cocone K diff --git a/src/Categories/Category/Instance/Properties/Setoids/Complete.agda b/src/Categories/Category/Instance/Properties/Setoids/Complete.agda index 72fcc0ed7..f48ced3a9 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Complete.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Complete.agda @@ -10,9 +10,9 @@ open import Relation.Binary.Core using (Rel) open Func open import Categories.Category using (Category; _[_,_]) -open import Categories.Functor.Core using (Functor) -open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Complete using (Complete) +open import Categories.Functor +open import Categories.Category.Instance.Setoids +open import Categories.Category.Complete import Categories.Category.Construction.Cones as Co @@ -36,7 +36,7 @@ Setoids-Complete o ℓ e c ℓ′ {J} F = { to = λ { (S , _) → S j } ; cong = λ eq → eq j } - ; commute = λ { {X} {Y} X⇒Y {_ , eq} → eq X⇒Y } + ; commute = λ { {X} {Y} X⇒Y {_ , eq} {y} f≈g → F₀.trans Y (eq X⇒Y) (f≈g Y) } } } ; ⊤-is-terminal = record @@ -44,12 +44,14 @@ Setoids-Complete o ℓ e c ℓ′ {J} F = let module K = Cone K in record { arr = record - { to = λ x → (λ j → K.ψ j ⟨$⟩ x) , λ f → K.commute f + { to = λ x → (λ j → K.ψ j ⟨$⟩ x) , λ f → K.commute f (Setoid.refl K.N) ; cong = λ a≈b j → cong (K.ψ j) a≈b } - ; commute = λ {X} → Setoid.refl (F₀ X) + ; commute = λ x≈y → cong (K.ψ _) x≈y } - ; !-unique = λ f j → F₀.sym j (Cone⇒.commute f) + ; !-unique = λ {K} f x≈y j → + let module K = Cone K + in F₀.sym j (Cone⇒.commute f (Setoid.sym K.N x≈y)) } } } diff --git a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda index f9d5a7dc8..ad0c42a10 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda @@ -12,7 +12,7 @@ open import Function using (flip) renaming (id to id→; _∘′_ to _∘→_) open import Function.Bundles using (Func; _⟨$⟩_) open import Function.Construct.Identity using () renaming (function to ⟶-id) open import Function.Construct.Composition using (function) -open import Function.Construct.Setoid using () renaming (setoid to _⇨_) +open import Function.Construct.Setoid using () renaming (function to _⇨_) open import Function.Definitions using (StrictlySurjective) open import Level using (Level) open import Relation.Binary using (Setoid; Rel; IsEquivalence) @@ -85,20 +85,20 @@ module _ ℓ where R.relation {SingletonSetoid} (record { to = λ _ → eq ; cong = λ _ → refl R.dom}) (record { to = λ _ → eq′ ; cong = λ _ → refl R.dom}) - (λ { zero → x₁≈ ○ x₁≈x₂ ○ ⟺ x₂≈ - ; (nzero _) → ≈y₁ ○ y₁≈y₂ ○ ⟺ ≈y₂}) + (λ { zero _ → x₁≈ ○ x₁≈x₂ ○ ⟺ x₂≈ + ; (nzero _) _ → ≈y₁ ○ y₁≈y₂ ○ ⟺ ≈y₂}) tt Quotient-Equivalence : IsEquivalence Equation Quotient-Equivalence = record { - refl = eqn _ (ES.is-refl₁) (ES.is-refl₂) - ; sym = λ { (eqn r eq₁ eq₂) → eqn (ES.sym ⟨$⟩ r) (ES.is-sym₁ ○ eq₂) (ES.is-sym₂ ○ eq₁) } + refl = eqn _ (ES.is-refl₁ X.refl) (ES.is-refl₂ X.refl) + ; sym = λ { (eqn r eq₁ eq₂) → eqn (ES.sym ⟨$⟩ r) (ES.is-sym₁ D.refl ○ eq₂) (ES.is-sym₂ D.refl ○ eq₁) } ; trans = λ { (eqn r x≈ ≈y) (eqn s y≈ ≈z) → let t = record { elem₁ = _ ; elem₂ = _ ; commute = y≈ ○ ⟺ ≈y } in eqn (ES.trans ∙ P₀⇒P₁ ⟨$⟩ t) - (ES.is-trans₁ ○ (cong R.p₁ (p₂-≈ {t}) ○ x≈)) - (ES.is-trans₂ ○ (cong R.p₂ (p₁-≈ {t}) ○ ≈z)) + (ES.is-trans₁ R×R.refl ○ (cong R.p₁ (p₂-≈ {t} {t} (D.refl , D.refl)) ○ x≈)) + (ES.is-trans₂ R×R.refl ○ (cong R.p₂ (p₁-≈ {t} {t} (D.refl , D.refl)) ○ ≈z)) } } where @@ -119,7 +119,7 @@ module _ ℓ where ; isCoequalizer = record { equality = inj-≈ ; coequalize = λ {_}{h} → quotient h - ; universal = λ {C} → Setoid.refl C + ; universal = λ {_}{h} → cong h ; unique = λ {_}{h}{i}{eq′} → unique {_}{h}{i}{eq′} } } @@ -130,21 +130,27 @@ module _ ℓ where inj : X ⇒ X∼ inj = record { to = id→ - ; cong = λ {x₁} eq → eqn (ES.refl ⟨$⟩ x₁) ES.is-refl₁ (ES.is-refl₂ ○ eq) + ; cong = λ {x₁} eq → eqn (ES.refl ⟨$⟩ x₁) (ES.is-refl₁ X.refl) (ES.is-refl₂ X.refl ○ eq) } inj-≈ : inj ∘ R.p₁ S.≈ inj ∘ R.p₂ - inj-≈ {x} = eqn x X.refl X.refl + inj-≈ {x} x≈y = eqn x X.refl (cong R.p₂ x≈y) -- coEqualizer wants the 'h' to be implicit, but can't figure it out, so make it explicit here quotient : {C : Obj} (h : X ⇒ C) → h ∘ R.p₁ S.≈ h ∘ R.p₂ → X∼ ⇒ C quotient {C} h eq = record { to = h ⟨$⟩_ - ; cong = λ { (eqn r x≈ ≈y) → trans C (cong h (X.sym x≈)) (trans C eq (cong h ≈y))} + ; cong = λ { (eqn r x≈ ≈y) → trans C (cong h (X.sym x≈)) (trans C (eq (refl R.dom)) (cong h ≈y))} } unique : {C : Obj} {h : X ⇒ C} {i : X∼ ⇒ C} {eq : h ∘ R.p₁ S.≈ h ∘ R.p₂} → h S.≈ i ∘ inj → i S.≈ quotient h eq - unique {C} eq {x} = sym C (eq {x}) + unique {C} {h} {i} {eq′} eq {x} {y} (eqn r x≈ ≈y) = begin + i ⟨$⟩ x ≈˘⟨ eq X.refl ⟩ + h ⟨$⟩ x ≈˘⟨ cong h x≈ ⟩ + h ⟨$⟩ (R.p₁ ⟨$⟩ r) ≈⟨ eq′ (refl R.dom) ⟩ + h ⟨$⟩ (R.p₂ ⟨$⟩ r) ≈⟨ cong h ≈y ⟩ + h ⟨$⟩ y ∎ + where open SR C -- Setoid (strict) Surjectivity SSurj : {A B : Setoid ℓ ℓ} (f : A ⇒ B) → Set ℓ @@ -152,7 +158,7 @@ module _ ℓ where -- Proposition 1 from "Olov Wilander, Setoids and universes" Epi⇒Surjective : ∀ {A B : Setoid ℓ ℓ} (f : A ⇒ B) → Epi S f → SSurj f - Epi⇒Surjective {A} {B} f epi y = g≈h .proj₁ (λ ()) _ + Epi⇒Surjective {A} {B} f epi y = g≈h (refl B {y}) .proj₁ (λ ()) _ where infix 3 _↔_ @@ -182,7 +188,7 @@ module _ ℓ where } g≈h : [ B ⇨ B′ ][ g ≈ h ] - g≈h = epi g h λ {x} → (λ _ u → x , Setoid.refl B) , λ _ () + g≈h = epi g h λ {x}{y} x≈y → (λ u _ → x , cong f x≈y) , λ _ () -- not needed for exactness, but worthwhile Surjective⇒RegularEpi : ∀ {A B : Setoid ℓ ℓ} (f : A ⇒ B) → ((y : ∣ B ∣) → Σ[ x ∈ ∣ A ∣ ] [ B ][ f ⟨$⟩ x ≈ y ]) → RegularEpi S f @@ -190,10 +196,10 @@ module _ ℓ where { h = p₁ kp ; g = p₂ kp ; coequalizer = record - { equality = λ {x} → commute kp {x} + { equality = λ {x} {y} → commute kp {x} {y} ; coequalize = λ {_} {h} → Coeq.coeq {h = h} - ; universal = λ {C} {h} {eq} → Coeq.universal′ {C} {h} (λ {x} → eq {x}) - ; unique = λ {_}{h}{i}{eq} h≈i∘f → Coeq.unique″ {_} {h} (λ {x} → eq {x}) {i} h≈i∘f + ; universal = λ {C} {h} {eq} → Coeq.universal′ {C} {h} (λ {x} {y} → eq {x} {y}) + ; unique = λ {_}{h}{i}{eq} h≈i∘f x≈y → Coeq.unique″ {_} {h} (λ {x} {y} → eq {x} {y}) {i} h≈i∘f x≈y } } where @@ -205,7 +211,7 @@ module _ ℓ where f⁻¹∘h b = h ⟨$⟩ proj₁ (surj b) module _ (h∘p₁≈h∘p₂ : h S.∘ p₁ kp S.≈ h S.∘ p₂ kp) where cong′ : {i j : ∣ B ∣} → [ B ][ i ≈ j ] → [ C ][ h ⟨$⟩ proj₁ (surj i) ≈ h ⟨$⟩ proj₁ (surj j) ] - cong′ {y₁}{y₂} y₁≈y₂ = h∘p₁≈h∘p₂ {pt₁} + cong′ {y₁}{y₂} y₁≈y₂ = h∘p₁≈h∘p₂ {pt₁} {pt₁} (refl A , refl A) where x₁ x₂ : ∣ A ∣ x₁ = surj y₁ .proj₁ @@ -219,20 +225,22 @@ module _ ℓ where coeq : B S.⇒ C coeq = record { to = f⁻¹∘h ; cong = cong′ } universal′ : h S.≈ coeq S.∘ f - universal′ {x} = begin - h ⟨$⟩ x ≈⟨ h∘p₁≈h∘p₂ {mk-× x x₁ (sym B eq₁)} ⟩ - h ⟨$⟩ proj₁ (surj (f ⟨$⟩ x)) ≡⟨⟩ -- by definition of f⁻¹∘h - f⁻¹∘h (f ⟨$⟩ x) ≡⟨⟩ -- by definition of coeq - coeq S.∘ f ⟨$⟩ x ∎ + universal′ {x} {y} x≈y = begin + h ⟨$⟩ x ≈⟨ cong h x≈y ⟩ + h ⟨$⟩ y ≈⟨ h∘p₁≈h∘p₂ {mk-× y x₁ (sym B eq₁)} {mk-× x x₁ (trans B (cong f x≈y) (sym B eq₁))} (sym A x≈y , refl A) ⟩ + h ⟨$⟩ proj₁ (surj (f ⟨$⟩ y)) ≡⟨⟩ -- by definition of f⁻¹∘h + f⁻¹∘h (f ⟨$⟩ y) ≡⟨⟩ -- by definition of coeq + coeq S.∘ f ⟨$⟩ y ∎ where x₁ : ∣ A ∣ - x₁ = surj (f ⟨$⟩ x) .proj₁ - eq₁ : [ B ][ f ⟨$⟩ x₁ ≈ f ⟨$⟩ x ] - eq₁ = surj (f ⟨$⟩ x) .proj₂ + x₁ = surj (f ⟨$⟩ y) .proj₁ + eq₁ : [ B ][ f ⟨$⟩ x₁ ≈ f ⟨$⟩ y ] + eq₁ = surj (f ⟨$⟩ y) .proj₂ unique″ : {i : B S.⇒ C} → h S.≈ i S.∘ f → i S.≈ coeq - unique″ {i} h≈i∘f {y} = begin + unique″ {i} h≈i∘f {x} {y} x≈y = begin + i ⟨$⟩ x ≈⟨ cong i x≈y ⟩ i ⟨$⟩ y ≈⟨ cong i (sym B eq₁) ⟩ - i ∘ f ⟨$⟩ x₁ ≈⟨ sym C h≈i∘f ⟩ + i ∘ f ⟨$⟩ x₁ ≈⟨ sym C (h≈i∘f (refl A)) ⟩ h ⟨$⟩ x₁ ≡⟨⟩ -- by definition of f⁻¹∘h f⁻¹∘h y ∎ where @@ -263,7 +271,7 @@ module _ ℓ where Surjective⇒RegularEpi (p₂ pb) λ y → let (x , eq) = Epi⇒Surjective f (Coequalizer⇒Epi S record { arr = f ; isCoequalizer = coeq }) (u ⟨$⟩ y) in let pt = mk-× x y eq in - P₀⇒P₁ ⟨$⟩ pt , p₂-≈ {pt} + P₀⇒P₁ ⟨$⟩ pt , p₂-≈ {pt} {pt} (refl B , refl D) where pb-fu : Pullback S f u @@ -280,26 +288,34 @@ module _ ℓ where { regular = Setoids-Regular ; quotient = Quotient-Coequalizer ; effective = λ {X} E → record - { commute = eqn _ (refl X) (refl X) + { commute = λ eq → eqn _ (refl X) (cong (Relation.p₂ (R E)) eq) ; universal = λ { {Z}{h₁}{h₂} → universal E h₁ h₂ } - ; unique = λ {Z}{h₁}{h₂}{u}{eq} eq₁ eq₂ {x} → Relation.relation (R E) u (universal E h₁ h₂ eq) - λ { zero {x} → trans X eq₁ (sym X (x₁≈ eq)) - ; (nzero _) {x} → trans X eq₂ (sym X (≈x₂ eq)) + ; unique = λ {Z}{h₁}{h₂}{u}{eq} eq₁ eq₂ {x}{y} → Relation.relation (R E) u (universal E h₁ h₂ eq) + λ { zero {x}{y} eq′ → trans X (eq₁ eq′) (sym X (p₁∘universal≈h₁ E h₁ h₂ eq (refl Z))) + ; (nzero _) {x}{y} eq′ → trans X (eq₂ eq′) (sym X (p₂∘universal≈h₂ E h₁ h₂ eq (refl Z))) } - ; p₁∘universal≈h₁ = λ { {eq = eq} → x₁≈ eq} - ; p₂∘universal≈h₂ = λ { {eq = eq} → ≈x₂ eq} + ; p₁∘universal≈h₁ = λ {Z}{h₁}{h₂}{eq} → p₁∘universal≈h₁ E h₁ h₂ eq + ; p₂∘universal≈h₂ = λ {Z}{h₁}{h₂}{eq} → p₂∘universal≈h₂ E h₁ h₂ eq } } where open Equivalence open Setoid open Coequalizer using (arr) - open Equation universal : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) → (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) → Z ⇒ Relation.dom (R E) - universal E h₁ h₂ eq = record - { to = λ _ → name eq - ; cong = λ {z}{z′} z≈z′ → quotient-trans E (eq {z}) (eq {z′}) (cong h₁ z≈z′) (cong h₂ z≈z′) + universal {X}{Z} E h₁ h₂ eq = record + { to = λ z → let (eqn eq _ _) = eq {z}{z} (refl Z) in eq + ; cong = λ {z}{z′} z≈z′ → quotient-trans E (eq {z}{z} (refl Z)) (eq {z′}{z′} (refl Z)) (cong h₁ z≈z′) (cong h₂ z≈z′) } + p₁∘universal≈h₁ : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) → + (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) → + [ Z ⇨ X ][ Relation.p₁ (R E) ∘ (universal E h₁ h₂ eq) ≈ h₁ ] + p₁∘universal≈h₁ {X}{Z} _ h₁ h₂ eq x≈y = let (eqn _ p₁z≈ _) = eq (refl Z) in trans X p₁z≈ (cong h₁ x≈y) + + p₂∘universal≈h₂ : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) → + (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) → + [ Z ⇨ X ][ Relation.p₂ (R E) ∘ (universal E h₁ h₂ eq) ≈ h₂ ] + p₂∘universal≈h₂ {X}{Z} _ h₁ h₂ eq x≈y = let (eqn _ _ p₂z≈) = eq (refl Z) in trans X p₂z≈ (cong h₂ x≈y) diff --git a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda index c2618ece3..2142fd2c9 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda @@ -9,7 +9,7 @@ open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂; _⊎ₛ_; open import Data.Unit.Polymorphic using (tt) open import Function.Bundles using (Func; _⟨$⟩_) open import Function.Construct.Composition using (function) -open import Function.Construct.Setoid using () renaming (setoid to _⇨_) +open import Function.Construct.Setoid using () renaming (function to _⇨_) open import Relation.Binary using (Setoid) import Relation.Binary.Reasoning.Setoid as SetoidR @@ -34,21 +34,24 @@ Setoids-Extensive ℓ = record ; pullback₂ = λ f → pullback ℓ ℓ f i₂ ; pullback-of-cp-is-cp = λ f → record { [_,_] = λ g h → copair f g h - ; inject₁ = λ {X g h z} → copair-inject₁ f g h z - ; inject₂ = λ {X g h z} → copair-inject₂ f g h z - ; unique = λ {X u g h} feq₁ feq₂ {z} → copair-unique f g h u z feq₁ feq₂ + ; inject₁ = λ {X g h z} eq → + trans (isEquivalence X) (copair-inject₁ f g h z) (cong g eq) + ; inject₂ = λ {X g h z} eq → + trans (isEquivalence X) (copair-inject₂ f g h z) (cong h eq) + ; unique = λ {X u g h} feq₁ feq₂ {z} eq → + trans (isEquivalence X) (copair-unique f g h u z (λ {z} → feq₁ {z}) (λ {z} → feq₂ {z})) (cong u eq) } - ; pullback₁-is-mono = λ _ _ eq → drop-inj₁ eq - ; pullback₂-is-mono = λ _ _ eq → drop-inj₂ eq + ; pullback₁-is-mono = λ _ _ eq x≈y → drop-inj₁ (eq x≈y) + ; pullback₂-is-mono = λ _ _ eq x≈y → drop-inj₂ (eq x≈y) ; disjoint = λ {A B} → record - { commute = λ { {()}} + { commute = λ { {()} _} ; universal = λ {C f g} eq → record - { to = λ z → conflict A B (eq {z}) + { to = λ z → conflict A B (eq {x = z} (refl (isEquivalence C))) ; cong = λ z → tt } - ; unique = λ _ _ → tt - ; p₁∘universal≈h₁ = λ {_ _ _ eq x} → conflict A B (eq {x}) - ; p₂∘universal≈h₂ = λ {_ _ _ eq y} → conflict A B (eq {y}) + ; unique = λ _ _ _ → tt + ; p₁∘universal≈h₁ = λ {_ _ _ eq} x≈y → conflict A B (eq x≈y) + ; p₂∘universal≈h₂ = λ {_ _ _ eq} x≈y → conflict A B (eq x≈y) } } where @@ -144,7 +147,7 @@ Setoids-Extensive ℓ = record copair ⟨$⟩ z XR.≈⟨ X.refl ⟩ g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl) XR.≈⟨ cong (g ⊎⟶ h) (to-⊎ₛ-cong fz≈w) ⟩ g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (inj₁ x) fz≈w) XR.≈⟨ X.refl ⟩ - g ⟨$⟩ fb XR.≈⟨ X.sym (feq₁ {x = fb}) ⟩ + g ⟨$⟩ fb XR.≈⟨ X.sym (feq₁ {x = fb} (C.refl , A.refl)) ⟩ u ⟨$⟩ z XR.∎ where @@ -154,7 +157,7 @@ Setoids-Extensive ℓ = record copair ⟨$⟩ z XR.≈⟨ X.refl ⟩ g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl) XR.≈⟨ cong (g ⊎⟶ h) (to-⊎ₛ-cong fz≈w) ⟩ g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (inj₂ y) fz≈w) XR.≈⟨ X.refl ⟩ - h ⟨$⟩ fb XR.≈⟨ X.sym feq₂ ⟩ + h ⟨$⟩ fb XR.≈⟨ X.sym (feq₂ {x = fb} {y = fb} (C.refl , B.refl)) ⟩ u ⟨$⟩ z XR.∎ where module XR = SetoidR X @@ -164,6 +167,6 @@ Setoids-Extensive ℓ = record [ A′ ⇨ X ][ u ∙ p₁ (pullback ℓ ℓ f i₁) ≈ g ] → [ B′ ⇨ X ][ u ∙ p₁ (pullback ℓ ℓ f i₂) ≈ h ] → [ X ][ copair ⟨$⟩ z ≈ u ⟨$⟩ z ] - copair-unique u z feq₁ feq₂ = copair-unique′ u z feq₁ feq₂ (f ⟨$⟩ z) A⊎B.refl + copair-unique u z feq₁ feq₂ = copair-unique′ u z (λ {x} {y} → feq₁ {x} {y}) (λ {x} {y} → feq₂ {x} {y}) (f ⟨$⟩ z) A⊎B.refl open Diagram diff --git a/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda b/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda index af856b8f1..2801c56c8 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda @@ -8,7 +8,6 @@ open import Function.Bundles using (Func; _⟨$⟩_) import Function.Construct.Identity as FId open import Relation.Binary using (Setoid) import Relation.Binary.PropositionalEquality.Core as ≡ -import Relation.Binary.Reasoning.Setoid as SetoidR open import Categories.Category.Core using (Category) open import Categories.Category.BinaryProducts using (BinaryProducts) @@ -153,10 +152,10 @@ module _ {o} where ; cong = λ eq → eq } ; ⊤-is-terminal = record - { ! = λ { {sliceobj f} → slicearr {h = f} refl } - ; !-unique = λ { {X} (slicearr △) → + { ! = λ { {sliceobj f} → slicearr {h = f} (Func.cong f) } + ; !-unique = λ { {X} (slicearr △) eq → let module X = SliceObj X - in sym △ } + in sym (△ (Setoid.sym X.Y eq)) } } } @@ -170,25 +169,23 @@ module _ {o} where where module X = SliceObj X module Y = SliceObj Y - f : SpanObj → Setoid o o - f = F₀ X Y F : Functor (Category.op Span) (Setoids o o) F = record - { F₀ = f - ; F₁ = λ { (span-id {B}) → FId.function (f B) + { F₀ = F₀ X Y + ; F₁ = λ { (span-id {B}) → FId.function (F₀ X Y B) ; span-arrˡ → X.arr ; span-arrʳ → Y.arr } - ; identity = λ {Z} → S.Equiv.refl {f Z} {f Z} {FId.function _} - ; homomorphism = λ { {Z} {_} {_} {span-id} {span-id} → Setoid.refl (f Z) - ; {_} {_} {_} {span-id} {span-arrˡ} → refl - ; {_} {_} {_} {span-id} {span-arrʳ} → refl - ; {_} {_} {_} {span-arrˡ} {span-id} → refl - ; {_} {_} {_} {span-arrʳ} {span-id} → refl + ; identity = λ {Z} → S.Equiv.refl {F₀ X Y Z} {F₀ X Y Z} {FId.function _} + ; homomorphism = λ { {_} {_} {_} {span-id} {span-id} eq → eq + ; {_} {_} {_} {span-id} {span-arrˡ} → Func.cong X.arr + ; {_} {_} {_} {span-id} {span-arrʳ} → Func.cong Y.arr + ; {_} {_} {_} {span-arrˡ} {span-id} → Func.cong X.arr + ; {_} {_} {_} {span-arrʳ} {span-id} → Func.cong Y.arr } - ; F-resp-≈ = λ { {Z} {_} {span-id} ≡.refl → Setoid.refl (f Z) - ; {_} {_} {span-arrˡ} ≡.refl → refl - ; {_} {_} {span-arrʳ} ≡.refl → refl + ; F-resp-≈ = λ { {_} {_} {span-id} ≡.refl eq → eq + ; {_} {_} {span-arrˡ} ≡.refl → Func.cong X.arr + ; {_} {_} {span-arrʳ} ≡.refl → Func.cong Y.arr } } @@ -220,11 +217,12 @@ module _ {o} where prod = slice-product.A×B eval : {f g : Sl.Obj} → prod (f ^ g) g Sl.⇒ f - eval {f} {g} = slicearr {h = h} λ { {J₁ , arr₁} → + eval {f} {g} = slicearr {h = h} λ { {J₁ , arr₁} {J₂ , arr₂} eq → let open SlExp (J₁ left) in trans (InverseImage.fx≈a (f⇒g (pack (J₁ right) _))) (trans (arr₁ span-arrˡ) - (sym (arr₁ span-arrʳ))) } + (trans (eq center) + (sym (arr₂ span-arrʳ)))) } where module f = SliceObj f module g = SliceObj g module fY = Setoid f.Y @@ -274,7 +272,7 @@ module _ {o} where { f⇒g = λ img → let open InverseImage img renaming (x to y) in pack (α.h ⟨$⟩ xypb x img) - (trans (α.△ {xypb x img}) + (trans (α.△ {xypb x img} {xypb x img} (Setoid.refl (SliceObj.Y (prod f g)) {xypb x img})) fx≈a) ; cong = λ img img′ eq → let module img = InverseImage img @@ -302,29 +300,22 @@ module _ {o} where } curry : f Sl.⇒ (h ^ g) - curry = slicearr {h = β} refl + curry = slicearr {h = β} (Func.cong f.arr) module _ {f g h : Sl.Obj} {α β : prod f g Sl.⇒ h} where private module f = SliceObj f module g = SliceObj g - module h = SliceObj h module gY = Setoid g.Y curry-resp-≈ : α Sl.≈ β → curry α Sl.≈ curry β - curry-resp-≈ hα≈hβ {z} = record - { idx≈ = refl + curry-resp-≈ eq eq′ = record + { idx≈ = Func.cong f.arr eq′ ; map≈ = λ img → - let open InverseImage img in - let open SetoidR h.Y - in begin - InverseImage.x (SlExp.f⇒g (Slice⇒.h (curry α) ⟨$⟩ z) img) ≈⟨ hα≈hβ ⟩ - InverseImage.x (SlExp.f⇒g (Slice⇒.h (curry β) ⟨$⟩ z) img) ≈⟨ Func.cong (Slice⇒.h β) ( - λ { center → refl - ; left → Setoid.refl f.Y - ; right → gY.refl - }) ⟩ - InverseImage.x (SlExp.f⇒g (Slice⇒.h (curry β) ⟨$⟩ z) (inverseImage-transport refl img)) ∎ + let open InverseImage img + in eq λ { center → Func.cong f.arr eq′ + ; left → eq′ + ; right → gY.refl } } module _ {f g h : Sl.Obj} {α : f Sl.⇒ (g ^ h)} {β : prod f h Sl.⇒ g} where @@ -339,15 +330,16 @@ module _ {o} where module hY = Setoid h.Y curry-unique : eval Sl.∘ (α products.⁂ Sl.id) Sl.≈ β → α Sl.≈ curry β - curry-unique eq {z} = record - { idx≈ = α.△ + curry-unique eq {z} {w} eq′ = record + { idx≈ = α.△ eq′ ; map≈ = λ img → let open InverseImage img in gY.trans (InverseImageMap.cong (SlExp.map (α.h ⟨$⟩ z)) img _ hY.refl) - (eq {xypb z (inverseImage-transport α.△ img)} - {-λ { center → Func.cong f.arr eq′ + (eq {xypb z (inverseImage-transport (trans (α.△ eq′) (Func.cong f.arr (fY.sym eq′))) img)} + {xypb w (inverseImage-transport (α.△ eq′) img)} + λ { center → Func.cong f.arr eq′ ; left → eq′ - ; right → hY.refl }-}) + ; right → hY.refl }) } slice-canonical : Canonical Sl @@ -365,12 +357,11 @@ module _ {o} where ; _^_ = _^_ ; eval = eval ; curry = curry - ; eval-comp = λ { {_} {A1} {A2} {α} {J , arr₁} → + ; eval-comp = λ { {_} {_} {_} {α} {J , arr₁} eq → let module α = Slice⇒ α - in Func.cong α.h λ { center → arr₁ span-arrˡ - ; left → Setoid.refl (SliceObj.Y A2) - ; right → Setoid.refl (SliceObj.Y A1) - } } + in Func.cong α.h λ { center → trans (arr₁ span-arrˡ) (eq center) + ; left → eq left + ; right → eq right } } ; curry-unique = λ {_ _ _} {α β} → curry-unique {_} {_} {_} {α} {β} } diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda index 381eb039f..650d73aad 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -49,18 +49,18 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record ; p₁ = record { to = elem₁ ; cong = proj₁ } ; p₂ = record { to = elem₂ ; cong = proj₂ } ; isPullback = record - { commute = λ { {fg} → commute fg} + { commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q) ; universal = λ {A} {h₁} {h₂} eq → record { to = λ a → record { elem₁ = h₁ ⟨$⟩ a ; elem₂ = h₂ ⟨$⟩ a - ; commute = eq + ; commute = eq (refl A) } ; cong = < cong h₁ , cong h₂ > } - ; unique = λ eq₁ eq₂ → eq₁ , eq₂ - ; p₁∘universal≈h₁ = X.refl - ; p₂∘universal≈h₂ = Y.refl + ; unique = λ eq₁ eq₂ x≈y → eq₁ x≈y , eq₂ x≈y + ; p₁∘universal≈h₁ = λ {_} {h₁} {_} eq → cong h₁ eq + ; p₂∘universal≈h₂ = λ {_} {_} {h₂} eq → cong h₂ eq } } where diff --git a/src/Categories/Category/Instance/Setoids.agda b/src/Categories/Category/Instance/Setoids.agda index 8de6d6075..04c6f8bea 100644 --- a/src/Categories/Category/Instance/Setoids.agda +++ b/src/Categories/Category/Instance/Setoids.agda @@ -21,14 +21,14 @@ Setoids : ∀ c ℓ → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids c ℓ = record { Obj = Setoid c ℓ ; _⇒_ = Func - ; _≈_ = λ {A} {B} f g → _≈_ (S.setoid A B) f g + ; _≈_ = λ {A} {B} f g → _≈_ (S.function A B) f g ; id = Id.function _ ; _∘_ = λ f g → Comp.function g f - ; assoc = λ {_} {_} {_} {D} → refl D - ; sym-assoc = λ {_} {_} {_} {D} → refl D - ; identityˡ = λ {_} {B} → refl B - ; identityʳ = λ {_} {B} → refl B - ; identity² = λ {A} → refl A - ; equiv = λ {A} {B} → isEquivalence (S.setoid A B) - ; ∘-resp-≈ = λ {_} {_} {C} {f} {h} {g} {i} f≈h g≈i {x} → trans C f≈h (cong h g≈i) + ; assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → cong h $ cong g $ cong f x≈y + ; sym-assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → cong h $ cong g $ cong f x≈y + ; identityˡ = λ {A} {B} {f} x≈y → cong f x≈y + ; identityʳ = λ {A} {B} {f} x≈y → cong f x≈y + ; identity² = λ x≈y → x≈y + ; equiv = λ {A} {B} → isEquivalence (S.function A B) + ; ∘-resp-≈ = λ f≈f′ g≈g′ x≈y → f≈f′ (g≈g′ x≈y) } diff --git a/src/Categories/Category/Instance/SimplicialSet/Properties.agda b/src/Categories/Category/Instance/SimplicialSet/Properties.agda index 19cbd31a3..1eb01e644 100644 --- a/src/Categories/Category/Instance/SimplicialSet/Properties.agda +++ b/src/Categories/Category/Instance/SimplicialSet/Properties.agda @@ -96,11 +96,12 @@ boundary-map {n = n} f b = record { to = λ (lift b) → lift (boundary-map f b) ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) } - ; identity = lift (Δ-eq Eq.refl) - ; homomorphism = lift (Δ-eq Eq.refl) - ; F-resp-≈ = λ {_} {_} {f} {g} f≈g {b} → lift $ Δ-eq $ λ {x} → begin - ⟦ hom (lower b) ⟧ (⟦ f ⟧ x) ≡⟨ cong ⟦ hom (lower b) ⟧ (Δ-pointwise f≈g) ⟩ - ⟦ hom (lower b) ⟧ (⟦ g ⟧ x) ∎ + ; identity = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) + ; homomorphism = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) + ; F-resp-≈ = λ {_} {_} {f} {g} f≈g {b} {b′} eq → lift $ Δ-eq $ λ {x} → begin + ⟦ hom (lower b) ⟧ (⟦ f ⟧ x) ≡⟨ Δ-pointwise (lower eq) ⟩ + ⟦ hom (lower b′) ⟧ (⟦ f ⟧ x) ≡⟨ cong ⟦ hom (lower b′) ⟧ (Δ-pointwise f≈g) ⟩ + ⟦ hom (lower b′) ⟧ (⟦ g ⟧ x) ∎ } where open Boundary @@ -140,11 +141,12 @@ record Horn (m n-1 : ℕ) (k : Fin (ℕ.suc n-1)) : Set where } ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) } - ; identity = lift (Δ-eq Eq.refl) - ; homomorphism = lift (Δ-eq Eq.refl) - ; F-resp-≈ = λ {_} {_} {f} {g} f≈g {h} → lift $ Δ-eq $ λ {x} → begin - ⟦ hom (lower h) ⟧ (⟦ f ⟧ x) ≡⟨ cong ⟦ hom (lower h) ⟧ (Δ-pointwise f≈g) ⟩ - ⟦ hom (lower h) ⟧ (⟦ g ⟧ x) ∎ + ; identity = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) + ; homomorphism = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) + ; F-resp-≈ = λ {_} {_} {f} {g} f≈g {h} {h′} eq → lift $ Δ-eq $ λ {x} → begin + ⟦ hom (lower h) ⟧ (⟦ f ⟧ x) ≡⟨ Δ-pointwise (lower eq) ⟩ + ⟦ hom (lower h′) ⟧ (⟦ f ⟧ x) ≡⟨ cong ⟦ hom (lower h′) ⟧ (Δ-pointwise f≈g) ⟩ + ⟦ hom (lower h′) ⟧ (⟦ g ⟧ x) ∎ } where open Horn @@ -165,14 +167,14 @@ module _ where { to = ⊥-elim ; cong = λ { {()} } } - ; commute = λ { _ {()} } + ; commute = λ { _ {()} _ } } ∂Δ-inj {ℕ.suc n} = ntHelper record { η = λ X → record { to = λ (lift b) → lift (hom b) ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) } - ; commute = λ f → lift (Δ-eq Eq.refl) + ; commute = λ f (lift eq) → lift (Δ-eq (Δ-pointwise eq)) } where open Boundary @@ -184,7 +186,7 @@ module _ where { to = λ (lift h) → lift (hom h) ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq)) } - ; commute = λ _ → lift (Δ-eq Eq.refl) + ; commute = λ f (lift eq) → lift (Δ-eq (Δ-pointwise eq)) } where open Horn diff --git a/src/Categories/Category/Monoidal/Instance/Setoids.agda b/src/Categories/Category/Monoidal/Instance/Setoids.agda index 447b46499..4edc6cdb4 100644 --- a/src/Categories/Category/Monoidal/Instance/Setoids.agda +++ b/src/Categories/Category/Monoidal/Instance/Setoids.agda @@ -44,9 +44,9 @@ module _ {o ℓ} where { to = λ x → f ⟨$⟩ x , g ⟨$⟩ x ; cong = λ eq → cong f eq , cong g eq } - ; project₁ = A.refl - ; project₂ = B.refl - ; unique = λ eq₁ eq₂ → A.sym eq₁ , B.sym eq₂ + ; project₁ = λ {_ h i} eq → cong h eq + ; project₂ = λ {_ h i} eq → cong i eq + ; unique = λ {W h i j} eq₁ eq₂ eq → A.sym (eq₁ (Setoid.sym W eq)) , B.sym (eq₂ (Setoid.sym W eq)) } } } @@ -68,10 +68,10 @@ module _ {o ℓ} where { to = [ f ⟨$⟩_ , g ⟨$⟩_ ] ; cong = λ { (inj₁ x) → cong f x ; (inj₂ x) → cong g x } } - ; inject₁ = λ {C} → Setoid.refl C - ; inject₂ = λ {C} → Setoid.refl C - ; unique = λ {C} h₁≈f h₂≈g → λ { {inj₁ x} → Setoid.sym C h₁≈f - ; {inj₂ y} → Setoid.sym C h₂≈g} + ; inject₁ = λ {_} {f} → cong f + ; inject₂ = λ {_} {_} {g} → cong g + ; unique = λ { {C} h≈f h≈g (inj₁ x) → Setoid.sym C (h≈f (Setoid.sym A x)) + ; {C} h≈f h≈g (inj₂ x) → Setoid.sym C (h≈g (Setoid.sym B x)) } } } } diff --git a/src/Categories/Category/Species/Constructions.agda b/src/Categories/Category/Species/Constructions.agda index 992a4aef2..571f499f8 100644 --- a/src/Categories/Category/Species/Constructions.agda +++ b/src/Categories/Category/Species/Constructions.agda @@ -91,10 +91,9 @@ module _ (o : Level) where { F₀ = proj₁ ; F₁ = λ f → record { to = from f ⟨$⟩_ - ; cong = Func.cong (from f) - } - ; identity = λ { {(S , _)} → Setoid.refl S } - ; homomorphism = λ {_} {_} {Z} → Setoid.refl (proj₁ Z) + ; cong = Func.cong (from f) } + ; identity = id→ + ; homomorphism = λ { {f = f} {g} x≈y → Func.cong (from g) (Func.cong (from f) x≈y)} ; F-resp-≈ = _≃_.from-≈ } @@ -107,12 +106,12 @@ module _ (o : Level) where ; cong = λ { (inj₁ x≈y) → inj₁ (Func.cong (A.₁ X≅Y) x≈y ) ; (inj₂ x≈y) → inj₂ (Func.cong (B.₁ X≅Y) x≈y)} } - ; identity = λ { {S , n , pf} {inj₁ x} → inj₁ (A.identity {x = x}) - ; {S , n , pf} {inj₂ y} → inj₂ B.identity} - ; homomorphism = λ { {x = inj₁ x} → inj₁ A.homomorphism - ; {x = inj₂ y} → inj₂ B.homomorphism} - ; F-resp-≈ = λ { f≈g {inj₁ x} → inj₁ (A.F-resp-≈ f≈g) - ; f≈g {inj₂ y} → inj₂ (B.F-resp-≈ f≈g)} + ; identity = λ { (inj₁ x) → inj₁ (A.identity x) + ; (inj₂ x) → inj₂ (B.identity x)} + ; homomorphism = λ { (inj₁ x) → inj₁ (A.homomorphism x) + ; (inj₂ x) → inj₂ (B.homomorphism x) } + ; F-resp-≈ = λ { f≃g (inj₁ x) → inj₁ (A.F-resp-≈ f≃g x) + ; f≃g (inj₂ x) → inj₂ (B.F-resp-≈ f≃g x)} } where module A = Functor A @@ -126,9 +125,9 @@ module _ (o : Level) where { to = ×.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_) ; cong = ×.map (Func.cong (A.₁ X≅Y)) (Func.cong (B.₁ X≅Y)) } - ; identity = A.identity , B.identity - ; homomorphism = A.homomorphism , B.homomorphism - ; F-resp-≈ = λ f≈g → (A.F-resp-≈ f≈g) , (B.F-resp-≈ f≈g) + ; identity = ×.map A.identity B.identity + ; homomorphism = ×.map A.homomorphism B.homomorphism + ; F-resp-≈ = λ f≈g → ×.map (A.F-resp-≈ f≈g) (B.F-resp-≈ f≈g) } where module A = Functor A diff --git a/src/Categories/CoYoneda.agda b/src/Categories/CoYoneda.agda index 0bdd7a820..7c602bec6 100644 --- a/src/Categories/CoYoneda.agda +++ b/src/Categories/CoYoneda.agda @@ -48,9 +48,9 @@ module Yoneda (C : Category o ℓ e) where embed = record { F₀ = Hom[ C ][_,-] ; F₁ = Hom[C,A]⇒Hom[C,B] -- B⇒A induces a NatTrans on the Homs. - ; identity = identityʳ - ; homomorphism = sym-assoc - ; F-resp-≈ = λ f≈g → refl⟩∘⟨ f≈g + ; identity = identityʳ ○_ + ; homomorphism = λ h₁≈h₂ → ∘-resp-≈ˡ h₁≈h₂ ○ sym-assoc + ; F-resp-≈ = λ f≈g h≈i → ∘-resp-≈ h≈i f≈g } -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor @@ -61,34 +61,34 @@ module Yoneda (C : Category o ℓ e) where ; from = λ x → ntHelper record { η = λ X → record { to = λ X⇒a → F.₁ X⇒a ⟨$⟩ x - ; cong = λ i≈j → F.F-resp-≈ i≈j + ; cong = λ i≈j → F.F-resp-≈ i≈j SE.refl } - ; commute = λ {X} {Y} X⇒Y {f} → + ; commute = λ {X} {Y} X⇒Y {f} {g} f≈g → let module SR = SetoidR (F.₀ Y) in SR.begin - F.₁ (X⇒Y ∘ f ∘ id) ⟨$⟩ x SR.≈⟨ F.F-resp-≈ (∘-resp-≈ʳ identityʳ) ⟩ - F.₁ (X⇒Y ∘ f) ⟨$⟩ x SR.≈⟨ F.homomorphism ⟩ - F.₁ X⇒Y ⟨$⟩ (F.₁ f ⟨$⟩ x) + F.₁ (X⇒Y ∘ f ∘ id) ⟨$⟩ x SR.≈⟨ F.F-resp-≈ (∘-resp-≈ʳ (identityʳ ○ f≈g)) SE.refl ⟩ + F.₁ (X⇒Y ∘ g) ⟨$⟩ x SR.≈⟨ F.homomorphism SE.refl ⟩ + F.₁ X⇒Y ⟨$⟩ (F.₁ g ⟨$⟩ x) SR.∎ } - ; to-cong = λ i≈j → i≈j - ; from-cong = λ i≈j → cong (F.₁ _) i≈j + ; to-cong = λ i≈j → i≈j CE.refl + ; from-cong = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j ; inverse = ( λ {b} {nat} eq → let module SR = SetoidR (F.₀ a) in let open SR in begin - to (η nat a) id ≈⟨ eq ⟩ - to (F.₁ id) b ≈⟨ F.identity ⟩ + to (η nat a) id ≈⟨ eq {a} {id} {id} CE.refl ⟩ + to (F.₁ id) b ≈⟨ F.identity (Setoid.refl (F.₀ a) {b}) ⟩ b ∎) - , λ {nat} {y} eq {b} {f} → + , λ {nat} {y} eq {b} {f} {g} f≈g → let open Setoid (F.₀ b) in let module SR = SetoidR (F.₀ b) in let open SR in begin - to (F.₁ f) y ≈⟨ cong (F.₁ f) eq ⟩ - to (F.₁ f) (to (η nat a) id) ≈⟨ sym-commute nat f ⟩ - to (η nat b) (f ∘ id ∘ id) ≈⟨ cong (η nat b) (refl⟩∘⟨ identity² ○ identityʳ) ⟩ - to (η nat b) f ∎ + to (F.₁ f) y ≈⟨ cong (F.₁ f) eq ⟩ + to (F.₁ f) (to (η nat a) id) ≈⟨ sym-commute nat f CE.refl ⟩ + to (η nat b) (f ∘ id ∘ id) ≈⟨ cong (η nat b) (refl⟩∘⟨ identity² ○ (identityʳ ○ f≈g)) ⟩ + to (η nat b) g ∎ } where module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity) @@ -111,50 +111,57 @@ module Yoneda (C : Category o ℓ e) where { η = λ where (F , A) → record { to = λ α → lift (yoneda-inverse.to α) - ; cong = λ i≈j → lift i≈j + ; cong = λ i≈j → lift (i≈j CE.refl) } ; commute = λ where - {_} {G , B} (α , f) {β} → lift $ cong (η α B) (helper f β) + {_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ) } ; F⇐G = ntHelper record - { η = λ { (F , A) → record + { η = λ (F , A) → record { to = λ x → yoneda-inverse.from (lower x) - ; cong = λ i≈j → cong (Functor.F₁ F _) (lower i≈j) - } } - ; commute = λ { {F , A} {G , B} (α , f) {X} {Z} {h} → helper′ α f} + ; cong = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j) + } + ; commute = λ { {F , A} {G , B} (α , f) {X} {Y} eq {Z} {h} {i} eq′ → helper′ α f (lower eq) eq′} } - ; iso = λ { (F , A) → record - { isoˡ = λ {α} → yoneda-inverse.strictlyInverseʳ α - ; isoʳ = lift (Functor.identity F) - } } + ; iso = λ (F , A) → record + { isoˡ = λ {α β} i≈j {X} y≈z → + Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.strictlyInverseʳ α {x = X} y≈z ) (i≈j CE.refl) + ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.strictlyInverseˡ {F = F} _) (lower eq)) + } } where helper : {F : Functor C (Setoids ℓ e)} {A B : Obj} (f : A ⇒ B) - (β : NaturalTransformation Hom[ C ][ A ,-] F) → - Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ id ∘ f) (Functor.F₁ F f ⟨$⟩ (η β A ⟨$⟩ id)) - helper {F} {A} {B} f β = S.begin + (β γ : NaturalTransformation Hom[ C ][ A ,-] F) → + Setoid._≈_ (Functor.F₀ Nat[Hom[C][c,-],F] (F , A)) β γ → + Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ id ∘ f) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id)) + helper {F} {A} {B} f β γ β≈γ = S.begin η β B ⟨$⟩ id ∘ f S.≈⟨ cong (η β B) (MR.id-comm-sym C ○ ∘-resp-≈ʳ (⟺ identity²)) ⟩ - η β B ⟨$⟩ f ∘ id ∘ id S.≈⟨ commute β f ⟩ - F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.∎ + η β B ⟨$⟩ f ∘ id ∘ id S.≈⟨ commute β f CE.refl ⟩ + F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩ + F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎ where module F = Functor F using (₀;₁) module S = SetoidR (F.₀ B) helper′ : ∀ {F G : Functor C (Setoids ℓ e)} {A B Z : Obj} - {h : B ⇒ Z} - {X : Setoid.Carrier (Functor.F₀ F A)} + {h i : B ⇒ Z} + {X Y : Setoid.Carrier (Functor.F₀ F A)} (α : NaturalTransformation F G) (f : A ⇒ B) → + Setoid._≈_ (Functor.F₀ F A) X Y → + h ≈ i → Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X))) - (η α Z ⟨$⟩ (Functor.F₁ F (h ∘ f) ⟨$⟩ X)) - helper′ {F} {G} {A} {B} {Z} {h} {X} α f = S.begin - G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h ⟩ - η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ cong (η α Z) F.homomorphism ⟩ - η α Z ⟨$⟩ (F.₁ (h ∘ f) ⟨$⟩ X) S.∎ + (η α Z ⟨$⟩ (Functor.F₁ F (i ∘ f) ⟨$⟩ Y)) + helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin + G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h ((S′.sym (cong (F.₁ f) eq))) ⟩ + η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) ((F.F-resp-≈ eq′ S′.refl)) ⟩ + η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) ((F.homomorphism (Setoid.refl (F.₀ A)))) ⟩ + η α Z ⟨$⟩ (F.₁ (i ∘ f) ⟨$⟩ Y) S.∎ where module F = Functor F using (₀; ₁; homomorphism; F-resp-≈) module G = Functor G using (₀; ₁) module S = SetoidR (G.₀ Z) + module S′ = Setoid (F.₀ B) using (refl; sym) module yoneda = NaturalIsomorphism yoneda diff --git a/src/Categories/Enriched/Over/Setoids.agda b/src/Categories/Enriched/Over/Setoids.agda index 5d8d6ecac..e7e04ac7b 100644 --- a/src/Categories/Enriched/Over/Setoids.agda +++ b/src/Categories/Enriched/Over/Setoids.agda @@ -37,9 +37,12 @@ Cat→Cat′ C = record { to = uncurry _∘_ ; cong = uncurry ∘-resp-≈ } - ; ⊚-assoc = assoc - ; unitˡ = identityˡ - ; unitʳ = identityʳ + ; ⊚-assoc = λ { {x = (x₁ , x₂) , x₃} {(y₁ , y₂) , y₃} ((x₁≈y₁ , x₂≈y₂) , x₃≈y₃) → begin + (x₁ ∘ x₂) ∘ x₃ ≈⟨ assoc {h = x₁} ⟩ + x₁ ∘ x₂ ∘ x₃ ≈⟨ (x₁≈y₁ ⟩∘⟨ x₂≈y₂ ⟩∘⟨ x₃≈y₃) ⟩ + y₁ ∘ y₂ ∘ y₃ ∎ } + ; unitˡ = λ { {_} {_} {_ , x} {_ , y} (_ , x≈y) → Equiv.trans (identityˡ {f = x}) x≈y } + ; unitʳ = λ z → Equiv.trans identityʳ (proj₁ z) } where open SCategory C @@ -52,11 +55,11 @@ Cat′→Cat 𝓒 = record ; _≈_ = λ {a} {b} f g → _≈_ (hom a b) f g ; id = id ⟨$⟩ lift tt ; _∘_ = λ f g → ⊚ ⟨$⟩ (f , g) - ; assoc = λ {A} {B} {C} {D} → ⊚-assoc - ; sym-assoc = λ {A} {B} {C} {D} → sym (hom A D) ⊚-assoc - ; identityˡ = λ {A} {B} → unitˡ - ; identityʳ = λ {A} {B} → unitʳ - ; identity² = λ {A} → unitˡ -- Enriched doesn't have a unit² + ; assoc = λ {A} {B} {C} {D} → ⊚-assoc ((refl (hom C D) , refl (hom B C)) , refl (hom A B)) + ; sym-assoc = λ {A} {B} {C} {D} → sym (hom A D) (⊚-assoc ((refl (hom C D) , refl (hom B C)) , refl (hom A B))) + ; identityˡ = λ {A} {B} → unitˡ (lift tt , refl (hom A B)) + ; identityʳ = λ {A} {B} → unitʳ (refl (hom A B) , lift tt) + ; identity² = λ {A} → unitˡ (lift tt , refl (hom A A)) -- Enriched doesn't have a unit² ; equiv = λ {A} {B} → record { refl = refl (hom A B) ; sym = sym (hom A B) diff --git a/src/Categories/Functor/Construction/LiftSetoids.agda b/src/Categories/Functor/Construction/LiftSetoids.agda index 53cbb6960..18a5f4cb3 100644 --- a/src/Categories/Functor/Construction/LiftSetoids.agda +++ b/src/Categories/Functor/Construction/LiftSetoids.agda @@ -38,9 +38,7 @@ LiftSetoids c′ ℓ′ = record { to = λ where (lift x) → lift $ f ⟨$⟩ x ; cong = λ where (lift eq) → lift $ cong f eq } - ; identity = λ {A} → lift $ refl A - ; homomorphism = λ {_} {_} {Z} → lift $ refl Z - ; F-resp-≈ = λ f≈g → lift f≈g + ; identity = idf + ; homomorphism = λ where {f = f} {g = g} (lift eq) → lift $ cong g $ cong f eq + ; F-resp-≈ = λ where fx≈gy (lift x≈y) → lift $ fx≈gy x≈y } - where - open Setoid diff --git a/src/Categories/Functor/Hom.agda b/src/Categories/Functor/Hom.agda index 9581e046e..046fabdc4 100644 --- a/src/Categories/Functor/Hom.agda +++ b/src/Categories/Functor/Hom.agda @@ -29,14 +29,42 @@ module Hom {o ℓ e} (C : Category o ℓ e) where { to = λ h → g ∘ h ∘ f ; cong = ∘-resp-≈ʳ ∙ ∘-resp-≈ˡ } - ; identity = identityˡ ○ identityʳ - ; homomorphism = refl⟩∘⟨ sym-assoc ○ ⟺ assoc²'' - ; F-resp-≈ = λ { (f₁≈g₁ , f₂≈g₂) → f₂≈g₂ ⟩∘⟨ refl⟩∘⟨ f₁≈g₁} + ; identity = identity′ + ; homomorphism = homomorphism′ + ; F-resp-≈ = F-resp-≈′ } where F₀′ : Obj × Obj → Setoid ℓ e F₀′ (A , B) = hom-setoid {A} {B} open HomReasoning + identity′ : {A : Obj × Obj} {x y : uncurry _⇒_ A} → x ≈ y → id ∘ x ∘ id ≈ y + identity′ {A} {x} {y} x≈y = begin + id ∘ x ∘ id ≈⟨ identityˡ ⟩ + x ∘ id ≈⟨ identityʳ ⟩ + x ≈⟨ x≈y ⟩ + y ∎ + + homomorphism′ : ∀ {X Y Z : Σ Obj (λ x → Obj)} + {f : proj₁ Y ⇒ proj₁ X × proj₂ X ⇒ proj₂ Y} + {g : proj₁ Z ⇒ proj₁ Y × proj₂ Y ⇒ proj₂ Z} + {x y : proj₁ X ⇒ proj₂ X} → + x ≈ y → + (proj₂ g ∘ proj₂ f) ∘ x ∘ proj₁ f ∘ proj₁ g ≈ + proj₂ g ∘ (proj₂ f ∘ y ∘ proj₁ f) ∘ proj₁ g + homomorphism′ {f = f₁ , f₂} {g₁ , g₂} {x} {y} x≈y = begin + (g₂ ∘ f₂) ∘ x ∘ f₁ ∘ g₁ ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + (g₂ ∘ f₂) ∘ (x ∘ f₁) ∘ g₁ ≈⟨ pullʳ (pullˡ (∘-resp-≈ʳ (∘-resp-≈ˡ x≈y))) ⟩ + g₂ ∘ (f₂ ∘ y ∘ f₁) ∘ g₁ ∎ + + F-resp-≈′ : ∀ {A B : Σ Obj (λ x → Obj)} + {f g : Σ (proj₁ B ⇒ proj₁ A) (λ x → proj₂ A ⇒ proj₂ B)} → + Σ (proj₁ f ≈ proj₁ g) (λ x → proj₂ f ≈ proj₂ g) → + {x y : proj₁ A ⇒ proj₂ A} → + x ≈ y → proj₂ f ∘ x ∘ proj₁ f ≈ proj₂ g ∘ y ∘ proj₁ g + F-resp-≈′ {f = f₁ , f₂} {g₁ , g₂} (f₁≈g₁ , f₂≈g₂) {x} {y} x≈y = begin + f₂ ∘ x ∘ f₁ ≈⟨ f₂≈g₂ ⟩∘⟨ x≈y ⟩∘⟨ f₁≈g₁ ⟩ + g₂ ∘ y ∘ g₁ ∎ + Hom[_,-] : Obj → Functor C (Setoids ℓ e) Hom[_,-] = appˡ Hom[-,-] diff --git a/src/Categories/Functor/Hom/Properties/Contra.agda b/src/Categories/Functor/Hom/Properties/Contra.agda index bea7d657a..2bca4f0db 100644 --- a/src/Categories/Functor/Hom/Properties/Contra.agda +++ b/src/Categories/Functor/Hom/Properties/Contra.agda @@ -45,14 +45,14 @@ module _ (W : Obj) {F : Functor J C} (col : Colimit F) where Hom≃ = record { F⇒G = ntHelper record { η = λ _ → idFun hom-setoid - ; commute = λ _ → C.assoc + ; commute = λ _ eq → C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq) ○ C.assoc } ; F⇐G = ntHelper record { η = λ _ → idFun hom-setoid - ; commute = λ _ → C.sym-assoc + ; commute = λ _ eq → C.sym-assoc ○ C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq) } ; iso = λ _ → record - { isoˡ = C.Equiv.refl - ; isoʳ = C.Equiv.refl + { isoˡ = λ eq → eq + ; isoʳ = λ eq → eq } } diff --git a/src/Categories/Functor/Hom/Properties/Covariant.agda b/src/Categories/Functor/Hom/Properties/Covariant.agda index 798b5ccf4..3ac32183b 100644 --- a/src/Categories/Functor/Hom/Properties/Covariant.agda +++ b/src/Categories/Functor/Hom/Properties/Covariant.agda @@ -51,7 +51,7 @@ module _ (W : Obj) {F : Functor J C} (lim : Limit F) where { N = W ; apex = record { ψ = λ X → K.ψ X ⟨$⟩ x - ; commute = λ f → ⟺ (∘-resp-≈ʳ identityʳ) ○ K.commute f + ; commute = λ f → ⟺ (∘-resp-≈ʳ identityʳ) ○ K.commute f (Setoid.refl K.N) } } @@ -62,21 +62,25 @@ module _ (W : Obj) {F : Functor J C} (lim : Limit F) where ; cong = λ {x y} eq → ψ-≈⇒rep-≈ F W (Cone.apex (KW x)) (Cone.apex (KW y)) lim (λ A → Func.cong (K.ψ A) eq) } - ; commute = λ {X} {x} → begin + ; commute = λ {X} {x y} eq → begin proj X ∘ rep (KW x) ∘ C.id ≈⟨ refl⟩∘⟨ C.identityʳ ⟩ proj X ∘ rep (KW x) ≈⟨ lim.commute ⟩ - K.ψ X ⟨$⟩ x ∎ + K.ψ X ⟨$⟩ x ≈⟨ Func.cong (K.ψ X) eq ⟩ + K.ψ X ⟨$⟩ y ∎ } !-unique : ∀ {K : Cone HomF} (f : Cones HomF [ K , ⊤ ]) → Cones HomF [ ! K ≈ f ] - !-unique {K} f {x} = terminal.!-unique f′ + !-unique {K} f {x} {y} x≈y = begin + rep (KW K x) ≈⟨ terminal.!-unique f′ ⟩ + f.arr ⟨$⟩ x ≈⟨ Func.cong f.arr x≈y ⟩ + f.arr ⟨$⟩ y ∎ where module K = Cone _ K module f = Cone⇒ _ f f′ : Cones F [ KW K x , limit ] f′ = record { arr = f.arr ⟨$⟩ x - ; commute = ⟺ (∘-resp-≈ʳ C.identityʳ) ○ f.commute + ; commute = ⟺ (∘-resp-≈ʳ C.identityʳ) ○ f.commute (Setoid.refl K.N) } hom-resp-limit : Limit HomF diff --git a/src/Categories/Functor/Instance/0-Truncation.agda b/src/Categories/Functor/Instance/0-Truncation.agda index 06a5dba23..4ad95941f 100644 --- a/src/Categories/Functor/Instance/0-Truncation.agda +++ b/src/Categories/Functor/Instance/0-Truncation.agda @@ -6,12 +6,13 @@ module Categories.Functor.Instance.0-Truncation where -- -- This is the right-adjoint of the inclusion functor from Setoids to -- Groupoids (see Categories.Functor.Adjoint.Instance.ZeroTruncation) --- + +import Function open import Function.Bundles using (Func) open import Relation.Binary using (Setoid) open import Categories.Category using (Category; _[_≈_]) -open import Categories.Functor using (Functor) +open import Categories.Functor hiding (id) open import Categories.Category.Groupoid using (Groupoid) open import Categories.Category.Instance.Groupoids using (Groupoids) open import Categories.Category.Instance.Setoids using (Setoids) @@ -22,8 +23,8 @@ Trunc : ∀ {o ℓ e} → Functor (Groupoids o ℓ e) (Setoids o ℓ) Trunc {o} {ℓ} {e} = record { F₀ = TruncSetoid ; F₁ = λ {G H} F → TruncMap {G} {H} F - ; identity = λ {A} → Category.id (category A) - ; homomorphism = λ {_} {_} {Z} → Category.id (category Z) + ; identity = Function.id + ; homomorphism = λ {_ _ _ F G} f → F₁ G (F₁ F f) ; F-resp-≈ = λ {G H} → TruncRespNI {G} {H} } where @@ -49,7 +50,7 @@ Trunc {o} {ℓ} {e} = record TruncRespNI : ∀ {G H : Groupoid o ℓ e} {E F : Functor (category G) (category H)} → E ≃ F → Setoids o ℓ [ TruncMap {G} {H} E ≈ TruncMap {G} {H} F ] - TruncRespNI {_} {H} {_} {F} μ {a} = ⇒.η a + TruncRespNI {_} {H} {_} {F} μ {a} f = F₁ F f ∘ ⇒.η a where open Groupoid H open NaturalIsomorphism μ diff --git a/src/Categories/Functor/Instance/ConnectedComponents.agda b/src/Categories/Functor/Instance/ConnectedComponents.agda index 30322351c..4503124a9 100644 --- a/src/Categories/Functor/Instance/ConnectedComponents.agda +++ b/src/Categories/Functor/Instance/ConnectedComponents.agda @@ -20,7 +20,26 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIs { to = Functor.F₀ F ; cong = ST.gmap (Functor.F₀ F) (Functor.F₁ F) } - ; identity = λ {A} → Plus⇔.forth (Category.id A) - ; homomorphism = λ {_ _ Z F G x} → Plus⇔.forth (Category.id Z) - ; F-resp-≈ = λ {A} {B} {f} {g} α {a} → Plus⇔.forth (NaturalIsomorphism.⇒.η α a) + ; identity = λ x → x + ; homomorphism = λ {_ _ _ F G} → ST.gmap + (Functor.F₀ G ∙ Functor.F₀ F) + (Functor.F₁ G ∙ Functor.F₁ F) + ; F-resp-≈ = my-resp _ _ } + where + my-resp : ∀ {A B : Category _ _ _} (f g : Functor A B) + (f≅g : NaturalIsomorphism f g) {x y} → + Plus⇔ (Category._⇒_ A) x y → + Plus⇔ (Category._⇒_ B) (Functor.F₀ f x) (Functor.F₀ g y) + my-resp {A} {B} f g f≅g {x} {y} (Plus⇔.forth m) + = Plus⇔.forth (B [ NaturalIsomorphism.⇒.η f≅g _ ∘ Functor.F₁ f m ]) + my-resp {A} {B} f g f≅g {x} {y} (Plus⇔.back m) + = Plus⇔.back (B [ Functor.F₁ f m ∘ NaturalIsomorphism.⇐.η f≅g _ ]) + my-resp {A} {B} f g f≅g {x} {y} (Plus⇔.forth⁺ m ms) + = Plus⇔.forth⁺ + (B [ NaturalIsomorphism.⇒.η f≅g _ ∘ Functor.F₁ f m ]) + (ST.gmap (Functor.F₀ g) (Functor.F₁ g) ms) + my-resp {A} {B} f g f≅g {x} {y} (Plus⇔.back⁺ m ms) + = Plus⇔.back⁺ + (B [ Functor.F₁ f m ∘ NaturalIsomorphism.⇐.η f≅g _ ]) + (ST.gmap (Functor.F₀ g) (Functor.F₁ g) ms) diff --git a/src/Categories/Functor/Instance/SetoidDiscrete.agda b/src/Categories/Functor/Instance/SetoidDiscrete.agda index d9910740f..8aa3e1f6b 100644 --- a/src/Categories/Functor/Instance/SetoidDiscrete.agda +++ b/src/Categories/Functor/Instance/SetoidDiscrete.agda @@ -50,11 +50,11 @@ Discrete {o} {ℓ} {e} = record } where open Setoid Z ExtensionalityNI : {A B : Setoid o ℓ} {f g : Func A B} → let open Setoid A in - ({x : Carrier} → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ x)) → + ({x y : Carrier} → x ≈ y → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ y)) → NaturalIsomorphism (DiscreteFunctor f) (DiscreteFunctor g) - ExtensionalityNI {A} {B} f≈g = record - { F⇒G = record { η = λ X → f≈g {X} } - ; F⇐G = record { η = λ X → B.sym (f≈g {X}) } + ExtensionalityNI {A} {B} cong≈ = record + { F⇒G = record { η = λ X → cong≈ A.refl } + ; F⇐G = record { η = λ X → B.sym (cong≈ A.refl) } } where module A = Setoid A diff --git a/src/Categories/Functor/Profunctor.agda b/src/Categories/Functor/Profunctor.agda index f9bbfd960..c7aaf14e8 100644 --- a/src/Categories/Functor/Profunctor.agda +++ b/src/Categories/Functor/Profunctor.agda @@ -26,10 +26,7 @@ open import Categories.NaturalTransformation using (NaturalTransformation; _∘ open import Categories.NaturalTransformation.Equivalence using (_≃_; ≃-isEquivalence) open import Categories.NaturalTransformation.Properties using (appˡ-nat; appʳ-nat) -import Relation.Binary.Reasoning.Setoid as SetoidR - open Setoid renaming (_≈_ to _[[_≈_]]) -open Func record Profunctor {o ℓ e} {o′ ℓ′ e′} ℓ″ e″ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) @@ -44,6 +41,7 @@ record Profunctor {o ℓ e} {o′ ℓ′ e′} ℓ″ e″ cod : Category o′ ℓ′ e′ cod = D + private variable o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ ℓP eP ℓQ eQ : Level C D E : Category o ℓ e @@ -89,7 +87,7 @@ _ⓟ′_ {C = C} {D} {E} P Q = record P.₁ˡ g ⟨$⟩ in-side y ≈⟨ cong (P.₁ˡ g) (FormalComposite.Twines.in-tertwines h) ⟩ P.₁ˡ g ⟨$⟩ (P.₁ʳ (FormalComposite.Twines.twiner h) ⟨$⟩ in-side x) - ≈˘⟨ [ P.bimodule ]-commute ⟩ + ≈˘⟨ [ P.bimodule ]-commute (refl (P.₀ _)) ⟩ P.₁ʳ (FormalComposite.Twines.twiner h) ⟨$⟩ (P.₁ˡ g ⟨$⟩ in-side x) ∎ ; out-ertwines = let open SetoidR (Q.₀ (rendezvous x , _)) in @@ -97,7 +95,7 @@ _ⓟ′_ {C = C} {D} {E} P Q = record Q.₁ʳ f ⟨$⟩ out-side x ≈⟨ cong (Q.₁ (D.id , f)) (FormalComposite.Twines.out-ertwines h) ⟩ Q.₁ʳ f ⟨$⟩ (Q.₁ˡ (FormalComposite.Twines.twiner h) ⟨$⟩ out-side y) - ≈⟨ [ Q.bimodule ]-commute ⟩ + ≈⟨ [ Q.bimodule ]-commute (refl (Q.₀ _)) ⟩ Q.₁ˡ (FormalComposite.Twines.twiner h) ⟨$⟩ (Q.₁ʳ f ⟨$⟩ out-side y) ∎ } @@ -111,12 +109,7 @@ _ⓟ′_ {C = C} {D} {E} P Q = record { F⇒G = record { η = λ x → record { twiner = D.id - ; in-tertwines = - let module SR = SetoidR (P.₀ (e , rendezvous x)) in - let open SR in begin - in-side x ≈˘⟨ P.identity ⟩ - to (P.F₁ (E.id , D.id)) (in-side x) ≈˘⟨ cong (P.F₁ (E.id , D.id)) P.identity ⟩ - to (P.F₁ (E.id , D.id)) (to (P.F₁ (E.id , D.id)) (in-side x)) ∎ + ; in-tertwines = Setoid.sym (P.₀ _) (P.identity (P.identity (Setoid.refl (P.₀ _)))) ; out-ertwines = Setoid.refl (Q.₀ _) } ; commute = λ f → id-comm-sym D @@ -126,12 +119,7 @@ _ⓟ′_ {C = C} {D} {E} P Q = record { η = λ x → record { twiner = D.id ; in-tertwines = Setoid.refl (P.₀ _) - ; out-ertwines = - let module SR = SetoidR (Q.₀ (rendezvous x , c)) in - let open SR in begin - out-side x ≈˘⟨ Q.identity ⟩ - to (Q.F₁ (D.id , C.id)) (out-side x) ≈˘⟨ cong (Q.F₁ (D.id , C.id)) Q.identity ⟩ - to (Q.F₁ (D.id , C.id)) (to (Q.F₁ (D.id , C.id)) (out-side x)) ∎ + ; out-ertwines = Setoid.sym (Q.₀ _) (Q.identity (Q.identity (Setoid.refl (Q.₀ _)))) } ; commute = λ f → id-comm-sym D ; sym-commute = λ f → id-comm D @@ -151,14 +139,20 @@ _ⓟ′_ {C = C} {D} {E} P Q = record { twiner = D.id ; in-tertwines = let open SetoidR (P.₀ (eZ , rendezvous X)) in begin - P.₁ˡ eg ⟨$⟩ (P.₁ˡ ef ⟨$⟩ in-side X) ≈˘⟨ P.homomorphismˡ ⟩ - P.₁ˡ (P.cod [ ef ∘ eg ]) ⟨$⟩ in-side X ≈˘⟨ P.identity ⟩ - P.₁ʳ D.id ⟨$⟩ (P.₁ˡ (P.cod [ ef ∘ eg ]) ⟨$⟩ in-side X) ∎ + P.₁ˡ eg ⟨$⟩ (P.₁ˡ ef ⟨$⟩ in-side X) + ≈˘⟨ P.homomorphismˡ (Setoid.refl (P.₀ _)) ⟩ + P.₁ˡ (P.cod [ ef ∘ eg ]) ⟨$⟩ in-side X + ≈˘⟨ P.identity (Setoid.refl (P.₀ _)) ⟩ + P.₁ʳ D.id ⟨$⟩ (P.₁ˡ (P.cod [ ef ∘ eg ]) ⟨$⟩ in-side X) + ∎ ; out-ertwines = let open SetoidR (Q.₀ (rendezvous X , cZ)) in begin - Q.₁ʳ (C [ cg ∘ cf ]) ⟨$⟩ out-side X ≈⟨ Q.homomorphismʳ ⟩ - Q.₁ʳ cg ⟨$⟩ (Q.₁ʳ cf ⟨$⟩ out-side X) ≈˘⟨ Q.identity ⟩ - Q.₁ˡ D.id ⟨$⟩ (Q.₁ʳ cg ⟨$⟩ (Q.₁ʳ cf ⟨$⟩ out-side X)) ∎ + Q.₁ʳ (C [ cg ∘ cf ]) ⟨$⟩ out-side X + ≈⟨ Q.homomorphismʳ (Setoid.refl (Q.₀ _)) ⟩ + Q.₁ʳ cg ⟨$⟩ (Q.₁ʳ cf ⟨$⟩ out-side X) + ≈˘⟨ Q.identity (Setoid.refl (Q.₀ _)) ⟩ + Q.₁ˡ D.id ⟨$⟩ (Q.₁ʳ cg ⟨$⟩ (Q.₁ʳ cf ⟨$⟩ out-side X)) + ∎ } ; commute = λ f → id-comm-sym D ; sym-commute = λ f → id-comm D @@ -169,17 +163,17 @@ _ⓟ′_ {C = C} {D} {E} P Q = record ; in-tertwines = let open SetoidR (P.₀ (eZ , rendezvous X)) in begin P.₁ˡ (E [ ef ∘ eg ]) ⟨$⟩ in-side X - ≈⟨ P.homomorphismˡ ⟩ + ≈⟨ P.homomorphismˡ (Setoid.refl (P.₀ _)) ⟩ P.₁ˡ eg ⟨$⟩ (P.₁ˡ ef ⟨$⟩ in-side X) - ≈˘⟨ P.identity ⟩ + ≈˘⟨ P.identity (Setoid.refl (P.₀ _)) ⟩ P.₁ʳ D.id ⟨$⟩ (P.₁ˡ eg ⟨$⟩ (P.₁ˡ ef ⟨$⟩ in-side X)) ∎ ; out-ertwines = let open SetoidR (Q.₀ (rendezvous X , cZ)) in begin Q.₁ʳ cg ⟨$⟩ (Q.₁ʳ cf ⟨$⟩ out-side X) - ≈˘⟨ Q.homomorphismʳ ⟩ + ≈˘⟨ Q.homomorphismʳ (Setoid.refl (Q.₀ _)) ⟩ Q.₁ʳ (C [ cg ∘ cf ]) ⟨$⟩ out-side X - ≈˘⟨ Q.identity ⟩ + ≈˘⟨ Q.identity (Setoid.refl (Q.₀ _)) ⟩ Q.₁ˡ D.id ⟨$⟩ (Q.₁ʳ (C [ cg ∘ cf ]) ⟨$⟩ out-side X) ∎ } @@ -195,19 +189,8 @@ _ⓟ′_ {C = C} {D} {E} P Q = record { F⇒G = record { η = λ X → record { twiner = D.id - ; in-tertwines = - let module SR = SetoidR (P.₀ (eB , rendezvous X)) in - let open SR in begin - to (P.F₁ (eg , D.id)) (in-side X) ≈⟨ P.F-resp-≈ ((E.Equiv.sym ef≈eg) , D.Equiv.refl) ⟩ - to (P.F₁ (ef , D.id)) (in-side X) ≈˘⟨ P.identity ⟩ - to (P.F₁ (E.id , D.id)) (to (P.F₁ (ef , D.id)) (in-side X)) ∎ - -- Setoid.sym (P.₀ _) P.identity - ; out-ertwines = - let module SR = SetoidR (Q.₀ (rendezvous X , cB)) in - let open SR in begin - to (Q.F₁ (D.id , cf)) (out-side X) ≈⟨ Q.F-resp-≈ (D.Equiv.refl , cf≈cg) ⟩ - to (Q.F₁ (D.id , cg)) (out-side X) ≈˘⟨ Q.identity ⟩ - to (Q.F₁ (D.id , C.id)) (to (Q.F₁ (D.id , cg)) (out-side X)) ∎ -- Setoid.sym (Q.₀ _) (Q.identity (Q.resp-≈ʳ (C.Equiv.sym cf≈cg) (Setoid.refl (Q.₀ _)))) + ; in-tertwines = Setoid.sym (P.₀ _) (P.identity (P.resp-≈ˡ ef≈eg (Setoid.refl (P.₀ _)))) + ; out-ertwines = Setoid.sym (Q.₀ _) (Q.identity (Q.resp-≈ʳ (C.Equiv.sym cf≈cg) (Setoid.refl (Q.₀ _)))) } ; commute = λ f → id-comm-sym D ; sym-commute = λ f → id-comm D @@ -215,18 +198,8 @@ _ⓟ′_ {C = C} {D} {E} P Q = record ; F⇐G = record { η = λ X → record { twiner = D.id - ; in-tertwines = - let module SR = SetoidR (P.₀ (eB , rendezvous X)) in - let open SR in begin - to (P.F₁ (ef , D.id)) (in-side X) ≈⟨ P.F-resp-≈ (ef≈eg , D.Equiv.refl) ⟩ - to (P.F₁ (eg , D.id)) (in-side X) ≈˘⟨ P.identity ⟩ - to (P.F₁ (E.id , D.id)) (to (P.F₁ (eg , D.id)) (in-side X)) ∎ - ; out-ertwines = - let module SR = SetoidR (Q.₀ (rendezvous X , cB)) in - let open SR in begin - to (Q.F₁ (D.id , cg)) (out-side X) ≈⟨ Q.F-resp-≈ (D.Equiv.refl , C.Equiv.sym cf≈cg) ⟩ - to (Q.F₁ (D.id , cf)) (out-side X) ≈˘⟨ Q.identity ⟩ - to (Q.F₁ (D.id , C.id)) (to (Q.F₁ (D.id , cf)) (out-side X)) ∎ + ; in-tertwines = Setoid.sym (P.₀ _) (P.identity (P.resp-≈ˡ (E.Equiv.sym ef≈eg) (Setoid.refl (P.₀ _)))) + ; out-ertwines = Setoid.sym (Q.₀ _) (Q.identity (Q.resp-≈ʳ cf≈cg (Setoid.refl (Q.₀ _)))) } ; commute = λ f → id-comm-sym D ; sym-commute = λ f → id-comm D @@ -252,22 +225,15 @@ _▻_ {oC} {ℓC} {eC} {oD} {ℓD} {eD} {oE} {ℓE} {eE} {ℓP} {eP} {ℓQ} {eQ} (LiftSetoids (ℓC ⊔ ℓP) (eC ⊔ eP) ∘ˡ appʳ-nat Q.bimodule cf) ∘ᵥ ϕ ∘ᵥ (LiftSetoids (ℓC ⊔ ℓQ) (eC ⊔ eQ) ∘ˡ appʳ-nat P.bimodule df) - ; cong = λ {σ τ} σ≈τ {e x} → lift (cong (Q.₁ʳ cf) (lower σ≈τ)) + ; cong = λ {σ τ} σ≈τ {e x y} x≈y → + lift (cong (Q.₁ʳ cf) (lower (σ≈τ (lift (cong (P.₁ʳ df) (lower x≈y)))))) } - ; identity = λ { {(d , c)} {σ} {e} {x} → lift - let module SR = SetoidR (Q.₀ (e , c)) in let open SR in begin - to (Q.F₁ (E.id , C.id)) - (lower (to (η σ e) (lift (to (P.F₁ (E.id , D.id)) (lower x))))) ≈⟨ Q.identity ⟩ - lower (to (η σ e) (lift (to (P.F₁ (E.id , D.id)) (lower x)))) ≈⟨ lower (cong (η σ e) (lift P.identity)) ⟩ - lower (to (η σ e) x) ∎} - ; homomorphism = λ { {(dX , cX)} {(dY , cY)} {(dZ , cZ)} {(df , cf)} {(dg , cg)} {σ} {e} {x} → - let module S = Setoid (Q.₀ (e , cZ)) in - lift (S.trans Q.homomorphismʳ - (cong (Q.₁ (E.id , cg)) (cong (Q.₁ (E.id , cf)) (lower (cong (η σ e) (lift P.homomorphismʳ))))))} - ; F-resp-≈ = λ { {_} {(dB , cB)} {(df , cf)} {(dg , cg)} (df≈dg , cf≈cg) {σ} {e} {x} → - let module S = Setoid (Q.₀ (e , cB)) in - lift (S.trans (Q.resp-≈ʳ cf≈cg) - (cong (Q.₁ (E.id , cg)) (lower (cong (η σ e) (lift (P.resp-≈ʳ df≈dg))))))} + ; identity = λ {(d , c)} {σ τ} σ≈τ {e x y} x≈y → + lift (Q.identity (lower (σ≈τ (lift (P.identity (lower x≈y)))))) + ; homomorphism = λ {(dX , cX) (dY , cY) (dZ , cZ) (df , cf) (dg , cg) σ τ} σ≈τ {e x y} x≈y → + lift (Q.homomorphismʳ (lower (σ≈τ (lift (P.homomorphismʳ (lower x≈y)))))) + ; F-resp-≈ = λ {(dA , cA) (dB , cB) (df , cf) (dg , cg)} (df≈dg , cf≈cg) {σ τ} σ≈τ {e x y} x≈y → + lift (Q.resp-≈ʳ cf≈cg (lower (σ≈τ (lift (P.resp-≈ʳ df≈dg (lower x≈y)))))) }) where module P = Profunctor P @@ -275,7 +241,6 @@ _▻_ {oC} {ℓC} {eC} {oD} {ℓD} {eD} {oE} {ℓE} {eE} {ℓP} {eP} {ℓQ} {eQ} module C = Category C module D = Category D module E = Category E - open NaturalTransformation using (η) _◅_ : ∀ {oC ℓC eC oD ℓD eD oE ℓE eE ℓP eP ℓQ eQ} {C : Category oC ℓC eC} {D : Category oD ℓD eD} {E : Category oE ℓE eE} @@ -289,19 +254,15 @@ _◅_ {oC} {ℓC} {eC} {oD} {ℓD} {eD} {oE} {ℓE} {eE} {ℓP} {eP} {ℓQ} {eQ} (LiftSetoids (ℓE ⊔ ℓQ) (eE ⊔ eQ) ∘ˡ appˡ-nat P.bimodule ef) ∘ᵥ ϕ ∘ᵥ (LiftSetoids (ℓE ⊔ ℓP) (eE ⊔ eP) ∘ˡ appˡ-nat Q.bimodule df) - ; cong = λ {σ} {τ} σ≈τ {e} {x} → lift (cong (P.₁ˡ ef) (lower σ≈τ )) + ; cong = λ {σ τ} σ≈τ {e x y} x≈y → + lift (cong (P.₁ˡ ef) (lower (σ≈τ (lift (cong (Q.₁ˡ df) (lower x≈y)))))) } - ; identity = λ { {(d , c)} {σ} {e} {x} → - let module S = Setoid (P.₀ (d , e)) in - lift (S.trans P.identity - (lower (cong (η σ e) (lift Q.identity))))} - ; homomorphism = λ { {_} {_} {(eZ , dZ)} {(ef , _)} {(eg , _)} {σ} {c} → - let module S = Setoid (P.₀ (eZ , c)) in - lift (S.trans P.homomorphismˡ - (cong (P.F₁ (eg , C.id)) (cong (P.F₁ (ef , C.id)) (lower (cong (η σ c) (lift Q.homomorphismˡ))))))} - ; F-resp-≈ = λ { {(eA , dA)} {(eB , dB)} {(ef , df)} {(eg , dg)} (ef≈eg , df≈dg) {σ} {c} → - let module S = Setoid (P.₀ (eB , c)) in - lift (S.trans (P.resp-≈ˡ ef≈eg) (cong (P.₁ (eg , C.id)) (lower (cong (η σ c) (lift (Q.resp-≈ˡ df≈dg))))))} + ; identity = λ {(d , c)} {σ τ} σ≈τ {e x y} x≈y → + lift (P.identity (lower (σ≈τ (lift (Q.identity (lower x≈y)))))) + ; homomorphism = λ {(eX , dX) (eY , dY) (eZ , dZ) (ef , df) (eg , dg) σ τ} σ≈τ {c x y} x≈y → + lift (P.homomorphismˡ (lower (σ≈τ (lift (Q.homomorphismˡ (lower x≈y)))))) + ; F-resp-≈ = λ {(eA , dA) (eB , dB) (ef , df) (eg , dg)} (ef≈eg , df≈dg) {σ τ} σ≈τ {c x y} x≈y → + lift (P.resp-≈ˡ ef≈eg (lower (σ≈τ (lift (Q.resp-≈ˡ df≈dg (lower x≈y)))))) }) where module P = Profunctor P @@ -309,7 +270,6 @@ _◅_ {oC} {ℓC} {eC} {oD} {ℓD} {eD} {oE} {ℓE} {eE} {ℓP} {eP} {ℓQ} {eQ} module C = Category C module D = Category D module E = Category E - open NaturalTransformation using (η) module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where private @@ -331,19 +291,20 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where { to = λ x → g ∘ x ∘ F₁ f ; cong = λ x → begin _ ≈⟨ refl⟩∘⟨ x ⟩∘⟨refl ⟩ _ ∎ } - ; identity = λ {x} {y} → begin + ; identity = λ {x} {y} {y'} y≈y' → begin D.id ∘ y ∘ F₁ C.id ≈⟨ D.identityˡ ⟩ y ∘ F₁ C.id ≈⟨ elimʳ identity ⟩ - y ∎ - ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} → begin - (g1 ∘ f1) ∘ x ∘ F₁ (f0 C.∘ g0) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩ - (g1 ∘ f1) ∘ x ∘ F₁ f0 ∘ F₁ g0 ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩ - (g1 ∘ f1) ∘ (x ∘ F₁ f0) ∘ F₁ g0 ≈⟨ Equiv.sym assoc²'' ⟩ - g1 ∘ (f1 ∘ x ∘ F₁ f0) ∘ F₁ g0 ∎ + y ≈⟨ y≈y' ⟩ + y' ∎ + ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} {y} x≈y → begin + (g1 ∘ f1) ∘ x ∘ F₁ (f0 C.∘ g0) ≈⟨ refl⟩∘⟨ x≈y ⟩∘⟨ F.homomorphism ⟩ + (g1 ∘ f1) ∘ y ∘ F₁ f0 ∘ F₁ g0 ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩ + (g1 ∘ f1) ∘ (y ∘ F₁ f0) ∘ F₁ g0 ≈⟨ Equiv.sym assoc²'' ⟩ + g1 ∘ (f1 ∘ y ∘ F₁ f0) ∘ F₁ g0 ∎ } - ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} → begin - f1 ∘ x ∘ F₁ f0 ≈⟨ f1≈g1 ⟩∘⟨ refl⟩∘⟨ F-resp-≈ f0≈g0 ⟩ - g1 ∘ x ∘ F₁ g0 ∎ + ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} {y} x≈y → begin + f1 ∘ x ∘ F₁ f0 ≈⟨ f1≈g1 ⟩∘⟨ x≈y ⟩∘⟨ F-resp-≈ f0≈g0 ⟩ + g1 ∘ y ∘ F₁ g0 ∎ } } where @@ -361,19 +322,20 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where { to = λ x → F₁ g ∘ x ∘ f ; cong = λ x → begin _ ≈⟨ refl⟩∘⟨ x ⟩∘⟨refl ⟩ _ ∎ } - ; identity = λ {x} {y} → begin + ; identity = λ {x} {y} {y'} y≈y' → begin F₁ C.id ∘ y ∘ D.id ≈⟨ elimˡ identity ⟩ y ∘ D.id ≈⟨ D.identityʳ ⟩ - y ∎ - ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} → begin - F₁ (g1 C.∘ f1) ∘ x ∘ f0 ∘ g0 ≈⟨ F.homomorphism ⟩∘⟨refl ⟩ - (F₁ g1 ∘ F₁ f1) ∘ x ∘ f0 ∘ g0 ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩ - (F₁ g1 ∘ F₁ f1) ∘ (x ∘ f0) ∘ g0 ≈⟨ Equiv.sym assoc²'' ⟩ - F₁ g1 ∘ (F₁ f1 ∘ x ∘ f0) ∘ g0 ∎ + y ≈⟨ y≈y' ⟩ + y' ∎ + ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} {y} x≈y → begin + F₁ (g1 C.∘ f1) ∘ x ∘ f0 ∘ g0 ≈⟨ F.homomorphism ⟩∘⟨ x≈y ⟩∘⟨refl ⟩ + (F₁ g1 ∘ F₁ f1) ∘ y ∘ f0 ∘ g0 ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩ + (F₁ g1 ∘ F₁ f1) ∘ (y ∘ f0) ∘ g0 ≈⟨ Equiv.sym assoc²'' ⟩ + F₁ g1 ∘ (F₁ f1 ∘ y ∘ f0) ∘ g0 ∎ } - ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} → begin - F₁ f1 ∘ x ∘ f0 ≈⟨ F-resp-≈ f1≈g1 ⟩∘⟨ refl⟩∘⟨ f0≈g0 ⟩ - F₁ g1 ∘ x ∘ g0 ∎ + ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} {y} x≈y → begin + F₁ f1 ∘ x ∘ f0 ≈⟨ F-resp-≈ f1≈g1 ⟩∘⟨ x≈y ⟩∘⟨ f0≈g0 ⟩ + F₁ g1 ∘ y ∘ g0 ∎ } } where @@ -391,7 +353,7 @@ homProf {ℓ = ℓ} {e} C D = record ; sym-assoc = λ { {f = f} {g} {h} → sym-assoc-lemma {f = f} {g} {h}} ; identityˡ = λ { {f = f} → id-lemmaˡ {f = f} } ; identityʳ = λ { {f = f} → id-lemmaʳ {f = f} } - ; identity² = λ {A} {x} → Setoid.refl (Functor.F₀ (Profunctor.bimodule A) x) + ; identity² = λ z → z ; equiv = ≃-isEquivalence ; ∘-resp-≈ = λ { {f = f} {h} {g} {i} eq eq' → ∘ᵥ-resp-≃ {f = f} {h} {g} {i} eq eq' } } diff --git a/src/Categories/Functor/Profunctor/Cograph.agda b/src/Categories/Functor/Profunctor/Cograph.agda index 3e2e9f6ec..5fce62447 100644 --- a/src/Categories/Functor/Profunctor/Cograph.agda +++ b/src/Categories/Functor/Profunctor/Cograph.agda @@ -48,29 +48,31 @@ module _ {o ℓ e o′ ℓ′ e′ ℓ″ e″} ; assoc = λ { {inj₁ dA} {inj₁ dB} {inj₁ dC} {inj₁ dD} {f} {g} {h} → lift D.assoc ; {inj₁ dA} {inj₁ dB} {inj₁ dC} {inj₂ cD} {f} {g} {r} → - lift (Setoid.sym (F₀ _) (homomorphismˡ)) + lift (Setoid.sym (F₀ _) (homomorphismˡ (Setoid.refl (F₀ _)))) ; {inj₁ dA} {inj₁ dB} {inj₂ cC} {inj₂ cD} {f} {q} {h} → - lift (Setoid.sym (F₀ _) ([ bimodule ]-commute)) + lift (Setoid.sym (F₀ _) ([ bimodule ]-commute (Setoid.refl (F₀ _)))) ; {inj₁ dA} {inj₂ cB} {inj₂ cC} {inj₂ cD} {p} {g} {h} → - lift (homomorphismʳ ) + lift (homomorphismʳ (Setoid.refl (F₀ _))) ; {inj₂ cA} {inj₂ cB} {inj₂ cC} {inj₂ cD} {f} {g} {h} → lift C.assoc } ; sym-assoc = λ { {inj₁ dA} {inj₁ dB} {inj₁ dC} {inj₁ dD} {f} {g} {h} → lift D.sym-assoc - ; {inj₁ dA} {inj₁ dB} {inj₁ dC} {inj₂ cD} {f} {g} {r} → lift homomorphismˡ - ; {inj₁ dA} {inj₁ dB} {inj₂ cC} {inj₂ cD} {f} {q} {h} → lift ([ bimodule ]-commute ) + ; {inj₁ dA} {inj₁ dB} {inj₁ dC} {inj₂ cD} {f} {g} {r} → + lift (homomorphismˡ (Setoid.refl (F₀ _))) + ; {inj₁ dA} {inj₁ dB} {inj₂ cC} {inj₂ cD} {f} {q} {h} → + lift ([ bimodule ]-commute (Setoid.refl (F₀ _))) ; {inj₁ dA} {inj₂ cB} {inj₂ cC} {inj₂ cD} {p} {g} {h} → - lift (Setoid.sym (F₀ _) homomorphismʳ) + lift (Setoid.sym (F₀ _) (homomorphismʳ (Setoid.refl (F₀ _)))) ; {inj₂ cA} {inj₂ cB} {inj₂ cC} {inj₂ cD} {f} {g} {h} → lift C.sym-assoc } ; identityˡ = λ { {inj₁ dA} {inj₁ dB} {f} → lift D.identityˡ - ; {inj₁ dA} {inj₂ cB} {p} → lift identity + ; {inj₁ dA} {inj₂ cB} {p} → lift (identity (Setoid.refl (F₀ _))) ; {inj₂ cA} {inj₂ cB} {f} → lift C.identityˡ } ; identityʳ = λ { {inj₁ dA} {inj₁ dB} {f} → lift D.identityʳ - ; {inj₁ dA} {inj₂ cB} {p} → lift identity + ; {inj₁ dA} {inj₂ cB} {p} → lift (identity (Setoid.refl (F₀ _))) ; {inj₂ cA} {inj₂ cB} {f} → lift C.identityʳ } ; identity² = λ @@ -103,12 +105,9 @@ module _ {o ℓ e o′ ℓ′ e′ ℓ″ e″} { {inj₁ dA} {inj₁ dB} {inj₁ dC} {f} {h} {g} {i} → λ x y → lift (D.∘-resp-≈ (lower x) (lower y)) ; {inj₁ dA} {inj₁ dB} {inj₂ cC} {f} {h} {g} {i} → - λ f≈h g≈i → lift ( - Setoid.trans (F₀ _) (resp-≈ˡ (lower g≈i)) - (cong (F₁ _) (lower f≈h))) + λ f≈h g≈i → lift (resp-≈ˡ (lower g≈i) (lower f≈h)) ; {inj₁ dA} {inj₂ cB} {inj₂ cC} {f} {h} {g} {i} → - λ f≈h g≈i → lift ( - Setoid.trans (F₀ _) (resp-≈ʳ (lower f≈h)) (cong (F₁ _) (lower g≈i))) + λ f≈h g≈i → lift (resp-≈ʳ (lower f≈h) (lower g≈i)) ; {inj₂ cA} {inj₂ cB} {inj₂ cC} {f} {h} {g} {i} → λ x y → lift (C.∘-resp-≈ (lower x) (lower y)) } diff --git a/src/Categories/Functor/Profunctor/FormalComposite.agda b/src/Categories/Functor/Profunctor/FormalComposite.agda index e41db7852..ce7df494f 100644 --- a/src/Categories/Functor/Profunctor/FormalComposite.agda +++ b/src/Categories/Functor/Profunctor/FormalComposite.agda @@ -44,8 +44,8 @@ module FormalComposite {o ℓ e} {ℓ′ e′ ℓ″ e″} ; _≈_ = λ f g → C [ Twines.twiner f ≈ Twines.twiner g ] ; id = λ {c} → record { twiner = Category.id C - ; in-tertwines = let x = F₀ (T.rendezvous c) in sym x identity - ; out-ertwines = let x = G.₀ (T.rendezvous c) in sym x G.identity } + ; in-tertwines = let x = F₀ (T.rendezvous c) in sym x (identity (refl x)) + ; out-ertwines = let x = G.₀ (T.rendezvous c) in sym x (G.identity (refl x)) } ; _∘_ = λ {a b c} f g → record { twiner = twiner f ∘ twiner g ; in-tertwines = let open SetoidR (F₀ (T.rendezvous c)) in @@ -53,17 +53,21 @@ module FormalComposite {o ℓ e} {ℓ′ e′ ℓ″ e″} T.in-side c ≈⟨ in-tertwines f ⟩ F₁ (twiner f) ⟨$⟩ T.in-side b - ≈⟨ Func.cong (F₁ (twiner f)) (in-tertwines g) ⟩ + ≈⟨ F-resp-≈ Equiv.refl (in-tertwines g) ⟩ F₁ (twiner f) ⟨$⟩ (F₁ (twiner g) ⟨$⟩ T.in-side a) - ≈⟨ sym (F₀ (T.rendezvous c)) homomorphism ⟩ + ≈⟨ sym (F₀ (T.rendezvous c)) (homomorphism (refl (F₀ (T.rendezvous a)))) ⟩ F₁ (twiner f ∘ twiner g) ⟨$⟩ T.in-side a ∎ ; out-ertwines = let open SetoidR (G.₀ (T.rendezvous a)) in begin - T.out-side a ≈⟨ out-ertwines g ⟩ - G.₁ (twiner g) ⟨$⟩ T.out-side b ≈⟨ Func.cong (G.₁ (twiner g)) (out-ertwines f) ⟩ - G.₁ (twiner g) ⟨$⟩ (G.₁ (twiner f) ⟨$⟩ T.out-side c) ≈˘⟨ G.homomorphism ⟩ - G.₁ (twiner f ∘ twiner g) ⟨$⟩ T.out-side c ∎ + T.out-side a + ≈⟨ out-ertwines g ⟩ + G.₁ (twiner g) ⟨$⟩ T.out-side b + ≈⟨ G.F-resp-≈ Equiv.refl (out-ertwines f) ⟩ + G.₁ (twiner g) ⟨$⟩ (G.₁ (twiner f) ⟨$⟩ T.out-side c) + ≈⟨ sym (G.₀ (T.rendezvous a)) (G.homomorphism (refl (G.₀ (T.rendezvous c)))) ⟩ + G.₁ (twiner f ∘ twiner g) ⟨$⟩ T.out-side c + ∎ } ; assoc = assoc ; sym-assoc = sym-assoc diff --git a/src/Categories/NaturalTransformation/Hom.agda b/src/Categories/NaturalTransformation/Hom.agda index 92f9ae0cd..a875579e4 100644 --- a/src/Categories/NaturalTransformation/Hom.agda +++ b/src/Categories/NaturalTransformation/Hom.agda @@ -21,17 +21,19 @@ private Hom[A,C]⇒Hom[B,C] : {A B : Obj} → (A ⇒ B) → NaturalTransformation Hom[ C ][-, A ] Hom[ C ][-, B ] Hom[A,C]⇒Hom[B,C] {A} A⇒B = ntHelper record { η = λ X → record { to = λ X⇒A → A⇒B ∘ X⇒A ; cong = ∘-resp-≈ʳ } - ; commute = λ f {g} → begin - A⇒B ∘ id ∘ g ∘ f ≈⟨ pullˡ id-comm ⟩ - (id ∘ A⇒B) ∘ g ∘ f ≈⟨ pullʳ sym-assoc ⟩ - id ∘ (A⇒B ∘ g) ∘ f ∎ + ; commute = λ f {g} {h} g≈h → begin + A⇒B ∘ id ∘ g ∘ f ≈⟨ sym-assoc ⟩ + (A⇒B ∘ id) ∘ g ∘ f ≈⟨ id-comm ⟩∘⟨ g≈h ⟩∘⟨refl ⟩ + (id ∘ A⇒B) ∘ h ∘ f ≈⟨ pullʳ sym-assoc ⟩ + id ∘ (A⇒B ∘ h) ∘ f ∎ } Hom[C,A]⇒Hom[C,B] : {A B : Obj} → (B ⇒ A) → NaturalTransformation Hom[ C ][ A ,-] Hom[ C ][ B ,-] Hom[C,A]⇒Hom[C,B] {A} B⇒A = ntHelper record { η = λ X → record { to = λ A⇒X → A⇒X ∘ B⇒A ; cong = ∘-resp-≈ˡ } - ; commute = λ f {g} → begin - (f ∘ g ∘ id) ∘ B⇒A ≈⟨ pullʳ (pullʳ id-comm-sym) ⟩ - f ∘ g ∘ B⇒A ∘ id ≈⟨ (refl⟩∘⟨ sym-assoc) ⟩ - f ∘ (g ∘ B⇒A) ∘ id ∎ + ; commute = λ f {g} {h} g≈h → begin + (f ∘ g ∘ id) ∘ B⇒A ≈⟨ pullʳ assoc ⟩ + f ∘ g ∘ id ∘ B⇒A ≈⟨ (refl⟩∘⟨ g≈h ⟩∘⟨ id-comm-sym) ⟩ + f ∘ h ∘ B⇒A ∘ id ≈⟨ (refl⟩∘⟨ sym-assoc) ⟩ + f ∘ (h ∘ B⇒A) ∘ id ∎ } diff --git a/src/Categories/NaturalTransformation/NaturalIsomorphism/Properties.agda b/src/Categories/NaturalTransformation/NaturalIsomorphism/Properties.agda index 20f26f193..1e931feb0 100644 --- a/src/Categories/NaturalTransformation/NaturalIsomorphism/Properties.agda +++ b/src/Categories/NaturalTransformation/NaturalIsomorphism/Properties.agda @@ -110,7 +110,7 @@ module _ {c ℓ ℓ′ e} {F G : Functor C (Setoids c ℓ)} (α : LiftSetoids { F⇒G = unlift-nat F⇒G ; F⇐G = unlift-nat F⇐G ; iso = λ X → record - { isoˡ = lower (iso.isoˡ X) - ; isoʳ = lower (iso.isoʳ X) + { isoˡ = λ eq → lower (iso.isoˡ X (lift eq)) + ; isoʳ = λ eq → lower (iso.isoʳ X (lift eq)) } } diff --git a/src/Categories/NaturalTransformation/Properties.agda b/src/Categories/NaturalTransformation/Properties.agda index 1d3a81bf7..e949043e8 100644 --- a/src/Categories/NaturalTransformation/Properties.agda +++ b/src/Categories/NaturalTransformation/Properties.agda @@ -108,5 +108,5 @@ module _ {c ℓ ℓ′ e} {F G : Functor C (Setoids c ℓ)} (α : NaturalTransfo { to = λ x → lower (to (η X) (lift x)) ; cong = λ eq → lower (cong (η X) (lift eq)) } - ; commute = λ f → lower (commute f) + ; commute = λ f eq → lower (commute f (lift eq)) } diff --git a/src/Categories/Yoneda.agda b/src/Categories/Yoneda.agda index fedb8a141..6dd4af653 100644 --- a/src/Categories/Yoneda.agda +++ b/src/Categories/Yoneda.agda @@ -10,7 +10,7 @@ module Categories.Yoneda where -- Hom[ Presheaves C] (Functor.F₀ embed a , F) ≅ Functor.F₀ F a -- as Setoids. In addition, Yoneda (yoneda) also says that this isomorphism is natural in a and F. open import Level -open import Function.Base using (_$_) renaming (id to id→) +open import Function.Base using (_$_) open import Function.Bundles using (Func; Inverse; _⟨$⟩_) open import Relation.Binary.Bundles using (module Setoid) import Relation.Binary.Reasoning.Setoid as SetoidR @@ -54,9 +54,9 @@ module Yoneda (C : Category o ℓ e) where embed = record { F₀ = Hom[ C ][-,_] ; F₁ = Hom[A,C]⇒Hom[B,C] -- A⇒B induces a NatTrans on the Homs. - ; identity = identityˡ - ; homomorphism = assoc - ; F-resp-≈ = λ f≈g → ∘-resp-≈ˡ f≈g + ; identity = identityˡ ○_ + ; homomorphism = λ h₁≈h₂ → ∘-resp-≈ʳ h₁≈h₂ ○ assoc + ; F-resp-≈ = λ f≈g h≈i → ∘-resp-≈ f≈g h≈i } -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor @@ -67,27 +67,27 @@ module Yoneda (C : Category o ℓ e) where ; from = λ x → ntHelper record { η = λ X → record { to = λ X⇒a → F.₁ X⇒a ⟨$⟩ x - ; cong = λ i≈j → F.F-resp-≈ i≈j + ; cong = λ i≈j → F.F-resp-≈ i≈j SE.refl } - ; commute = λ {X} {Y} Y⇒X {f} → + ; commute = λ {X} {Y} Y⇒X {f} {g} f≈g → let module SR = SetoidR (F.₀ Y) in SR.begin - F.₁ (id ∘ f ∘ Y⇒X) ⟨$⟩ x SR.≈⟨ F.F-resp-≈ identityˡ ⟩ - F.₁ (f ∘ Y⇒X) ⟨$⟩ x SR.≈⟨ F.homomorphism ⟩ - F.₁ Y⇒X ⟨$⟩ (F.₁ f ⟨$⟩ x) + F.₁ (id ∘ f ∘ Y⇒X) ⟨$⟩ x SR.≈⟨ F.F-resp-≈ (identityˡ ○ ∘-resp-≈ˡ f≈g) (SE.refl {x}) ⟩ + F.₁ (g ∘ Y⇒X) ⟨$⟩ x SR.≈⟨ F.homomorphism SE.refl ⟩ + F.₁ Y⇒X ⟨$⟩ (F.₁ g ⟨$⟩ x) SR.∎ } - ; to-cong = λ i≈j → i≈j - ; from-cong = λ x≈y → cong (F.₁ _) x≈y + ; to-cong = λ i≈j → i≈j CE.refl + ; from-cong = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j ; inverse = record - { fst = λ p → Setoid.trans (F.₀ a) p F.identity - ; snd = λ {nat} p {x} {f} → + { fst = λ p → Setoid.trans (F.₀ a) (p CE.refl) (F.identity SE.refl) + ; snd = λ {nat} p {x} {f} {g} f≈g → let module S = Setoid (F.₀ x) in S.trans (S.trans (cong (F.₁ f) p) - (sym-commute nat f)) - (cong (η nat x) (identityˡ ○ identityˡ)) + (sym-commute nat f CE.refl)) + (cong (η nat x) (identityˡ ○ identityˡ ○ f≈g)) } } where @@ -115,49 +115,53 @@ module Yoneda (C : Category o ℓ e) where { η = λ where (F , A) → record { to = λ α → lift (yoneda-inverse.to α) - ; cong = λ i≈j → lift i≈j + ; cong = λ i≈j → lift (i≈j CE.refl) } ; commute = λ where - {_} {G , B} (α , f) {β} → lift $ cong (η α B) (helper f β) + {_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ) } ; F⇐G = ntHelper record - { η = λ { (F , A) → record + { η = λ (F , A) → record { to = λ x → yoneda-inverse.from (lower x) - ; cong = λ x≈y → cong (Functor.F₁ F _) (lower x≈y) - } } - ; commute = λ { {F , X} (α , f) → helper′ α f (Setoid.refl (Functor.F₀ F X)) } + ; cong = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j) + } + ; commute = λ (α , f) eq eq′ → helper′ α f (lower eq) eq′ } - ; iso = λ { (F , A) → record - { isoˡ = λ {α} → yoneda-inverse.strictlyInverseʳ α - ; isoʳ = lift (Functor.identity F) - } } + ; iso = λ (F , A) → record + { isoˡ = λ {α β} i≈j {X} y≈z → + Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.strictlyInverseʳ α {x = X} y≈z) (i≈j CE.refl) + ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.strictlyInverseˡ {F = F} _) (lower eq)) + } } where helper : {F : Functor C.op (Setoids ℓ e)} {A B : Obj} (f : B ⇒ A) - (β : NaturalTransformation Hom[ C ][-, A ] F) → - Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ f ∘ id) (Functor.F₁ F f ⟨$⟩ (η β A ⟨$⟩ id)) - helper {F} {A} {B} f β = S.begin + (β γ : NaturalTransformation Hom[ C ][-, A ] F) → + Setoid._≈_ (Functor.F₀ Nat[Hom[C][-,c],F] (F , A)) β γ → + Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ f ∘ id) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id)) + helper {F} {A} {B} f β γ β≈γ = S.begin η β B ⟨$⟩ f ∘ id S.≈⟨ cong (η β B) (id-comm ○ (⟺ identityˡ)) ⟩ - η β B ⟨$⟩ id ∘ id ∘ f S.≈⟨ commute β f ⟩ - F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.∎ + η β B ⟨$⟩ id ∘ id ∘ f S.≈⟨ commute β f CE.refl ⟩ + F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩ + F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎ where module F = Functor F using (₀;₁) module S = SetoidR (F.₀ B) helper′ : ∀ {F G : Functor (Category.op C) (Setoids ℓ e)} {A B Z : Obj} - {h : Z ⇒ B} + {h i : Z ⇒ B} {X Y : Setoid.Carrier (Functor.F₀ F A)} (α : NaturalTransformation F G) (f : B ⇒ A) → Setoid._≈_ (Functor.F₀ F A) X Y → + h ≈ i → Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X))) - (η α Z ⟨$⟩ (Functor.F₁ F (f ∘ h) ⟨$⟩ Y)) - helper′ {F} {G} {A} {B} {Z} {h} {X} {Y} α f eq = S.begin - G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h ⟩ - η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈⟨ cong (η α Z) (cong (F.₁ h) (cong (F.₁ f) eq)) ⟩ - η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) F.homomorphism ⟩ - η α Z ⟨$⟩ (F.₁ (f ∘ h) ⟨$⟩ Y) S.∎ + (η α Z ⟨$⟩ (Functor.F₁ F (f ∘ i) ⟨$⟩ Y)) + helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin + G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h (S′.sym (cong (F.₁ f) eq)) ⟩ + η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) (F.F-resp-≈ eq′ S′.refl) ⟩ + η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) (F.homomorphism (Setoid.refl (F.₀ A))) ⟩ + η α Z ⟨$⟩ (F.₁ (f ∘ i) ⟨$⟩ Y) S.∎ where module F = Functor F using (₀; ₁; homomorphism; F-resp-≈) module G = Functor G using (₀; ₁) diff --git a/src/Categories/Yoneda/Continuous.agda b/src/Categories/Yoneda/Continuous.agda index 3c9817bb4..56bdcee41 100644 --- a/src/Categories/Yoneda/Continuous.agda +++ b/src/Categories/Yoneda/Continuous.agda @@ -1,27 +1,27 @@ {-# OPTIONS --without-K --safe #-} -open import Categories.Category using (Category; _[_,_]; _[_≈_]) +open import Categories.Category module Categories.Yoneda.Continuous {o ℓ e} (C : Category o ℓ e) where open import Function.Bundles using (Func; _⟨$⟩_) open import Relation.Binary using (Setoid) -open import Categories.Category.Construction.Cones using (Cones; Cone; Cone⇒) -open import Categories.Category.Construction.Presheaves using (Presheaves) -open import Categories.Diagram.Cone.Properties using (F-map-Coneˡ) -open import Categories.Diagram.Limit using (Limit) -open import Categories.Functor using (Functor; _∘F_) -open import Categories.Functor.Limits using (Continuous) -open import Categories.Functor.Hom using (module Hom) -open import Categories.Functor.Hom.Properties C using (hom-resp-limit) -open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Categories.Yoneda using (module Yoneda) +open import Categories.Category.Construction.Cones +open import Categories.Category.Construction.Presheaves +open import Categories.Diagram.Cone.Properties +open import Categories.Diagram.Limit +open import Categories.Functor +open import Categories.Functor.Limits +open import Categories.Functor.Hom +open import Categories.Functor.Hom.Properties C +open import Categories.NaturalTransformation +open import Categories.Yoneda import Categories.Morphism.Reasoning as MR open Hom C -open Yoneda C using (embed) +open Yoneda C private module C = Category C @@ -55,7 +55,7 @@ module _ {o′ ℓ′ e′} {J : Category o′ ℓ′ e′} {F : Functor J C} (L { N = K.N.₀ X ; apex = record { ψ = λ j → K.ψ.η j X - ; commute = λ f → C.∘-resp-≈ʳ C.identityʳ ○ K.commute f + ; commute = λ f eq → C.∘-resp-≈ʳ C.identityʳ ○ K.commute f eq } } @@ -63,17 +63,17 @@ module _ {o′ ℓ′ e′} {J : Category o′ ℓ′ e′} {F : Functor J C} (L ! = record { arr = ntHelper record { η = λ X → Cone⇒.arr (HomL.terminal.! X {KHF X}) - ; commute = λ {X Y} f {x} → L.terminal.!-unique record + ; commute = λ {X Y} f {x y} eq → L.terminal.!-unique record { arr = C.id C.∘ L.rep _ C.∘ f ; commute = λ {j} → begin L.proj j C.∘ C.id C.∘ L.rep _ C.∘ f ≈⟨ refl⟩∘⟨ C.identityˡ ⟩ L.proj j C.∘ L.rep _ C.∘ f ≈⟨ pullˡ L.commute ⟩ - (K.ψ.η j X ⟨$⟩ x) C.∘ f ≈˘⟨ C.identityˡ ⟩ - C.id C.∘ (K.ψ.η j X ⟨$⟩ x) C.∘ f ≈˘⟨ K.ψ.commute j f ⟩ + (K.ψ.η j X ⟨$⟩ y) C.∘ f ≈˘⟨ C.identityˡ ⟩ + C.id C.∘ (K.ψ.η j X ⟨$⟩ y) C.∘ f ≈˘⟨ K.ψ.commute j f eq ⟩ K.ψ.η j Y ⟨$⟩ (K.N.₁ f ⟨$⟩ x) ∎ } } - ; commute = L.commute + ; commute = λ eq → L.commute ○ Func.cong (K.ψ.η _ _) eq } module _ (f : Cones yF [ K , ⊤ ]) where @@ -83,9 +83,9 @@ module _ {o′ ℓ′ e′} {J : Category o′ ℓ′ e′} {F : Functor J C} (L module arr = NaturalTransformation arr !-unique : Cones yF [ ! ≈ f ] - !-unique {X} {x} = L.terminal.!-unique record - { arr = f.arr.η X ⟨$⟩ x - ; commute = f.commute + !-unique {X} {x} {y} eq = L.terminal.!-unique record + { arr = f.arr.η X ⟨$⟩ y + ; commute = f.commute (Setoid.sym (K.N.₀ X) eq) } embed-resp-limit : Limit yF diff --git a/src/Categories/Yoneda/Properties.agda b/src/Categories/Yoneda/Properties.agda index 2a0ff0eb4..2229b9537 100644 --- a/src/Categories/Yoneda/Properties.agda +++ b/src/Categories/Yoneda/Properties.agda @@ -36,16 +36,17 @@ private module C = Category C using (op; id) YoFull : Full embed -YoFull {X} {Y} ε = Func.to (η ε X) id , λ {A} {x} → begin - Func.to (η ε X) id ∘ x ≈˘⟨ identityˡ ⟩ - id ∘ Func.to (η ε X) id ∘ x ≈⟨ sym-commute ε x ⟩ - Func.to (η ε A) (id ∘ id ∘ x) ≈⟨ Func.cong (η ε A) (identityˡ ○ identityˡ) ⟩ - Func.to (η ε A) x ∎ +YoFull {X} {Y} ε = Func.to (η ε X) id , λ {A} {x} {y} x≈y → begin + Func.to (η ε X) id ∘ x ≈⟨ refl⟩∘⟨ x≈y ⟩ + Func.to (η ε X) id ∘ y ≈˘⟨ identityˡ ⟩ + id ∘ Func.to (η ε X) id ∘ y ≈⟨ sym-commute ε y CE.refl ⟩ + Func.to (η ε A) (id ∘ id ∘ y) ≈⟨ Func.cong (η ε A) (identityˡ ○ identityˡ) ⟩ + Func.to (η ε A) y ∎ YoFaithful : Faithful embed YoFaithful {X} {Y} {f} {g} p = begin f ≈˘⟨ identityʳ ⟩ - f ∘ id ≈⟨ p ⟩ + f ∘ id ≈⟨ p CE.refl ⟩ g ∘ id ≈⟨ identityʳ ⟩ g ∎ @@ -61,13 +62,13 @@ yoneda-iso {A} {B} niso = record ; iso = record { isoˡ = begin (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id) ≈˘⟨ identityˡ ⟩ - C.id ∘ Func.to (⇐.η B) id ∘ Func.to (⇒.η A) id ≈⟨ B⇒A.strictlyInverseʳ F⇐G ⟩ - Func.to (⇐.η A) (Func.to (⇒.η A) id) ≈⟨ iso.isoˡ A ⟩ + C.id ∘ Func.to (⇐.η B) id ∘ Func.to (⇒.η A) id ≈⟨ B⇒A.strictlyInverseʳ F⇐G CE.refl ⟩ + Func.to (⇐.η A) (Func.to (⇒.η A) id) ≈⟨ iso.isoˡ A CE.refl ⟩ id ∎ ; isoʳ = begin Func.to (⇒.η A) C.id ∘ Func.to (⇐.η B) C.id ≈˘⟨ identityˡ ⟩ - C.id ∘ Func.to (⇒.η A) id ∘ Func.to (⇐.η B) C.id ≈⟨ A⇒B.strictlyInverseʳ F⇒G ⟩ - Func.to (⇒.η B) (Func.to (⇐.η B) id) ≈⟨ iso.isoʳ B ⟩ + C.id ∘ Func.to (⇒.η A) id ∘ Func.to (⇐.η B) C.id ≈⟨ A⇒B.strictlyInverseʳ F⇒G CE.refl ⟩ + Func.to (⇒.η B) (Func.to (⇐.η B) id) ≈⟨ iso.isoʳ B CE.refl ⟩ id ∎ } } @@ -96,18 +97,18 @@ module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where NaturalTransformation Hom[ C ][-, F.₀ X ] Hom[ C ][-, G.₀ X ] nat-appʳ X α = ntHelper record { η = λ Y → η α (Y , X) - ; commute = λ {_ Y} f → Func.cong (η α (Y , X)) (∘-resp-≈ˡ (⟺ F.identity)) ○ commute α (f , D.id) ○ ∘-resp-≈ˡ G.identity + ; commute = λ {_ Y} f eq → Func.cong (η α (Y , X)) (∘-resp-≈ˡ (⟺ F.identity)) ○ commute α (f , D.id) eq ○ ∘-resp-≈ˡ G.identity } transform : NaturalTransformation Hom[-,F-] Hom[-,G-] → NaturalTransformation F G transform α = ntHelper record { η = λ X → η α (F.₀ X , X) ⟨$⟩ id ; commute = λ {X Y} f → begin - (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f ≈˘⟨ identityˡ ⟩ - id ∘ (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ Y ] , _} (idN , F.₁ f) {nat-appʳ Y α}) ⟩ + (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f ≈˘⟨ identityˡ ⟩ + id ∘ (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ Y ] , _} (idN , F.₁ f) {nat-appʳ Y α} {nat-appʳ Y α} (Func.cong (η α _))) ⟩ η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id ≈⟨ Func.cong (η α (F.₀ X , Y)) (∘-resp-≈ʳ (⟺ identityˡ)) ⟩ - η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id ∘ id ≈⟨ commute α (id , f) ⟩ - G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id ∘ id ≈⟨ commute α (id , f) CE.refl ⟩ + G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id) ∎ } @@ -133,17 +134,21 @@ module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ (⇒.η (F.₀ X , X) ⟨$⟩ id) ≈⟨ introˡ CE.refl ⟩ id ∘ (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ (⇒.η (F.₀ X , X) ⟨$⟩ id) ≈˘⟨ lower {e} (yoneda.⇒.commute {Y = Hom[ C ][-, F.₀ X ] , _} (idN , (⇒.η (F.₀ X , X) ⟨$⟩ id)) - {nat-appʳ {F = G} {F} X F⇐G} ) ⟩ + {nat-appʳ {F = G} {F} X F⇐G} + {nat-appʳ {F = G} {F} X F⇐G} + (Func.cong (⇐.η (_ , X) ))) ⟩ ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ id ≈⟨ Func.cong (⇐.η _) identityʳ ⟩ - ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id) ≈⟨ iso.isoˡ _ ⟩ + ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id) ≈⟨ iso.isoˡ _ CE.refl ⟩ id ∎ ; isoʳ = begin (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ (⇐.η (G.₀ X , X) ⟨$⟩ id) ≈⟨ introˡ CE.refl ⟩ id ∘ (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ (⇐.η (G.₀ X , X) ⟨$⟩ id) ≈˘⟨ lower {e} (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ X ] , _} (idN , (⇐.η (G.₀ X , X) ⟨$⟩ C.id)) - {nat-appʳ {F = F} {G} X F⇒G} ) ⟩ + {nat-appʳ {F = F} {G} X F⇒G} + {nat-appʳ {F = F} {G} X F⇒G} + (Func.cong (⇒.η _))) ⟩ ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ id ≈⟨ Func.cong (⇒.η _) identityʳ ⟩ - ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id) ≈⟨ iso.isoʳ _ ⟩ + ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id) ≈⟨ iso.isoʳ _ CE.refl ⟩ id ∎ } } diff --git a/src/Function/Construct/Setoid.agda b/src/Function/Construct/Setoid.agda index a89cdbfaf..3d098a5a9 100644 --- a/src/Function/Construct/Setoid.agda +++ b/src/Function/Construct/Setoid.agda @@ -14,18 +14,19 @@ module Function.Construct.Setoid where variable a₁ a₂ b₁ b₂ c₁ c₂ : Level - setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _ - setoid From To = record + function : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _ + function From To = record { Carrier = Func From To - ; _≈_ = λ f g → ∀ {x} → f ⟨$⟩ x To.≈ g ⟨$⟩ x + ; _≈_ = λ f g → ∀ {x y} → x From.≈ y → f ⟨$⟩ x To.≈ g ⟨$⟩ y ; isEquivalence = record - { refl = To.refl - ; sym = λ f≈g → To.sym f≈g - ; trans = λ f≈g g≈h → To.trans f≈g g≈h + { refl = λ {f} x≈y → Func.cong f x≈y + ; sym = λ {f} {g} fx≈gy x≈y → To.sym (fx≈gy (From.sym x≈y)) + ; trans = λ {f} {g} {h} fx≈gy gx≈hy x≈y → To.trans (fx≈gy x≈y) (gx≈hy From.refl) } } where module To = Setoid To + module From = Setoid From -- This doesn't really belong here, it should be in Function.Construct.Composition but that's in stdlib -- so will need to be contributed to there first.