From 3553722340bd8cb5f42b6abefedc3ac653d383bf Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 16 Feb 2021 07:39:11 -0800 Subject: [PATCH 1/9] Add a nicer definition of pullbacks in Setoid --- .../Properties/Setoids/Limits/Canonical.agda | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda new file mode 100644 index 000000000..1f907918e --- /dev/null +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --without-K --safe #-} + +-- A "canonical" presentation of limits in Setoid. +-- +-- These limits are obviously isomorphic to those created by +-- the Completeness proof, but are far less unweildy to work with. + +module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where + +open import Level + +open import Data.Product using (_,_; _×_) + +open import Relation.Binary.Bundles using (Setoid) +open import Function.Equality as SΠ renaming (id to ⟶-id) +import Relation.Binary.Reasoning.Setoid as SR + +open import Categories.Diagram.Pullback + +open import Categories.Category.Instance.Setoids + +open Setoid renaming (_≈_ to [_][_≈_]) + +-------------------------------------------------------------------------------- +-- Pullbacks + +record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : Set (o ⊔ ℓ) where + field + elem₁ : Carrier X + elem₂ : Carrier Y + commute : [ Z ][ f ⟨$⟩ elem₁ ≈ g ⟨$⟩ elem₂ ] + +open FiberProduct + +pullback : ∀ {o ℓ} {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g +pullback {X = X} {Y = Y} {Z = Z} f g = record + { P = record + { Carrier = FiberProduct f g + ; _≈_ = λ p q → [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ] + ; isEquivalence = record + { refl = (refl X) , (refl Y) + ; sym = λ (eq₁ , eq₂) → sym X eq₁ , sym Y eq₂ + ; trans = λ (eq₁ , eq₂) (eq₁′ , eq₂′) → (trans X eq₁ eq₁′) , (trans Y eq₂ eq₂′) + } + } + ; p₁ = record { _⟨$⟩_ = elem₁ ; cong = λ (eq₁ , _) → eq₁ } + ; p₂ = record { _⟨$⟩_ = elem₂ ; cong = λ (_ , eq₂) → eq₂ } + ; isPullback = record + { commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q) + ; universal = λ {A} {h₁} {h₂} eq → record + { _⟨$⟩_ = λ a → record + { elem₁ = h₁ ⟨$⟩ a + ; elem₂ = h₂ ⟨$⟩ a + ; commute = eq (refl A) + } + ; cong = λ eq → cong h₁ eq , cong h₂ eq } + ; 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 + } + } From eb93b061aafd2fed974ea31fdf550c5118f1c472 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 16 Feb 2021 07:58:06 -0800 Subject: [PATCH 2/9] Add some nicer notation for coherence morphisms in a bicategory --- src/Categories/Bicategory.agda | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/Categories/Bicategory.agda b/src/Categories/Bicategory.agda index 7af8034db..ce03907fd 100644 --- a/src/Categories/Bicategory.agda +++ b/src/Categories/Bicategory.agda @@ -63,6 +63,29 @@ record Bicategory o ℓ e t : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where _▷_ : {A B C : Obj} {f g : A ⇒₁ B} (h : B ⇒₁ C) (α : f ⇒₂ g) → h ∘ₕ f ⇒₂ h ∘ₕ g _ ▷ α = id₂ ⊚₁ α + -- Coherence morphisms + unitˡ⇒ : {A B : Obj} {f : A ⇒₁ B} → id₁ ⊚₀ f ⇒₂ f + unitˡ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitˡ (_ , f) + + unitˡ⇐ : {A B : Obj} {f : A ⇒₁ B} → f ⇒₂ id₁ ⊚₀ f + unitˡ⇐ {_} {_} {f} = NaturalIsomorphism.⇐.η unitˡ (_ , f) + + unitʳ⇒ : {A B : Obj} {f : A ⇒₁ B} → f ⊚₀ id₁ ⇒₂ f + unitʳ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitʳ (f , _) + + unitʳ⇐ : {A B : Obj} {f : A ⇒₁ B} → f ⇒₂ f ⊚₀ id₁ + unitʳ⇐ {_} {_} {f} = NaturalIsomorphism.⇐.η unitʳ (f , _) + + assoc⇒ : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} → + ((f ⊚₀ g) ⊚₀ h) ⇒₂ (f ⊚₀ (g ⊚₀ h)) + assoc⇒ {_} {_} {_} {_} {f} {g} {h} = NaturalIsomorphism.⇒.η ⊚-assoc ((f , g) , h) + + assoc⇐ : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} → + (f ⊚₀ (g ⊚₀ h)) ⇒₂ ((f ⊚₀ g) ⊚₀ h) + assoc⇐ {_} {_} {_} {_} {f} {g} {h} = NaturalIsomorphism.⇐.η ⊚-assoc ((f , g) , h) + + + -- Abbreviations of some longer names for local use private λ⇒ : {A B : Obj} {f : A ⇒₁ B} → id₁ ⊚₀ f hom.⇒ f λ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitˡ (_ , f) From 1f48be123500d4e866a39141499028c9f6b39985 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 16 Feb 2021 07:58:29 -0800 Subject: [PATCH 3/9] Define Monads in a bicategory --- src/Categories/Bicategory/Monad.agda | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 src/Categories/Bicategory/Monad.agda diff --git a/src/Categories/Bicategory/Monad.agda b/src/Categories/Bicategory/Monad.agda new file mode 100644 index 000000000..0d16a72a5 --- /dev/null +++ b/src/Categories/Bicategory/Monad.agda @@ -0,0 +1,26 @@ +{-# OPTIONS --without-K --safe #-} + +-- A Monad in a Bicategory. +-- For the more elementary version of Monads, see 'Categories.Monad'. +module Categories.Bicategory.Monad where + +open import Level +open import Data.Product using (_,_) + +open import Categories.Bicategory +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) + + +record Monad {o ℓ e t} (𝒞 : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e ⊔ t) where + open Bicategory 𝒞 + + field + C : Obj + T : C ⇒₁ C + η : id₁ ⇒₂ T + μ : (T ⊚₀ T) ⇒₂ T + + assoc : μ ∘ᵥ (T ▷ μ) ∘ᵥ assoc⇒ ≈ (μ ∘ᵥ (μ ◁ T)) + sym-assoc : μ ∘ᵥ (μ ◁ T) ∘ᵥ assoc⇐ ≈ (μ ∘ᵥ (T ▷ μ)) + identityˡ : μ ∘ᵥ (T ▷ η) ∘ᵥ unitʳ⇐ ≈ id₂ + identityʳ : μ ∘ᵥ (η ◁ T) ∘ᵥ unitˡ⇐ ≈ id₂ From 440ffba4f7673850ce8a94f6568a8a9c99e2e83a Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 16 Feb 2021 08:31:52 -0800 Subject: [PATCH 4/9] Add explicit levels to Setoids Canonical pullbac --- .../Instance/Properties/Setoids/Limits/Canonical.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda index 1f907918e..fb7b15aec 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -32,8 +32,8 @@ record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : open FiberProduct -pullback : ∀ {o ℓ} {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g -pullback {X = X} {Y = Y} {Z = Z} f g = record +pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g +pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record { P = record { Carrier = FiberProduct f g ; _≈_ = λ p q → [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ] From 9437e96696fd3034a09d196c714e13ce69fe03d7 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Tue, 16 Feb 2021 08:33:24 -0800 Subject: [PATCH 5/9] Show that monads in Span are categories --- .../Construction/Spans/Properties.agda | 133 ++++++++++++++++++ 1 file changed, 133 insertions(+) create mode 100644 src/Categories/Bicategory/Construction/Spans/Properties.agda diff --git a/src/Categories/Bicategory/Construction/Spans/Properties.agda b/src/Categories/Bicategory/Construction/Spans/Properties.agda new file mode 100644 index 000000000..bd73d1d92 --- /dev/null +++ b/src/Categories/Bicategory/Construction/Spans/Properties.agda @@ -0,0 +1,133 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Bicategory.Construction.Spans.Properties where + +open import Level + +open import Data.Product using (_,_; _×_) +open import Relation.Binary.Bundles using (Setoid) +import Relation.Binary.Reasoning.Setoid as SR +open import Function.Equality as SΠ renaming (id to ⟶-id) + +open import Categories.Category +open import Categories.Category.Helper +open import Categories.Category.Instance.Setoids +open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical + +open import Categories.Diagram.Pullback + +open import Categories.Bicategory +open import Categories.Bicategory.Monad + +import Categories.Category.Diagram.Span as Span +import Categories.Bicategory.Construction.Spans as Spans + +-------------------------------------------------------------------------------- +-- Monads in the Bicategory of Spans are Categories + +module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where + + private + module T = Monad T + + open Span (Setoids (o ⊔ ℓ) ℓ) + open Spans (pullback o ℓ) + open Span⇒ + open Bicategory Spans + + open Setoid renaming (_≈_ to [_][_≈_]) + + + -- We can view the roof of the span as a hom set! However, we need to partition + -- this big set up into small chunks with known domains/codomains. + record Hom (X Y : Carrier T.C) : Set (o ⊔ ℓ) where + field + hom : Carrier (Span.M T.T) + dom-eq : [ T.C ][ Span.dom T.T ⟨$⟩ hom ≈ X ] + cod-eq : [ T.C ][ Span.cod T.T ⟨$⟩ hom ≈ Y ] + + open Hom + + private + ObjSetoid : Setoid (o ⊔ ℓ) ℓ + ObjSetoid = T.C + + HomSetoid : Setoid (o ⊔ ℓ) ℓ + HomSetoid = Span.M T.T + + module ObjSetoid = Setoid ObjSetoid + module HomSetoid = Setoid HomSetoid + + id⇒ : (X : Carrier T.C) → Hom X X + id⇒ X = record + { hom = arr T.η ⟨$⟩ X + ; 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) + _×ₚ_ {B = B} f g = record + { elem₁ = hom g + ; elem₂ = hom f + ; commute = begin + Span.cod T.T ⟨$⟩ hom g ≈⟨ cod-eq g ⟩ + B ≈⟨ ObjSetoid.sym (dom-eq f) ⟩ + Span.dom T.T ⟨$⟩ hom f ∎ + } + where + open SR ObjSetoid + + _∘⇒_ : ∀ {A B C} (f : Hom B C) → (g : Hom A B) → Hom A C + _∘⇒_ {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} {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} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl) ⟩ + Span.cod T.T ⟨$⟩ hom f ≈⟨ cod-eq f ⟩ + C ∎ + } + where + open SR ObjSetoid + + SpanMonad⇒Category : Category (o ⊔ ℓ) (o ⊔ ℓ) ℓ + SpanMonad⇒Category = categoryHelper record + { Obj = Setoid.Carrier T.C + ; _⇒_ = Hom + ; _≈_ = λ f g → [ HomSetoid ][ hom f ≈ hom g ] + ; id = λ {X} → id⇒ X + ; _∘_ = _∘⇒_ + ; assoc = λ {A} {B} {C} {D} {f} {g} {h} → + let f×ₚ⟨g×ₚh⟩ = record + { elem₁ = record + { elem₁ = hom f + ; elem₂ = hom g + ; commute = FiberProduct.commute (g ×ₚ f) + } + ; elem₂ = hom h + ; commute = FiberProduct.commute (h ×ₚ g) + } + 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⟩} {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ʳ 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ˡ HomSetoid.refl ⟩ + hom f ∎ + ; equiv = record + { refl = HomSetoid.refl + ; sym = HomSetoid.sym + ; trans = HomSetoid.trans + } + ; ∘-resp-≈ = λ f≈h g≈i → cong (arr T.μ) (g≈i , f≈h) + } + where + open SR HomSetoid From 277dcdd5225dc66ad40180fb6c0e0039743de929 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 17 Feb 2021 09:04:23 -0800 Subject: [PATCH 6/9] Remove coherence helpers in Categories.Bicategory These are already found in Categories.Bicategory.Extras --- src/Categories/Bicategory.agda | 23 ----------------------- src/Categories/Bicategory/Monad.agda | 11 ++++++----- 2 files changed, 6 insertions(+), 28 deletions(-) diff --git a/src/Categories/Bicategory.agda b/src/Categories/Bicategory.agda index ce03907fd..7af8034db 100644 --- a/src/Categories/Bicategory.agda +++ b/src/Categories/Bicategory.agda @@ -63,29 +63,6 @@ record Bicategory o ℓ e t : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where _▷_ : {A B C : Obj} {f g : A ⇒₁ B} (h : B ⇒₁ C) (α : f ⇒₂ g) → h ∘ₕ f ⇒₂ h ∘ₕ g _ ▷ α = id₂ ⊚₁ α - -- Coherence morphisms - unitˡ⇒ : {A B : Obj} {f : A ⇒₁ B} → id₁ ⊚₀ f ⇒₂ f - unitˡ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitˡ (_ , f) - - unitˡ⇐ : {A B : Obj} {f : A ⇒₁ B} → f ⇒₂ id₁ ⊚₀ f - unitˡ⇐ {_} {_} {f} = NaturalIsomorphism.⇐.η unitˡ (_ , f) - - unitʳ⇒ : {A B : Obj} {f : A ⇒₁ B} → f ⊚₀ id₁ ⇒₂ f - unitʳ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitʳ (f , _) - - unitʳ⇐ : {A B : Obj} {f : A ⇒₁ B} → f ⇒₂ f ⊚₀ id₁ - unitʳ⇐ {_} {_} {f} = NaturalIsomorphism.⇐.η unitʳ (f , _) - - assoc⇒ : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} → - ((f ⊚₀ g) ⊚₀ h) ⇒₂ (f ⊚₀ (g ⊚₀ h)) - assoc⇒ {_} {_} {_} {_} {f} {g} {h} = NaturalIsomorphism.⇒.η ⊚-assoc ((f , g) , h) - - assoc⇐ : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} → - (f ⊚₀ (g ⊚₀ h)) ⇒₂ ((f ⊚₀ g) ⊚₀ h) - assoc⇐ {_} {_} {_} {_} {f} {g} {h} = NaturalIsomorphism.⇐.η ⊚-assoc ((f , g) , h) - - - -- Abbreviations of some longer names for local use private λ⇒ : {A B : Obj} {f : A ⇒₁ B} → id₁ ⊚₀ f hom.⇒ f λ⇒ {_} {_} {f} = NaturalIsomorphism.⇒.η unitˡ (_ , f) diff --git a/src/Categories/Bicategory/Monad.agda b/src/Categories/Bicategory/Monad.agda index 0d16a72a5..b78750c06 100644 --- a/src/Categories/Bicategory/Monad.agda +++ b/src/Categories/Bicategory/Monad.agda @@ -8,11 +8,12 @@ open import Level open import Data.Product using (_,_) open import Categories.Bicategory +import Categories.Bicategory.Extras as Bicat open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) record Monad {o ℓ e t} (𝒞 : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e ⊔ t) where - open Bicategory 𝒞 + open Bicat 𝒞 field C : Obj @@ -20,7 +21,7 @@ record Monad {o ℓ e t} (𝒞 : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e η : id₁ ⇒₂ T μ : (T ⊚₀ T) ⇒₂ T - assoc : μ ∘ᵥ (T ▷ μ) ∘ᵥ assoc⇒ ≈ (μ ∘ᵥ (μ ◁ T)) - sym-assoc : μ ∘ᵥ (μ ◁ T) ∘ᵥ assoc⇐ ≈ (μ ∘ᵥ (T ▷ μ)) - identityˡ : μ ∘ᵥ (T ▷ η) ∘ᵥ unitʳ⇐ ≈ id₂ - identityʳ : μ ∘ᵥ (η ◁ T) ∘ᵥ unitˡ⇐ ≈ id₂ + assoc : μ ∘ᵥ (T ▷ μ) ∘ᵥ associator.from ≈ (μ ∘ᵥ (μ ◁ T)) + sym-assoc : μ ∘ᵥ (μ ◁ T) ∘ᵥ associator.to ≈ (μ ∘ᵥ (T ▷ μ)) + identityˡ : μ ∘ᵥ (T ▷ η) ∘ᵥ unitorʳ.to ≈ id₂ + identityʳ : μ ∘ᵥ (η ◁ T) ∘ᵥ unitorˡ.to ≈ id₂ From 4e596c950a6f49bb6ea0b34e36719764a4c4c345 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 17 Feb 2021 09:05:01 -0800 Subject: [PATCH 7/9] Add note clarifying the location of an isomorphism proof --- .../Category/Instance/Properties/Setoids/Limits/Canonical.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda index fb7b15aec..5d746ca2f 100644 --- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda +++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda @@ -4,6 +4,7 @@ -- -- These limits are obviously isomorphic to those created by -- the Completeness proof, but are far less unweildy to work with. +-- This isomorphism is witnessed by Categories.Diagram.Pullback.up-to-iso module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where From 9aaa7bca8bddc24f5216493dae25b79bbba2239d Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 17 Feb 2021 09:44:23 -0800 Subject: [PATCH 8/9] Show that Bicategorical Monads in Cat are elementary monads --- .../Bicategory/Monad/Properties.agda | 95 +++++++++++++++++++ 1 file changed, 95 insertions(+) create mode 100644 src/Categories/Bicategory/Monad/Properties.agda diff --git a/src/Categories/Bicategory/Monad/Properties.agda b/src/Categories/Bicategory/Monad/Properties.agda new file mode 100644 index 000000000..326b1edd4 --- /dev/null +++ b/src/Categories/Bicategory/Monad/Properties.agda @@ -0,0 +1,95 @@ +{-# OPTIONS --without-K --safe #-} +module Categories.Bicategory.Monad.Properties where + +open import Categories.Category +open import Categories.Bicategory.Instance.Cats +open import Categories.NaturalTransformation using (NaturalTransformation) +open import Categories.Functor using (Functor) + +import Categories.Bicategory.Monad as BicatMonad +import Categories.Monad as ElemMonad + +import Categories.Morphism.Reasoning as MR + +-------------------------------------------------------------------------------- +-- Bicategorical Monads in Cat are the same as the more elementary +-- definition of Monads. +-- +-- NOTE: + +CatMonad⇒Monad : ∀ {o ℓ e} → (T : BicatMonad.Monad (Cats o ℓ e)) → ElemMonad.Monad (BicatMonad.Monad.C T) +CatMonad⇒Monad T = record + { F = T.T + ; η = T.η + ; μ = T.μ + ; assoc = λ {X} → begin + η T.μ X ∘ F₁ T.T (η T.μ X) ≈⟨ intro-ids ⟩ + (η T.μ X ∘ (F₁ T.T (η T.μ X) ∘ id) ∘ id) ≈⟨ T.assoc ⟩ + (η T.μ X ∘ F₁ T.T id ∘ η T.μ (F₀ T.T X)) ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ˡ (identity T.T) ○ identityˡ) ⟩ + η T.μ X ∘ η T.μ (F₀ T.T X) ∎ + ; sym-assoc = λ {X} → begin + η T.μ X ∘ η T.μ (F₀ T.T X) ≈⟨ intro-F-ids ⟩ + η T.μ X ∘ (F₁ T.T id ∘ η T.μ (F₀ T.T X)) ∘ id ≈⟨ T.sym-assoc ⟩ + η T.μ X ∘ F₁ T.T (η T.μ X) ∘ id ≈⟨ ∘-resp-≈ʳ identityʳ ⟩ + η T.μ X ∘ F₁ T.T (η T.μ X) ∎ + ; identityˡ = λ {X} → begin + η T.μ X ∘ F₁ T.T (η T.η X) ≈⟨ intro-ids ⟩ + η T.μ X ∘ (F₁ T.T (η T.η X) ∘ id) ∘ id ≈⟨ T.identityˡ ⟩ + id ∎ + ; identityʳ = λ {X} → begin + η T.μ X ∘ η T.η (F₀ T.T X) ≈⟨ intro-F-ids ⟩ + η T.μ X ∘ (F₁ T.T id ∘ η T.η (F₀ T.T X)) ∘ id ≈⟨ T.identityʳ ⟩ + id ∎ + } + where + module T = BicatMonad.Monad T + open Category (BicatMonad.Monad.C T) + open HomReasoning + open Equiv + open MR (BicatMonad.Monad.C T) + + open NaturalTransformation + open Functor + + intro-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → f ∘ g ≈ f ∘ (g ∘ id) ∘ id + intro-ids = ⟺ (∘-resp-≈ʳ identityʳ) ○ ⟺ (∘-resp-≈ʳ identityʳ) + + intro-F-ids : ∀ {X Y Z} {f : F₀ T.T Y ⇒ Z} {g : X ⇒ F₀ T.T Y} → f ∘ g ≈ f ∘ (F₁ T.T id ∘ g) ∘ id + intro-F-ids = ∘-resp-≈ʳ (⟺ identityˡ ○ ⟺ (∘-resp-≈ˡ (identity T.T))) ○ ⟺ (∘-resp-≈ʳ identityʳ) + +Monad⇒CatMonad : ∀ {o ℓ e} {𝒞 : Category o ℓ e} → (T : ElemMonad.Monad 𝒞) → BicatMonad.Monad (Cats o ℓ e) +Monad⇒CatMonad {𝒞 = 𝒞} T = record + { C = 𝒞 + ; T = T.F + ; η = T.η + ; μ = T.μ + ; assoc = λ {X} → begin + T.μ.η X ∘ (T.F.F₁ (T.μ.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩ + T.μ.η X ∘ T.F.F₁ (T.μ.η X) ≈⟨ T.assoc ⟩ + T.μ.η X ∘ T.μ.η (T.F.F₀ X) ≈⟨ ∘-resp-≈ʳ (⟺ identityˡ ○ ∘-resp-≈ˡ (⟺ T.F.identity)) ⟩ + T.μ.η X ∘ T.F.F₁ id ∘ T.μ.η (T.F.F₀ X) ∎ + ; sym-assoc = λ {X} → begin + T.μ.η X ∘ (T.F.F₁ id ∘ T.μ.η (T.F.F₀ X)) ∘ id ≈⟨ eliminate-F-ids ⟩ + T.μ.η X ∘ T.μ.η (T.F.F₀ X) ≈⟨ T.sym-assoc ⟩ + T.μ.η X ∘ T.F.F₁ (T.μ.η X) ≈⟨ ∘-resp-≈ʳ (⟺ identityʳ) ⟩ + T.μ.η X ∘ T.F.F₁ (T.μ.η X) ∘ id ∎ + ; identityˡ = λ {X} → begin + T.μ.η X ∘ (T.F.F₁ (T.η.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩ + T.μ.η X ∘ T.F.F₁ (T.η.η X) ≈⟨ T.identityˡ ⟩ + id ∎ + ; identityʳ = λ {X} → begin + (T.μ.η X ∘ (T.F.F₁ id ∘ T.η.η (T.F.F₀ X)) ∘ id) ≈⟨ eliminate-F-ids ⟩ + T.μ.η X ∘ T.η.η (T.F.F₀ X) ≈⟨ T.identityʳ ⟩ + id ∎ + } + where + module T = ElemMonad.Monad T + open Category 𝒞 + open HomReasoning + open MR 𝒞 + + eliminate-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → f ∘ (g ∘ id) ∘ id ≈ f ∘ g + eliminate-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ identityʳ + + eliminate-F-ids : ∀ {X Y Z} {f : T.F.F₀ Y ⇒ Z} {g : X ⇒ T.F.F₀ Y} → f ∘ (T.F.F₁ id ∘ g) ∘ id ≈ f ∘ g + eliminate-F-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ (∘-resp-≈ˡ T.F.identity ○ identityˡ) From 462899fd0bb719bb540d7b9eb74ac2c4cae0e53b Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 17 Feb 2021 09:46:03 -0800 Subject: [PATCH 9/9] Remove vestigial note --- src/Categories/Bicategory/Monad/Properties.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Categories/Bicategory/Monad/Properties.agda b/src/Categories/Bicategory/Monad/Properties.agda index 326b1edd4..c4df88c1b 100644 --- a/src/Categories/Bicategory/Monad/Properties.agda +++ b/src/Categories/Bicategory/Monad/Properties.agda @@ -14,8 +14,6 @@ import Categories.Morphism.Reasoning as MR -------------------------------------------------------------------------------- -- Bicategorical Monads in Cat are the same as the more elementary -- definition of Monads. --- --- NOTE: CatMonad⇒Monad : ∀ {o ℓ e} → (T : BicatMonad.Monad (Cats o ℓ e)) → ElemMonad.Monad (BicatMonad.Monad.C T) CatMonad⇒Monad T = record