From cb2efa506d9ecec48aad72deb10acb6ffba45970 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 8 Dec 2025 15:30:53 -0600 Subject: Update category of cospans --- Category/Diagram/Cospan.agda | 117 ++++++++++++++++++++++++++++ Category/Instance/Cospans.agda | 87 +-------------------- Category/Instance/DecoratedCospans.agda | 17 ++-- Category/Instance/FinitelyCocompletes.agda | 19 ++--- Cospan/Decorated.agda | 2 +- Functor/Instance/Cospan/Embed.agda | 103 ++++++++++++------------ Functor/Instance/Cospan/Stack.agda | 96 +++++++++++------------ Functor/Instance/Decorate.agda | 29 ++++--- Functor/Instance/DecoratedCospan/Embed.agda | 10 +-- Functor/Instance/DecoratedCospan/Stack.agda | 41 +++++----- 10 files changed, 275 insertions(+), 246 deletions(-) create mode 100644 Category/Diagram/Cospan.agda diff --git a/Category/Diagram/Cospan.agda b/Category/Diagram/Cospan.agda new file mode 100644 index 0000000..b988651 --- /dev/null +++ b/Category/Diagram/Cospan.agda @@ -0,0 +1,117 @@ +{-# OPTIONS --without-K --safe #-} + +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Level using (Level; _⊔_) + +module Category.Diagram.Cospan {o ℓ e : Level} (𝒞 : FinitelyCocompleteCategory o ℓ e) where + +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Relation.Binary using (IsEquivalence) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 + +open 𝒞 hiding (i₁; i₂; _≈_) +open ⇒-Reasoning U using (switch-fromtoˡ; glueTrianglesˡ) +open Morphism U using (_≅_; module ≅) + +record Cospan (A B : Obj) : Set (o ⊔ ℓ) where + + constructor cospan + + field + {N} : Obj + f₁ : A ⇒ N + f₂ : B ⇒ N + +private + variable + A B C D : Obj + +record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where + + module C = Cospan C + module D = Cospan D + + field + ≅N : C.N ≅ D.N + + open _≅_ ≅N public + module ≅N = _≅_ ≅N + + field + from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁ + from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂ + +infix 4 _≈_ + +private + variable + f g h : Cospan A B + +≈-refl : f ≈ f +≈-refl {f = cospan f₁ f₂} = record + { ≅N = ≅.refl + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ + } + where abstract + from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁ + from∘f₁≈f₁ = identityˡ + from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂ + from∘f₂≈f₂ = identityˡ + +≈-sym : f ≈ g → g ≈ f +≈-sym f≈g = record + { ≅N = ≅.sym ≅N + ; from∘f₁≈f₁ = a + ; from∘f₂≈f₂ = b + } + where abstract + open _≈_ f≈g + a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁ + a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁) + b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂ + b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂) + +≈-trans : f ≈ g → g ≈ h → f ≈ h +≈-trans f≈g g≈h = record + { ≅N = ≅.trans f≈g.≅N g≈h.≅N + ; from∘f₁≈f₁ = a + ; from∘f₂≈f₂ = b + } + where abstract + module f≈g = _≈_ f≈g + module g≈h = _≈_ g≈h + a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁ + a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁ + b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂ + b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂ + +≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B}) +≈-equiv = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + +compose : Cospan A B → Cospan B C → Cospan A C +compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i) + where + open pushout g h + +identity : Cospan A A +identity = cospan id id + +compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D +compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂) + where + module P₁ = pushout f₂ g₁ + module P₂ = pushout g₂ h₁ + module P₃ = pushout P₁.i₂ P₂.i₁ + +_⊗_ : Cospan A B → Cospan C D → Cospan (A + C) (B + D) +_⊗_ (cospan f₁ f₂) (cospan g₁ g₂) = cospan (f₁ +₁ g₁) (f₂ +₁ g₂) + +infixr 10 _⊗_ diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda index ae6d359..d17a58d 100644 --- a/Category/Instance/Cospans.agda +++ b/Category/Instance/Cospans.agda @@ -13,12 +13,10 @@ open Category U hiding (_≈_) open import Categories.Diagram.Pushout U using (Pushout) open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso) -open import Relation.Binary using (IsEquivalence) open import Categories.Morphism U using (_≅_; module ≅) open import Categories.Morphism.Reasoning U using ( switch-fromtoˡ - ; glueTrianglesˡ ; pullˡ ; pullʳ ; cancelˡ ) @@ -30,99 +28,16 @@ open import Category.Diagram.Pushout U  ; extend-i₁-iso ; extend-i₂-iso ) -record Cospan (A B : Obj) : Set (o ⊔ ℓ) where - - constructor cospan - - field - {N} : Obj - f₁ : A ⇒ N - f₂ : B ⇒ N +open import Category.Diagram.Cospan 𝒞 using (Cospan; compose; compose-3; identity; _≈_; cospan; ≈-trans; ≈-sym; ≈-equiv) private variable A B C D : Obj -compose : Cospan A B → Cospan B C → Cospan A C -compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i) - where - open pushout g h - -identity : Cospan A A -identity = cospan id id - -compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D -compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂) - where - module P₁ = pushout f₂ g₁ - module P₂ = pushout g₂ h₁ - module P₃ = pushout P₁.i₂ P₂.i₁ - -record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where - - module C = Cospan C - module D = Cospan D - - field - ≅N : C.N ≅ D.N - - open _≅_ ≅N public - module ≅N = _≅_ ≅N - - field - from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁ - from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂ - private variable f g h : Cospan A B -≈-refl : f ≈ f -≈-refl {f = cospan f₁ f₂} = record - { ≅N = ≅.refl - ; from∘f₁≈f₁ = from∘f₁≈f₁ - ; from∘f₂≈f₂ = from∘f₂≈f₂ - } - where abstract - from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁ - from∘f₁≈f₁ = identityˡ - from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂ - from∘f₂≈f₂ = identityˡ - -≈-sym : f ≈ g → g ≈ f -≈-sym f≈g = record - { ≅N = ≅.sym ≅N - ; from∘f₁≈f₁ = a - ; from∘f₂≈f₂ = b - } - where abstract - open _≈_ f≈g - a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁ - a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁) - b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂ - b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂) - -≈-trans : f ≈ g → g ≈ h → f ≈ h -≈-trans f≈g g≈h = record - { ≅N = ≅.trans f≈g.≅N g≈h.≅N - ; from∘f₁≈f₁ = a - ; from∘f₂≈f₂ = b - } - where abstract - module f≈g = _≈_ f≈g - module g≈h = _≈_ g≈h - a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁ - a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁ - b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂ - b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂ - -≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B}) -≈-equiv = record - { refl = ≈-refl - ; sym = ≈-sym - ; trans = ≈-trans - } - compose-idˡ : compose f identity ≈ f compose-idˡ {f = cospan {N} f₁ f₂} = record { ≅N = ≅P diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda index 7e63f81..b527265 100644 --- a/Category/Instance/DecoratedCospans.agda +++ b/Category/Instance/DecoratedCospans.agda @@ -20,6 +20,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟 import Categories.Category.Monoidal.Utilities as ⊗-Util import Category.Instance.Cospans 𝒞 as Cospans +import Category.Diagram.Cospan 𝒞 as Cospan open import Categories.Category using (Category; _[_∘_]) open import Categories.Category.Cocartesian using (module CocartesianMonoidal) @@ -52,7 +53,7 @@ private compose : DecoratedCospan A B → DecoratedCospan B C → DecoratedCospan A C compose c₁ c₂ = record - { cospan = Cospans.compose C₁.cospan C₂.cospan + { cospan = Cospan.compose C₁.cospan C₂.cospan ; decoration = F₁ [ i₁ , i₂ ] ∘ φ ∘ s⊗t } where @@ -69,7 +70,7 @@ compose c₁ c₂ = record identity : DecoratedCospan A A identity = record - { cospan = Cospans.identity + { cospan = Cospan.identity ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ] } @@ -80,9 +81,9 @@ record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where module C₂ = DecoratedCospan C₂ field - cospans-≈ : C₁.cospan Cospans.≈ C₂.cospan + cospans-≈ : C₁.cospan Cospan.≈ C₂.cospan - open Cospans._≈_ cospans-≈ public + open Cospan._≈_ cospans-≈ public open Morphism 𝒟.U using (_≅_) field @@ -107,13 +108,13 @@ module _ where ≈-refl : f ≈ f ≈-refl = record - { cospans-≈ = Cospans.≈-refl + { cospans-≈ = Cospan.≈-refl ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ } ≈-sym : f ≈ g → g ≈ f ≈-sym f≈g = record - { cospans-≈ = Cospans.≈-sym cospans-≈ + { cospans-≈ = Cospan.≈-sym cospans-≈ ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) } where @@ -121,7 +122,7 @@ module _ where ≈-trans : f ≈ g → g ≈ h → f ≈ h ≈-trans f≈g g≈h = record - { cospans-≈ = Cospans.≈-trans f≈g.cospans-≈ g≈h.cospans-≈ + { cospans-≈ = Cospan.≈-trans f≈g.cospans-≈ g≈h.cospans-≈ ; same-deco = homomorphism ⟩∘⟨refl ○ glueTrianglesˡ 𝒟.U g≈h.same-deco f≈g.same-deco @@ -613,7 +614,7 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re module C₂ = DecoratedCospan c₂ module C₂′ = DecoratedCospan c₂′ ≅C₂∘C₁ = Cospans.compose-equiv ≅C₂.cospans-≈ ≅C₁.cospans-≈ - module ≅C₂∘C₁ = Cospans._≈_ ≅C₂∘C₁ + module ≅C₂∘C₁ = Cospan._≈_ ≅C₂∘C₁ P = 𝒞.pushout C₁.f₂ C₂.f₁ P′ = 𝒞.pushout C₁′.f₂ C₂′.f₁ module P = Pushout P diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda index 2766df2..9bee58e 100644 --- a/Category/Instance/FinitelyCocompletes.agda +++ b/Category/Instance/FinitelyCocompletes.agda @@ -1,29 +1,31 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level) + +open import Level using (Level; suc; _⊔_) + module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where +import Category.Instance.One.Properties as OneProps + open import Categories.Category using (_[_,_]) open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Helper using (categoryHelper) -open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) open import Categories.Category.Core using (Category) +open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Instance.Cats using (Cats) open import Categories.Category.Instance.One using (One; One-⊤) +open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat) open import Categories.Diagram.Coequalizer using (IsCoequalizer) open import Categories.Functor using (Functor) renaming (id to idF) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) open import Categories.Object.Coproduct using (IsCoproduct) open import Categories.Object.Initial using (IsInitial) open import Categories.Object.Product.Core using (Product) -open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×) -open import Category.Instance.One.Properties using (One-FinitelyCocomplete) open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′) -open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) open import Function.Base using (id; flip) -open import Level using (Level; suc; _⊔_) +open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) FinitelyCocompletes = categoryHelper record @@ -48,7 +50,7 @@ FinitelyCocompletes = categoryHelper record One-FCC : FinitelyCocompleteCategory o ℓ e One-FCC = record { U = One - ; finCo = One-FinitelyCocomplete + ; finCo = OneProps.finitelyCocomplete } _×_ @@ -62,7 +64,6 @@ _×_ 𝒞 𝒟 = record where module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = FinitelyCocompleteCategory 𝒟 -{-# INJECTIVE_FOR_INFERENCE _×_ #-} module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where diff --git a/Cospan/Decorated.agda b/Cospan/Decorated.agda index 498a869..b5d6f07 100644 --- a/Cospan/Decorated.agda +++ b/Cospan/Decorated.agda @@ -17,7 +17,7 @@ module Cospan.Decorated module C = FinitelyCocompleteCategory C module D = SymmetricMonoidalCategory D -open import Category.Instance.Cospans C using (Cospan) +open import Category.Diagram.Cospan C using (Cospan) open import Level using (_⊔_) diff --git a/Functor/Instance/Cospan/Embed.agda b/Functor/Instance/Cospan/Embed.agda index 77f0361..6dbc04a 100644 --- a/Functor/Instance/Cospan/Embed.agda +++ b/Functor/Instance/Cospan/Embed.agda @@ -1,4 +1,5 @@ {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) @@ -14,9 +15,10 @@ open import Categories.Category using (_[_,_]; _[_∘_]; _[_≈_]) open import Categories.Category.Core using (Category) open import Categories.Functor.Core using (Functor) open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan 𝒞 using (cospan) open import Data.Product.Base using (_,_) open import Function.Base using (id) -open import Functor.Instance.Cospan.Stack using (⊗) +open import Functor.Instance.Cospan.Stack 𝒞 using (⊗) module 𝒞 = FinitelyCocompleteCategory 𝒞 module Cospans = Category Cospans @@ -28,24 +30,26 @@ open Morphism U using (module ≅; _≅_) open PushoutProperties U using (up-to-iso) open Pushout′ U using (pushout-id-g; pushout-f-id) -L₁ : {A B : 𝒞.Obj} → U [ A , B ] → Cospans [ A , B ] -L₁ f = record - { f₁ = f - ; f₂ = 𝒞.id - } +private + variable + A B C : 𝒞.Obj + W X Y Z : 𝒞.Obj + +L₁ : U [ A , B ] → Cospans [ A , B ] +L₁ f = cospan f 𝒞.id -L-identity : {A : 𝒞.Obj} → L₁ 𝒞.id ≈ Cospans.id {A} +L-identity : L₁ 𝒞.id ≈ Cospans.id {A} L-identity = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identity² } -L-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] +L-homomorphism : {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] L-homomorphism {X} {Y} {Z} {f} {g} = record { ≅N = up-to-iso P′ P - ; from∘f₁≈f₁′ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) - ; from∘f₂≈f₂′ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₁≈f₁ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) + ; from∘f₂≈f₂ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ } where open ⇒-Reasoning U @@ -57,11 +61,11 @@ L-homomorphism {X} {Y} {Z} {f} {g} = record module P = Pushout P module P′ = Pushout P′ -L-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] +L-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] L-resp-≈ {A} {B} {f} {g} f≈g = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ ○ f≈g - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identityˡ ○ f≈g + ; from∘f₂≈f₂ = 𝒞.identity² } where open 𝒞.HomReasoning @@ -75,24 +79,21 @@ L = record ; F-resp-≈ = L-resp-≈ } -R₁ : {A B : 𝒞.Obj} → U [ B , A ] → Cospans [ A , B ] -R₁ g = record - { f₁ = 𝒞.id - ; f₂ = g - } +R₁ : U [ B , A ] → Cospans [ A , B ] +R₁ g = cospan 𝒞.id g -R-identity : {A : 𝒞.Obj} → R₁ 𝒞.id ≈ Cospans.id {A} +R-identity : R₁ 𝒞.id ≈ Cospans.id {A} R-identity = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identity² } -R-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] -R-homomorphism {X} {Y} {Z} {f} {g} = record +R-homomorphism : {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] +R-homomorphism {f} {g} = record { ≅N = up-to-iso P′ P - ; from∘f₁≈f₁′ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ - ; from∘f₂≈f₂′ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) + ; from∘f₁≈f₁ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₂≈f₂ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) } where open ⇒-Reasoning U @@ -104,11 +105,11 @@ R-homomorphism {X} {Y} {Z} {f} {g} = record module P = Pushout P module P′ = Pushout P′ -R-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] -R-resp-≈ {A} {B} {f} {g} f≈g = record +R-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] +R-resp-≈ {f} {g} f≈g = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ f≈g + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identityˡ ○ f≈g } where open 𝒞.HomReasoning @@ -122,17 +123,11 @@ R = record ; F-resp-≈ = R-resp-≈ } -B₁ : {A B C : 𝒞.Obj} → U [ A , C ] → U [ B , C ] → Cospans [ A , B ] -B₁ f g = record - { f₁ = f - ; f₂ = g - } - -B∘L : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ B₁ g h ∘ L₁ f ] ≈ B₁ (U [ g ∘ f ]) h -B∘L {W} {X} {Y} {Z} {f} {g} {h} = record +B∘L : {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ cospan g h ∘ L₁ f ] ≈ cospan (U [ g ∘ f ]) h +B∘L {f} {g} {h} = record { ≅N = up-to-iso P P′ - ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) - ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) + ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ } where open ⇒-Reasoning U @@ -144,11 +139,11 @@ B∘L {W} {X} {Y} {Z} {f} {g} {h} = record module P = Pushout P module P′ = Pushout P′ -R∘B : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ B₁ f g ] ≈ B₁ f (U [ g ∘ h ]) -R∘B {W} {X} {Y} {Z} {f} {g} {h} = record +R∘B : {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ cospan f g ] ≈ cospan f (U [ g ∘ h ]) +R∘B {f} {g} {h} = record { ≅N = up-to-iso P P′ - ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ - ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) + ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) } where open ⇒-Reasoning U @@ -164,20 +159,18 @@ module _ where open _≅_ - ≅-L-R : ∀ {X Y : 𝒞.Obj} (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) - ≅-L-R {X} {Y} X≅Y = record + ≅-L-R : (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) + ≅-L-R X≅Y = record { ≅N = X≅Y - ; from∘f₁≈f₁′ = isoʳ X≅Y - ; from∘f₂≈f₂′ = 𝒞.identityʳ + ; from∘f₁≈f₁ = isoʳ X≅Y + ; from∘f₂≈f₂ = 𝒞.identityʳ } -module ⊗ = Functor (⊗ 𝒞) - -L-resp-⊗ : {X Y X′ Y′ : 𝒞.Obj} {a : U [ X , X′ ]} {b : U [ Y , Y′ ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) -L-resp-⊗ {X} {Y} {X′} {Y′} {a} {b} = record +L-resp-⊗ : {a : U [ W , X ]} {b : U [ Y , Z ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) +L-resp-⊗ {a} {b} = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ - ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) + ; from∘f₁≈f₁ = 𝒞.identityˡ + ; from∘f₂≈f₂ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) } where open 𝒞.HomReasoning diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda index 03cca1f..b72219b 100644 --- a/Functor/Instance/Cospan/Stack.agda +++ b/Functor/Instance/Cospan/Stack.agda @@ -9,9 +9,11 @@ import Categories.Diagram.Pushout.Properties as PushoutProperties import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as ⇒-Reasoning -open import Categories.Category.Core using (Category) +open import Categories.Category using (Category) +open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor) -open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same; id-Cospan; compose) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan 𝒞 as Cospan using (Cospan; identity; compose; _⊗_) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using () renaming (_×_ to _×′_) open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) @@ -32,27 +34,19 @@ open DiagramPushout U×U using () renaming (Pushout to Pushout′) open import Categories.Category.Monoidal.Utilities monoidal using (_⊗ᵢ_) -together : {A A′ B B′ : Obj} → Cospan A B → Cospan A′ B′ → Cospan (A + A′) (B + B′) -together A⇒B A⇒B′ = record - { f₁ = f₁ A⇒B +₁ f₁ A⇒B′ - ; f₂ = f₂ A⇒B +₁ f₂ A⇒B′ - } - where - open Cospan - -id⊗id≈id : {A B : Obj} → Same (together (id-Cospan {A}) (id-Cospan {B})) (id-Cospan {A + B}) +id⊗id≈id : {A B : Obj} → identity {A} ⊗ identity {B} Cospan.≈ identity {A + B} id⊗id≈id {A} {B} = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = from∘f≈f′ - ; from∘f₂≈f₂′ = from∘f≈f′ + ; from∘f₁≈f₁ = from∘f≈f + ; from∘f₂≈f₂ = from∘f≈f } where open Morphism U using (module ≅) open HomReasoning open 𝒞 using (+-η; []-cong₂) open coproduct {A} {B} using (i₁; i₂) - from∘f≈f′ : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id - from∘f≈f′ = begin + from∘f≈f : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id + from∘f≈f = begin id ∘ [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ identityˡ ⟩ [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ []-cong₂ identityʳ identityʳ ⟩ [ i₁ , i₂ ] ≈⟨ +-η ⟩ @@ -64,14 +58,14 @@ homomorphism → (B⇒C : Cospan B C) → (A⇒B′ : Cospan A′ B′) → (B⇒C′ : Cospan B′ C′) - → Same (together (compose A⇒B B⇒C) (compose A⇒B′ B⇒C′)) (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′) ) + → compose A⇒B B⇒C ⊗ compose A⇒B′ B⇒C′ Cospan.≈ compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′) homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record { ≅N = ≅N - ; from∘f₁≈f₁′ = from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = from∘f₂≈f₂′ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where - open Cospan + open Cospan.Cospan open Pushout open HomReasoning open ⇒-Reasoning U @@ -89,56 +83,62 @@ homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record P₃′ = IsPushout⇒Pushout (-+-.F-resp-pushout P₁×P₂.isPushout) ≅N : Q P₃′ ≅ Q P₃ ≅N = up-to-iso P₃′ P₃ - from∘f₁≈f₁′ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′)) - from∘f₁≈f₁′ = begin + from∘f₁≈f₁ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′)) + from∘f₁≈f₁ = begin from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈⟨ Equiv.refl ⟩ from ≅N ∘ ((i₁ P₁ ∘ f₁ A⇒B) +₁ (i₁ P₂ ∘ f₁ A⇒B′)) ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨ from ≅N ∘ (i₁ P₁ +₁ i₁ P₂) ∘ (f₁ A⇒B +₁ f₁ A⇒B′) ≈⟨ Equiv.refl ⟩ - from ≅N ∘ i₁ P₃′ ∘ f₁ (together A⇒B A⇒B′) ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩ - i₁ P₃ ∘ f₁ (together A⇒B A⇒B′) ∎ - from∘f₂≈f₂′ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′)) - from∘f₂≈f₂′ = begin + from ≅N ∘ i₁ P₃′ ∘ f₁ (A⇒B ⊗ A⇒B′) ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩ + i₁ P₃ ∘ f₁ (A⇒B ⊗ A⇒B′) ∎ + from∘f₂≈f₂ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′)) + from∘f₂≈f₂ = begin from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈⟨ Equiv.refl ⟩ from ≅N ∘ ((i₂ P₁ ∘ f₂ B⇒C) +₁ (i₂ P₂ ∘ f₂ B⇒C′)) ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨ from ≅N ∘ (i₂ P₁ +₁ i₂ P₂) ∘ (f₂ B⇒C +₁ f₂ B⇒C′) ≈⟨ Equiv.refl ⟩ - from ≅N ∘ i₂ P₃′ ∘ f₂ (together B⇒C B⇒C′) ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩ - i₂ P₃ ∘ f₂ (together B⇒C B⇒C′) ∎ + from ≅N ∘ i₂ P₃′ ∘ f₂ (B⇒C ⊗ B⇒C′) ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩ + i₂ P₃ ∘ f₂ (B⇒C ⊗ B⇒C′) ∎ ⊗-resp-≈ : {A A′ B B′ : Obj} {f f′ : Cospan A B} {g g′ : Cospan A′ B′} - → Same f f′ - → Same g g′ - → Same (together f g) (together f′ g′) + → f Cospan.≈ f′ + → g Cospan.≈ g′ + → f ⊗ g Cospan.≈ f′ ⊗ g′ ⊗-resp-≈ {_} {_} {_} {_} {f} {f′} {g} {g′} ≈f ≈g = record { ≅N = ≈f.≅N ⊗ᵢ ≈g.≅N - ; from∘f₁≈f₁′ = from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = from∘f₂≈f₂′ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open 𝒞 using (-+-) - module ≈f = Same ≈f - module ≈g = Same ≈g + module ≈f = Cospan._≈_ ≈f + module ≈g = Cospan._≈_ ≈g open HomReasoning - open Cospan + open Cospan.Cospan open 𝒞 using (+₁-cong₂; +₁∘+₁) - from∘f₁≈f₁′ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′ - from∘f₁≈f₁′ = begin  + from∘f₁≈f₁ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′ + from∘f₁≈f₁ = begin  (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈⟨ +₁∘+₁ ⟩ - (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g) ≈⟨ +₁-cong₂ (≈f.from∘f₁≈f₁′) (≈g.from∘f₁≈f₁′) ⟩ + (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g) ≈⟨ +₁-cong₂ ≈f.from∘f₁≈f₁ ≈g.from∘f₁≈f₁ ⟩ f₁ f′ +₁ f₁ g′ ∎ - from∘f₂≈f₂′ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′ - from∘f₂≈f₂′ = begin  + from∘f₂≈f₂ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′ + from∘f₂≈f₂ = begin  (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈⟨ +₁∘+₁ ⟩ - (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g) ≈⟨ +₁-cong₂ (≈f.from∘f₂≈f₂′) (≈g.from∘f₂≈f₂′) ⟩ + (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g) ≈⟨ +₁-cong₂ ≈f.from∘f₂≈f₂ ≈g.from∘f₂≈f₂ ⟩ f₂ f′ +₁ f₂ g′ ∎ +private + ⊗′ : Bifunctor Cospans Cospans Cospans + ⊗′ = record + { F₀ = λ (A , A′) → A + A′ + ; F₁ = λ (f , g) → f ⊗ g + ; identity = λ { {x , y} → id⊗id≈id {x} {y} } + ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } + ; F-resp-≈ = λ (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g + } + ⊗ : Bifunctor Cospans Cospans Cospans -⊗ = record - { F₀ = λ { (A , A′) → A + A′ } - ; F₁ = λ { (f , g) → together f g } - ; identity = λ { {x , y} → id⊗id≈id {x} {y} } - ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } - ; F-resp-≈ = λ { (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g } - } +⊗ = ⊗′ + +module ⊗ = Functor ⊗ diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda index 30cec87..fedddba 100644 --- a/Functor/Instance/Decorate.agda +++ b/Functor/Instance/Decorate.agda @@ -1,4 +1,5 @@ {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) open import Categories.Functor.Monoidal.Symmetric using (module Lax) @@ -19,6 +20,7 @@ module Functor.Instance.Decorate import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning import Categories.Diagram.Pushout as DiagramPushout import Categories.Morphism.Reasoning as ⇒-Reasoning +import Category.Diagram.Cospan 𝒞 as Cospan open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) open import Categories.Category.Cocartesian using (module CocartesianMonoidal) @@ -27,10 +29,10 @@ open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Properties using ([_]-resp-≅) open import Function.Base using () renaming (id to idf) -open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same) +open import Category.Instance.Cospans 𝒞 using (Cospans) open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) -open import Functor.Instance.Cospan.Stack using (⊗) -open import Functor.Instance.DecoratedCospan.Stack using () renaming (⊗ to ⊗′) +open import Functor.Instance.Cospan.Stack 𝒞 using (module ⊗) +open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using () renaming (module ⊗ to ⊗′) module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = SymmetricMonoidalCategory 𝒟 @@ -67,14 +69,14 @@ identity = record open ⇒-Reasoning 𝒟.U homomorphism : DecoratedCospans [ decorate (Cospans [ g ∘ f ]) ≈ DecoratedCospans [ decorate g ∘ decorate f ] ] -homomorphism {B} {C} {g} {A} {f} = record +homomorphism {g} {f} = record { cospans-≈ = Cospans.Equiv.refl ; same-deco = same-deco } where - open Cospan f using (N; f₂) - open Cospan g using () renaming (N to M; f₁ to g₁) + open Cospan.Cospan f using (N; f₂) + open Cospan.Cospan g using () renaming (N to M; f₁ to g₁) open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) @@ -99,7 +101,7 @@ homomorphism {B} {C} {g} {A} {f} = record F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩ F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ F.homomorphism ⟩ - F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ push-center (sym F.homomorphism) ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ push-center F.homomorphism ⟩ F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨ F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩ F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , ¡)) ⟨ @@ -126,19 +128,15 @@ Decorate = record ; F-resp-≈ = F-resp-≈ } -module ⊗ = Functor (⊗ 𝒞) -module ⊗′ = Functor (⊗′ 𝒞 F) -open 𝒞 using (_+₁_) - Decorate-resp-⊗ : DecoratedCospans [ decorate (⊗.₁ (f , g)) ≈ ⊗′.₁ (decorate f , decorate g) ] -Decorate-resp-⊗ {f = f} {g = g} = record - { cospans-≈ = Cospans.Equiv.refl +Decorate-resp-⊗ {f} {g} = record + { cospans-≈ = Cospan.≈-refl ; same-deco = same-deco } where - open Cospan f using (N) - open Cospan g using () renaming (N to M) + open Cospan.Cospan f using (N) + open Cospan.Cospan g using () renaming (N to M) open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) @@ -165,4 +163,3 @@ Decorate-resp-⊗ {f = f} {g = g} = record F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ extendʳ (φ-commute (¡ , ¡)) ⟨ φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ∎ - diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda index 4595a8f..77b16fa 100644 --- a/Functor/Instance/DecoratedCospan/Embed.agda +++ b/Functor/Instance/DecoratedCospan/Embed.agda @@ -19,6 +19,7 @@ import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning import Categories.Diagram.Pushout.Properties as PushoutProperties import Categories.Morphism.Reasoning as ⇒-Reasoning import Category.Diagram.Pushout as Pushout′ +import Category.Diagram.Cospan as Cospan import Functor.Instance.Cospan.Embed 𝒞 as Embed open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) @@ -34,9 +35,9 @@ import Categories.Morphism as Morphism open import Categories.Category.Cocartesian using (module CocartesianMonoidal) open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Functor using (Functor; _∘F_) -open import Data.Product.Base using (_,_) -open import Function.Base using () renaming (id to idf) -open import Functor.Instance.DecoratedCospan.Stack using (⊗) +open import Data.Product using (_,_) +open import Function using () renaming (id to idf) +open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗) module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = SymmetricMonoidalCategory 𝒟 @@ -62,7 +63,7 @@ R = Decorate ∘F Embed.R B₁ : 𝒞.U [ A , C ] → 𝒞.U [ B , C ] → 𝒟.U [ 𝒟.unit , F.F₀ C ] → DecoratedCospans [ A , B ] B₁ f g s = record - { cospan = Embed.B₁ f g + { cospan = Cospan.cospan f g ; decoration = s } @@ -265,7 +266,6 @@ module _ where where module Decorate = Functor Decorate - module ⊗ = Functor (⊗ 𝒞 F) open 𝒞 using (_+₁_) L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ] diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda index 5c3c232..381ee06 100644 --- a/Functor/Instance/DecoratedCospan/Stack.agda +++ b/Functor/Instance/DecoratedCospan/Stack.agda @@ -19,6 +19,7 @@ import Categories.Diagram.Pushout as DiagramPushout import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as ⇒-Reasoning import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning + import Functor.Instance.Cospan.Stack 𝒞 as Stack open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) @@ -26,13 +27,16 @@ open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Category.Monoidal.Properties using (coherence-inv₃) open import Categories.Category.Monoidal.Braided.Properties using (braiding-coherence-inv) +open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor) open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) open import Categories.Object.Initial using (Initial) open import Categories.Object.Duality using (Coproduct⇒coProduct) -open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; Same to Same′) -open import Category.Instance.Cospans 𝒞 using (Same; compose) +open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; _≈_ to _≈_′) + +import Category.Diagram.Cospan 𝒞 as Cospan + open import Cospan.Decorated 𝒞 F using (DecoratedCospan) open import Data.Product.Base using (_,_) @@ -52,10 +56,9 @@ private variable A A′ B B′ C C′ : Obj - together : Cospans [ A , B ] → Cospans [ A′ , B′ ] → Cospans [ A + A′ , B + B′ ] together A⇒B A⇒B′ = record - { cospan = Stack.together A⇒B.cospan A⇒B′.cospan + { cospan = A⇒B.cospan Cospan.⊗ A⇒B′.cospan ; decoration = ⊗-homo.η (A⇒B.N , A⇒B′.N) ∘ A⇒B.decoration ⊗₁ A⇒B′.decoration ∘ unitorʳ.to } where @@ -108,9 +111,9 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record module _ where open DecoratedCospan using (cospan) - cospans-≈ : Same (Stack.together _ _) (compose (Stack.together _ _) (Stack.together _ _)) + cospans-≈ : _ Cospan.⊗ _ Cospan.≈ Cospan.compose (_ Cospan.⊗ _) (_ Cospan.⊗ _) cospans-≈ = Stack.homomorphism (f .cospan) (g .cospan) (f′ .cospan) (g′ .cospan) - open Same cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public + open Cospan._≈_ cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public module DecorationNames where open DecoratedCospan f using (N) renaming (decoration to s) public @@ -185,7 +188,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record ≅∘[]+[]≈μ∘μ+μ = begin ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′ ≈⟨ refl⟩∘⟨ μ∘+ ⟩⊗⟨ μ∘+ ⟩ ≅ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ introˡ +-η ⟩ - ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ push-center (sym μ∘+) ⟩ + ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ push-center μ∘+ ⟩ ≅ ∘ μ ∘ (ι₁ +₁ ι₂) ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ⊗-distrib-over-∘ ⟩ ≅ ∘ μ ∘ (ι₁ ∘ μ ∘ i₁ +₁ i₂) +₁ (ι₂ ∘ μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ μ-natural) ⟩⊗⟨ (extendʳ μ-natural) ⟩ ≅ ∘ μ ∘ (μ ∘ ι₁ +₁ ι₁ ∘ i₁ +₁ i₂) +₁ (μ ∘ ι₂ +₁ ι₂ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩⊗⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩ @@ -221,7 +224,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record α⇐ ∘ w +₁ (x +₁ _ ∘ α⇒ ∘ _) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ assoc-commute-from ⟩∘⟨refl ⟨ α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y) +₁ z ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pushˡ split₁ʳ) ⟩∘⟨refl ⟨ α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y ∘ +-swap) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ σ.⇒.sym-commute _ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩ - α⇐ ∘ w +₁ (α⇒ ∘ (+-swap ∘ y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center (sym split₁ˡ) ⟩∘⟨refl ⟩ + α⇐ ∘ w +₁ (α⇒ ∘ (+-swap ∘ y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center split₁ˡ ⟩∘⟨refl ⟩ α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ (y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ assoc-commute-to) ⟩∘⟨refl ⟨ α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐ ∘ y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc²εβ ⟩∘⟨refl ⟩ α⇐ ∘ w +₁ ((α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ @@ -231,7 +234,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record μ∘μ+μ∘swap-inner : {X : Obj} → μ {X} ∘ μ +₁ μ ∘ swap-inner ≈ μ ∘ μ +₁ μ {X} μ∘μ+μ∘swap-inner = begin - μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ push-center (sym serialize₁₂) ⟩ + μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ push-center serialize₁₂ ⟩ μ ∘ μ +₁ id ∘ id +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ μ ∘ μ +₁ id ∘ (id +₁ id) +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-to ⟨ μ ∘ μ +₁ id ∘ α⇐ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ pullˡ μ-assoc ⟩ @@ -243,7 +246,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record μ ∘ id +₁ (μ ∘ μ +₁ id ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pull-center (sym split₁ˡ) ⟩∘⟨refl ⟩ μ ∘ id +₁ (μ ∘ (μ ∘ +-swap) +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ μ∘σ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩ μ ∘ id +₁ (μ ∘ μ +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (sym-assoc ○ flip-iso associator (μ-assoc ○ sym-assoc)) ⟩∘⟨refl ⟩ - μ ∘ id +₁ (μ ∘ id +₁ μ) ∘ α⇒ ≈⟨ push-center (sym split₂ʳ) ⟩ + μ ∘ id +₁ (μ ∘ id +₁ μ) ∘ α⇒ ≈⟨ push-center split₂ʳ ⟩ μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟨ μ ∘ id +₁ μ ∘ α⇒ ∘ (id +₁ id) +₁ μ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩ μ ∘ id +₁ μ ∘ α⇒ ∘ id +₁ μ ≈⟨ refl⟩∘⟨ sym-assoc ⟩ @@ -370,13 +373,13 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record } where - open Same′ using (cospans-≈) + open _≈_′ using (cospans-≈) module SameNames where - open Same′ ≈f using () renaming (same-deco to ≅∘s≈t) public - open Same′ ≈g using () renaming (same-deco to ≅∘s≈t′) public - open Same (≈f .cospans-≈) using (module ≅N) public - open Same (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public + open _≈_′ ≈f using () renaming (same-deco to ≅∘s≈t) public + open _≈_′ ≈g using () renaming (same-deco to ≅∘s≈t′) public + open Cospan._≈_ (≈f .cospans-≈) using (module ≅N) public + open Cospan._≈_ (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public open SameNames @@ -417,9 +420,11 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record ⊗ : Bifunctor Cospans Cospans Cospans ⊗ = record - { F₀ = λ { (A , A′) → A + A′ } - ; F₁ = λ { (f , g) → together f g } + { F₀ = λ (A , A′) → A + A′ + ; F₁ = λ (f , g) → together f g ; identity = λ { {x , y} → id⊗id≈id {x} {y} } ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } - ; F-resp-≈ = λ { (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g } + ; F-resp-≈ = λ (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g } + +module ⊗ = Functor ⊗ -- cgit v1.2.3