diff options
Diffstat (limited to 'Category')
21 files changed, 1877 insertions, 509 deletions
diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda index dedfa16..5425233 100644 --- a/Category/Instance/Properties/FinitelyCocompletes.agda +++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda @@ -1,23 +1,27 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level) -module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where +open import Level using (Level; suc; _⊔_) +module Category.Cartesian.Instance.FinitelyCocompletes {o ℓ e : Level} where + +import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as ⇒-Reasoning open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_) open import Categories.Diagram.Coequalizer using (IsCoequalizer) +open import Categories.Functor.Bifunctor using (flip-bifunctor) open import Categories.Functor.Core using (Functor) -open import Categories.Functor using (_∘F_) renaming (id to idF) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso) open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) open import Categories.Object.Initial using (IsInitial) +open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) + open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) -open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) open import Functor.Exact using (IsRightExact; RightExactFunctor) -open import Level using (_⊔_; suc) +open import Functor.Exact.Instance.Swap using (Swap) FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) FinitelyCocompletes-CC = record @@ -202,9 +206,37 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where ; F-resp-coeq = +-resp-coeq 𝒞 } } + module x+y = RightExactFunctor -+- + + ↔-+- : 𝒞 × 𝒞 ⇒ 𝒞 + ↔-+- = -+- ∘ Swap 𝒞 𝒞 + module y+x = RightExactFunctor ↔-+- [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 [x+y]+z = -+- ∘ (-+- ×₁ id) + module [x+y]+z = RightExactFunctor [x+y]+z x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ + module x+[y+z] = RightExactFunctor x+[y+z] + + assoc-≃ : [x+y]+z.F ≃ x+[y+z].F + assoc-≃ = pointwise-iso (λ { ((X , Y) , Z) → ≅.sym (𝒞.+-assoc {X} {Y} {Z})}) commute + where + open 𝒞 + module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞) + open Morphism U using (_≅_; module ≅) + module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z})) + open import Categories.Category.BinaryProducts using (BinaryProducts) + open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct) + op-binaryProducts : BinaryProducts op + op-binaryProducts = record { product = Coproduct⇒coProduct coproduct } + open BinaryProducts op-binaryProducts using () renaming (assocʳ∘⁂ to +₁∘assocˡ) + open Equiv + commute + : {((X , Y) , Z) : 𝒞×𝒞×𝒞.Obj} + {((X′ , Y′) , Z′) : 𝒞×𝒞×𝒞.Obj} + → (F : ((X , Y) , Z) 𝒞×𝒞×𝒞.⇒ ((X′ , Y′) , Z′)) + → (+-assoc.from 𝒞.∘ [x+y]+z.₁ F) + ≈ (x+[y+z].₁ F 𝒞.∘ +-assoc.from) + commute {(X , Y) , Z} {(X′ , Y′) , Z′} ((F , G) , H) = sym +₁∘assocˡ diff --git a/Category/Cartesian/Instance/SymMonCat.agda b/Category/Cartesian/Instance/SymMonCat.agda new file mode 100644 index 0000000..7d91d52 --- /dev/null +++ b/Category/Cartesian/Instance/SymMonCat.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; suc; _⊔_) + +module Category.Cartesian.Instance.SymMonCat {o ℓ e : Level} where + +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) + +SymMonCat-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +SymMonCat-CC = record + { U = SymMonCat + ; cartesian = SymMonCat-Cartesian + } + diff --git a/Category/Cocomplete/Finitely/Bundle.agda b/Category/Cocomplete/Finitely/Bundle.agda index 74f434f..8af8633 100644 --- a/Category/Cocomplete/Finitely/Bundle.agda +++ b/Category/Cocomplete/Finitely/Bundle.agda @@ -28,6 +28,7 @@ record FinitelyCocompleteCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where ; monoidal = monoidal ; symmetric = symmetric } + {-# INJECTIVE_FOR_INFERENCE symmetricMonoidalCategory #-} cocartesianCategory : CocartesianCategory o ℓ e cocartesianCategory = record diff --git a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda index 26813eb..2b66d19 100644 --- a/Category/Cocomplete/Finitely/SymmetricMonoidal.agda +++ b/Category/Cocomplete/Finitely/SymmetricMonoidal.agda @@ -4,11 +4,11 @@ open import Categories.Category.Core using (Category) module Category.Cocomplete.Finitely.SymmetricMonoidal {o ℓ e} {𝒞 : Category o ℓ e} where -open import Categories.Category.Cocomplete.Finitely using (FinitelyCocomplete) +open import Categories.Category.Cocomplete.Finitely 𝒞 using (FinitelyCocomplete) open import Categories.Category.Cocartesian 𝒞 using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) -module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete 𝒞) where +module FinitelyCocompleteSymmetricMonoidal (finCo : FinitelyCocomplete) where open FinitelyCocomplete finCo using (cocartesian) open CocartesianMonoidal cocartesian using (+-monoidal) public diff --git a/Category/Construction/CMonoids.agda b/Category/Construction/CMonoids.agda new file mode 100644 index 0000000..c2793cf --- /dev/null +++ b/Category/Construction/CMonoids.agda @@ -0,0 +1,57 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Level using (Level; _⊔_) + +-- The category of commutative monoids internal to a symmetric monoidal category + +module Category.Construction.CMonoids + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + {M : Monoidal 𝒞} + (symmetric : Symmetric M) + where + +open import Categories.Functor using (Functor) +open import Categories.Morphism.Reasoning 𝒞 +open import Object.Monoid.Commutative symmetric + +open Category 𝒞 +open Monoidal M +open HomReasoning +open CommutativeMonoid⇒ + +CMonoids : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e +CMonoids = record + { Obj = CommutativeMonoid + ; _⇒_ = CommutativeMonoid⇒ + ; _≈_ = λ f g → arr f ≈ arr g + ; id = record + { monoid⇒ = record + { arr = id + ; preserves-μ = identityˡ ○ introʳ ⊗.identity + ; preserves-η = identityˡ + } + } + ; _∘_ = λ f g → record + { monoid⇒ = record + { arr = arr f ∘ arr g + ; preserves-μ = glue (preserves-μ f) (preserves-μ g) ○ ∘-resp-≈ʳ (⟺ ⊗.homomorphism) + ; preserves-η = glueTrianglesˡ (preserves-η f) (preserves-η g) + } + } + ; assoc = assoc + ; sym-assoc = sym-assoc + ; identityˡ = identityˡ + ; identityʳ = identityʳ + ; identity² = identity² + ; equiv = record + { refl = refl + ; sym = sym + ; trans = trans + } + ; ∘-resp-≈ = ∘-resp-≈ + } + where open Equiv diff --git a/Category/Construction/CMonoids/Properties.agda b/Category/Construction/CMonoids/Properties.agda new file mode 100644 index 0000000..fab8b0b --- /dev/null +++ b/Category/Construction/CMonoids/Properties.agda @@ -0,0 +1,74 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Level using (Level; _⊔_) + +module Category.Construction.CMonoids.Properties + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + {monoidal : Monoidal 𝒞} + (symmetric : Symmetric monoidal) + where + +import Categories.Category.Monoidal.Reasoning monoidal as ⊗-Reasoning +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning +import Category.Construction.Monoids.Properties {o} {ℓ} {e} {𝒞} monoidal as Monoids + +open import Categories.Category using (_[_,_]) +open import Categories.Category.Monoidal.Symmetric.Properties symmetric using (module Shorthands) +open import Categories.Morphism using (_≅_) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Categories.Object.Monoid monoidal using (Monoid) +open import Category.Construction.CMonoids symmetric using (CMonoids) +open import Data.Product using (Σ-syntax; _,_) +open import Object.Monoid.Commutative symmetric using (CommutativeMonoid) + +module 𝒞 = Category 𝒞 + +open CommutativeMonoid using (monoid) renaming (Carrier to ∣_∣) + +transport-by-iso + : {X : 𝒞.Obj} + → (M : CommutativeMonoid) + → 𝒞 [ ∣ M ∣ ≅ X ] + → Σ[ Xₘ ∈ CommutativeMonoid ] CMonoids [ M ≅ Xₘ ] +transport-by-iso {X} M ∣M∣≅X + using (Xₘ′ , M≅Xₘ′) ← Monoids.transport-by-iso {X} (monoid M) ∣M∣≅X = Xₘ , M≅Xₘ + where + module M≅Xₘ′ = _≅_ M≅Xₘ′ + open _≅_ ∣M∣≅X + module Xₘ′ = Monoid Xₘ′ + open CommutativeMonoid M + open 𝒞 using (_≈_; _∘_) + open Shorthands + open ⊗-Reasoning + open ⇒-Reasoning + open Symmetric symmetric using (_⊗₁_; module braiding) + comm : from ∘ μ ∘ to ⊗₁ to ≈ (from ∘ μ ∘ to ⊗₁ to) ∘ σ⇒ + comm = begin + from ∘ μ ∘ to ⊗₁ to ≈⟨ push-center (commutative) ⟩ + from ∘ μ ∘ σ⇒ ∘ to ⊗₁ to ≈⟨ pushʳ (pushʳ (braiding.⇒.commute (to , to))) ⟩ + (from ∘ μ ∘ to ⊗₁ to) ∘ σ⇒ ∎ + Xₘ : CommutativeMonoid + Xₘ = record + { Carrier = X + ; isCommutativeMonoid = record + { isMonoid = Xₘ′.isMonoid + ; commutative = comm + } + } + M⇒Xₘ : CMonoids [ M , Xₘ ] + M⇒Xₘ = record { monoid⇒ = M≅Xₘ′.from } + Xₘ⇒M : CMonoids [ Xₘ , M ] + Xₘ⇒M = record { monoid⇒ = M≅Xₘ′.to } + M≅Xₘ : CMonoids [ M ≅ Xₘ ] + M≅Xₘ = record + { from = M⇒Xₘ + ; to = Xₘ⇒M + ; iso = record + { isoˡ = isoˡ + ; isoʳ = isoʳ + } + } diff --git a/Category/Construction/Monoids/Properties.agda b/Category/Construction/Monoids/Properties.agda new file mode 100644 index 0000000..df48063 --- /dev/null +++ b/Category/Construction/Monoids/Properties.agda @@ -0,0 +1,108 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal.Core using (Monoidal) +open import Level using (Level; _⊔_) + +module Category.Construction.Monoids.Properties + {o ℓ e : Level} + {𝒞 : Category o ℓ e} + (monoidal : Monoidal 𝒞) + where + +import Categories.Category.Monoidal.Reasoning monoidal as ⊗-Reasoning +import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning + +open import Categories.Category using (_[_,_]) +open import Categories.Category.Construction.Monoids monoidal using (Monoids) +open import Categories.Category.Monoidal.Utilities monoidal using (module Shorthands; _⊗ᵢ_) +open import Categories.Morphism using (_≅_) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Categories.Object.Monoid monoidal using (Monoid) +open import Data.Product using (Σ-syntax; _,_) + +module 𝒞 = Category 𝒞 + +open Monoid using () renaming (Carrier to ∣_∣) + +transport-by-iso + : {X : 𝒞.Obj} + → (M : Monoid) + → 𝒞 [ ∣ M ∣ ≅ X ] + → Σ[ Xₘ ∈ Monoid ] Monoids [ M ≅ Xₘ ] +transport-by-iso {X} M ∣M∣≅X = Xₘ , M≅Xₘ + where + open _≅_ ∣M∣≅X + open Monoid M + open 𝒞 using (_∘_; id; _≈_; module Equiv) + open Monoidal monoidal + using (_⊗₀_; _⊗₁_; assoc-commute-from; unitorˡ-commute-from; unitorʳ-commute-from) + open Shorthands + open ⊗-Reasoning + open ⇒-Reasoning + as + : (from ∘ μ ∘ to ⊗₁ to) + ∘ (from ∘ μ ∘ to ⊗₁ to) ⊗₁ id + ≈ (from ∘ μ ∘ to ⊗₁ to) + ∘ id ⊗₁ (from ∘ μ ∘ to ⊗₁ to) + ∘ α⇒ + as = extendˡ (begin + (μ ∘ to ⊗₁ to) ∘ (from ∘ μ ∘ to ⊗₁ to) ⊗₁ id ≈⟨ pullʳ merge₁ʳ ⟩ + μ ∘ (to ∘ from ∘ μ ∘ to ⊗₁ to) ⊗₁ to ≈⟨ refl⟩∘⟨ cancelˡ isoˡ ⟩⊗⟨refl ⟩ + μ ∘ (μ ∘ to ⊗₁ to) ⊗₁ to ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ + μ ∘ μ ⊗₁ id ∘ (to ⊗₁ to) ⊗₁ to ≈⟨ extendʳ assoc ⟩ + μ ∘ (id ⊗₁ μ ∘ α⇒) ∘ (to ⊗₁ to) ⊗₁ to ≈⟨ pushʳ (pullʳ assoc-commute-from) ⟩ + (μ ∘ id ⊗₁ μ) ∘ to ⊗₁ (to ⊗₁ to) ∘ α⇒ ≈⟨ extendˡ (pullˡ merge₂ˡ) ⟩ + (μ ∘ to ⊗₁ (μ ∘ to ⊗₁ to)) ∘ α⇒ ≈⟨ (refl⟩∘⟨ refl⟩⊗⟨ insertˡ isoˡ) ⟩∘⟨refl ⟩ + (μ ∘ to ⊗₁ (to ∘ from ∘ μ ∘ to ⊗₁ to)) ∘ α⇒ ≈⟨ pushˡ (pushʳ split₂ʳ) ⟩ + (μ ∘ to ⊗₁ to) ∘ id ⊗₁ (from ∘ μ ∘ to ⊗₁ to) ∘ α⇒ ∎) + idˡ : λ⇒ ≈ (from ∘ μ ∘ to ⊗₁ to) ∘ (from ∘ η) ⊗₁ id + idˡ = begin + λ⇒ ≈⟨ insertˡ isoʳ ⟩ + from ∘ to ∘ λ⇒ ≈⟨ refl⟩∘⟨ unitorˡ-commute-from ⟨ + from ∘ λ⇒ ∘ id ⊗₁ to ≈⟨ refl⟩∘⟨ pushˡ identityˡ ⟩ + from ∘ μ ∘ η ⊗₁ id ∘ id ⊗₁ to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ serialize₁₂ ⟨ + from ∘ μ ∘ η ⊗₁ to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ insertˡ isoˡ ⟩⊗⟨refl ⟩ + from ∘ μ ∘ (to ∘ from ∘ η) ⊗₁ to ≈⟨ pushʳ (pushʳ split₁ʳ) ⟩ + (from ∘ μ ∘ to ⊗₁ to) ∘ (from ∘ η) ⊗₁ id ∎ + idʳ : ρ⇒ ≈ (from ∘ μ ∘ to ⊗₁ to) ∘ id ⊗₁ (from ∘ η) + idʳ = begin + ρ⇒ ≈⟨ insertˡ isoʳ ⟩ + from ∘ to ∘ ρ⇒ ≈⟨ refl⟩∘⟨ unitorʳ-commute-from ⟨ + from ∘ ρ⇒ ∘ to ⊗₁ id ≈⟨ refl⟩∘⟨ pushˡ identityʳ ⟩ + from ∘ μ ∘ id ⊗₁ η ∘ to ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ serialize₂₁ ⟨ + from ∘ μ ∘ to ⊗₁ η ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ insertˡ isoˡ ⟩ + from ∘ μ ∘ to ⊗₁ (to ∘ from ∘ η) ≈⟨ pushʳ (pushʳ split₂ʳ) ⟩ + (from ∘ μ ∘ to ⊗₁ to) ∘ id ⊗₁ (from ∘ η) ∎ + Xₘ : Monoid + Xₘ = record + { Carrier = X + ; isMonoid = record + { μ = from ∘ μ ∘ to ⊗₁ to + ; η = from ∘ η + ; assoc = as + ; identityˡ = idˡ + ; identityʳ = idʳ + } + } + M⇒Xₘ : Monoids [ M , Xₘ ] + M⇒Xₘ = record + { arr = from + ; preserves-μ = pushʳ (insertʳ (_≅_.isoˡ (∣M∣≅X ⊗ᵢ ∣M∣≅X))) + ; preserves-η = Equiv.refl + } + Xₘ⇒M : Monoids [ Xₘ , M ] + Xₘ⇒M = record + { arr = to + ; preserves-μ = cancelˡ isoˡ + ; preserves-η = cancelˡ isoˡ + } + M≅Xₘ : Monoids [ M ≅ Xₘ ] + M≅Xₘ = record + { from = M⇒Xₘ + ; to = Xₘ⇒M + ; iso = record + { isoˡ = isoˡ + ; isoʳ = isoʳ + } + } 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 d54499d..d17a58d 100644 --- a/Category/Instance/Cospans.agda +++ b/Category/Instance/Cospans.agda @@ -7,7 +7,9 @@ open import Level using (_⊔_) module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where -open FinitelyCocompleteCategory 𝒞 +module 𝒞 = FinitelyCocompleteCategory 𝒞 +open 𝒞 using (U; pushout) +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) @@ -15,8 +17,8 @@ open import Categories.Morphism U using (_≅_; module ≅) open import Categories.Morphism.Reasoning U using ( switch-fromtoˡ - ; glueTrianglesˡ ; pullˡ ; pullʳ + ; cancelˡ ) open import Category.Diagram.Pushout U @@ -26,254 +28,213 @@ open import Category.Diagram.Pushout U ; extend-i₁-iso ; extend-i₂-iso ) -private +open import Category.Diagram.Cospan 𝒞 using (Cospan; compose; compose-3; identity; _≈_; cospan; ≈-trans; ≈-sym; ≈-equiv) +private variable - A B C D X Y Z : Obj - f g h : A ⇒ B - -record Cospan (A B : Obj) : Set (o ⊔ ℓ) where - - field - {N} : Obj - f₁ : A ⇒ N - f₂ : B ⇒ N - -compose : Cospan A B → Cospan B C → Cospan A C -compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ } - where - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module p = pushout C₁.f₂ C₂.f₁ - -id-Cospan : Cospan A A -id-Cospan = record { f₁ = id ; f₂ = id } - -compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D -compose-3 c₁ c₂ c₃ = record { f₁ = P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ ; f₂ = P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ } - where - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module C₃ = Cospan c₃ - module P₁ = pushout C₁.f₂ C₂.f₁ - module P₂ = pushout C₂.f₂ C₃.f₁ - module P₃ = pushout P₁.i₂ P₂.i₁ + A B C D : Obj -record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where - - module C = Cospan C - module C′ = Cospan C′ - - field - ≅N : C.N ≅ C′.N - - open _≅_ ≅N public - module ≅N = _≅_ ≅N - - field - from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁ - from∘f₂≈f₂′ : from ∘ C.f₂ ≈ C′.f₂ - -same-refl : {C : Cospan A B} → Same C C -same-refl = record - { ≅N = ≅.refl - ; from∘f₁≈f₁′ = identityˡ - ; from∘f₂≈f₂′ = identityˡ - } - -same-sym : {C C′ : Cospan A B} → Same C C′ → Same C′ C -same-sym C≅C′ = record - { ≅N = ≅.sym ≅N - ; from∘f₁≈f₁′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁′) - ; from∘f₂≈f₂′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂′) - } - where - open Same C≅C′ - -same-trans : {C C′ C″ : Cospan A B} → Same C C′ → Same C′ C″ → Same C C″ -same-trans C≈C′ C′≈C″ = record - { ≅N = ≅.trans C≈C′.≅N C′≈C″.≅N - ; from∘f₁≈f₁′ = glueTrianglesˡ C′≈C″.from∘f₁≈f₁′ C≈C′.from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = glueTrianglesˡ C′≈C″.from∘f₂≈f₂′ C≈C′.from∘f₂≈f₂′ - } - where - module C≈C′ = Same C≈C′ - module C′≈C″ = Same C′≈C″ +private + variable + f g h : Cospan A B -compose-idˡ : {C : Cospan A B} → Same (compose C id-Cospan) C -compose-idˡ {_} {_} {C} = record +compose-idˡ : compose f identity ≈ f +compose-idˡ {f = cospan {N} f₁ f₂} = record { ≅N = ≅P - ; from∘f₁≈f₁′ = begin - ≅P.from ∘ P.i₁ ∘ C.f₁ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₁) ∘ C.f₁ ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩ - id ∘ C.f₁ ≈⟨ identityˡ ⟩ - C.f₁ ∎ - ; from∘f₂≈f₂′ = begin - ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ - ≅P.from ∘ P.i₂ ≈⟨ P.universal∘i₂≈h₂ ⟩ - C.f₂ ∎ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C = Cospan C - P = pushout C.f₂ id + P P′ : Pushout f₂ id + P = pushout f₂ id + P′ = pushout-f-id {f = f₂} module P = Pushout P - P′ = pushout-f-id {f = C.f₂} + ≅P : P.Q ≅ N ≅P = up-to-iso P P′ module ≅P = _≅_ ≅P - -compose-idʳ : {C : Cospan A B} → Same (compose id-Cospan C) C -compose-idʳ {_} {_} {C} = record + abstract + from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ f₁ 𝒞.≈ f₁ + from∘f₁≈f₁ = begin + ≅P.from ∘ P.i₁ ∘ f₁ ≈⟨ cancelˡ P.universal∘i₁≈h₁ ⟩ + f₁ ∎ + from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ id 𝒞.≈ f₂ + from∘f₂≈f₂ = begin + ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + ≅P.from ∘ P.i₂ ≈⟨ P.universal∘i₂≈h₂ ⟩ + f₂ ∎ + +compose-idʳ : compose identity f ≈ f +compose-idʳ {f = cospan {N} f₁ f₂} = record { ≅N = ≅P - ; from∘f₁≈f₁′ = begin - ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ - ≅P.from ∘ P.i₁ ≈⟨ P.universal∘i₁≈h₁ ⟩ - C.f₁ ∎ - ; from∘f₂≈f₂′ = begin - ≅P.from ∘ P.i₂ ∘ C.f₂ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₂) ∘ C.f₂ ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩ - id ∘ C.f₂ ≈⟨ identityˡ ⟩ - C.f₂ ∎ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C = Cospan C - P = pushout id C.f₁ + P P′ : Pushout id f₁ + P = pushout id f₁ module P = Pushout P - P′ = pushout-id-g {g = C.f₁} + P′ = pushout-id-g {g = f₁} + ≅P : P.Q ≅ N ≅P = up-to-iso P P′ module ≅P = _≅_ ≅P - -compose-id² : Same {A} (compose id-Cospan id-Cospan) id-Cospan + abstract + from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ id 𝒞.≈ f₁ + from∘f₁≈f₁ = begin + ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + ≅P.from ∘ P.i₁ ≈⟨ P.universal∘i₁≈h₁ ⟩ + f₁ ∎ + from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ f₂ 𝒞.≈ f₂ + from∘f₂≈f₂ = begin + ≅P.from ∘ P.i₂ ∘ f₂ ≈⟨ cancelˡ P.universal∘i₂≈h₂ ⟩ + f₂ ∎ + +compose-id² : compose identity identity ≈ identity {A} compose-id² = compose-idˡ -compose-3-right - : {c₁ : Cospan A B} - {c₂ : Cospan B C} - {c₃ : Cospan C D} - → Same (compose c₁ (compose c₂ c₃)) (compose-3 c₁ c₂ c₃) -compose-3-right {_} {_} {_} {_} {c₁} {c₂} {c₃} = record - { ≅N = up-to-iso P₄′ P₄ - ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc - ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl +compose-3-right : compose f (compose g h) ≈ compose-3 f g h +compose-3-right {f = f} {g = g} {h = h} = record + { ≅N = ≅N + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module C₃ = Cospan c₃ + module C₁ = Cospan f + module C₂ = Cospan g + module C₃ = Cospan h + P₁ : Pushout C₁.f₂ C₂.f₁ P₁ = pushout C₁.f₂ C₂.f₁ + P₂ : Pushout C₂.f₂ C₃.f₁ P₂ = pushout C₂.f₂ C₃.f₁ module P₁ = Pushout P₁ module P₂ = Pushout P₂ + P₃ : Pushout P₁.i₂ P₂.i₁ P₃ = pushout P₁.i₂ P₂.i₁ module P₃ = Pushout P₃ + P₄ P₄′ : Pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁) P₄ = glue-i₂ P₁ P₃ - module P₄ = Pushout P₄ P₄′ = pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁) + module P₄ = Pushout P₄ module P₄′ = Pushout P₄′ - -compose-3-left - : {c₁ : Cospan A B} - {c₂ : Cospan B C} - {c₃ : Cospan C D} - → Same (compose (compose c₁ c₂) c₃) (compose-3 c₁ c₂ c₃) -compose-3-left {_} {_} {_} {_} {c₁} {c₂} {c₃} = record + ≅N : P₄′.Q ≅ P₄.Q + ≅N = up-to-iso P₄′ P₄ + module ≅N = _≅_ ≅N + abstract + from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ C₁.f₁ 𝒞.≈ P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ + from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc + from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ P₂.i₂ ∘ C₃.f₂ 𝒞.≈ P₄.i₂ ∘ P₂.i₂ ∘ C₃.f₂ + from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl + +compose-3-left : compose (compose f g) h ≈ compose-3 f g h +compose-3-left {f = f} {g = g} {h = h} = record { ≅N = up-to-iso P₄′ P₄ - ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl - ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module C₃ = Cospan c₃ + module C₁ = Cospan f + module C₂ = Cospan g + module C₃ = Cospan h + P₁ : Pushout C₁.f₂ C₂.f₁ P₁ = pushout C₁.f₂ C₂.f₁ + P₂ : Pushout C₂.f₂ C₃.f₁ P₂ = pushout C₂.f₂ C₃.f₁ module P₁ = Pushout P₁ module P₂ = Pushout P₂ + P₃ : Pushout P₁.i₂ P₂.i₁ P₃ = pushout P₁.i₂ P₂.i₁ module P₃ = Pushout P₃ + P₄ P₄′ : Pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁ P₄ = glue-i₁ P₂ P₃ - module P₄ = Pushout P₄ P₄′ = pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁ + module P₄ = Pushout P₄ module P₄′ = Pushout P₄′ + ≅N : P₄′.Q ≅ P₄.Q + ≅N = up-to-iso P₄′ P₄ + module ≅N = _≅_ ≅N + abstract + from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ P₁.i₁ ∘ C₁.f₁ 𝒞.≈ P₄.i₁ ∘ P₁.i₁ ∘ C₁.f₁ + from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl + from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ C₃.f₂ 𝒞.≈ P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ + from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc compose-assoc : {c₁ : Cospan A B} {c₂ : Cospan B C} {c₃ : Cospan C D} - → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃) -compose-assoc = same-trans compose-3-right (same-sym compose-3-left) + → compose c₁ (compose c₂ c₃) ≈ (compose (compose c₁ c₂) c₃) +compose-assoc = ≈-trans compose-3-right (≈-sym compose-3-left) compose-sym-assoc : {c₁ : Cospan A B} {c₂ : Cospan B C} {c₃ : Cospan C D} - → Same (compose (compose c₁ c₂) c₃) (compose c₁ (compose c₂ c₃)) -compose-sym-assoc = same-trans compose-3-left (same-sym compose-3-right) + → compose (compose c₁ c₂) c₃ ≈ compose c₁ (compose c₂ c₃) +compose-sym-assoc = ≈-trans compose-3-left (≈-sym compose-3-right) compose-equiv : {c₂ c₂′ : Cospan B C} {c₁ c₁′ : Cospan A B} - → Same c₂ c₂′ - → Same c₁ c₁′ - → Same (compose c₁ c₂) (compose c₁′ c₂′) + → c₂ ≈ c₂′ + → c₁ ≈ c₁′ + → compose c₁ c₂ ≈ compose c₁′ c₂′ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≈C₂ ≈C₁ = record - { ≅N = up-to-iso P P″ - ; from∘f₁≈f₁′ = begin - ≅P.from ∘ P.i₁ ∘ C₁.f₁ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₁) ∘ C₁.f₁ ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩ - (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁ ≈⟨ assoc ⟩ - P′.i₁ ∘ ≈C₁.from ∘ C₁.f₁ ≈⟨ refl⟩∘⟨ ≈C₁.from∘f₁≈f₁′ ⟩ - P′.i₁ ∘ C₁′.f₁ ∎ - ; from∘f₂≈f₂′ = begin - ≅P.from ∘ P.i₂ ∘ C₂.f₂ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₂) ∘ C₂.f₂ ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩ - (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂ ≈⟨ assoc ⟩ - P′.i₂ ∘ ≈C₂.from ∘ C₂.f₂ ≈⟨ refl⟩∘⟨ ≈C₂.from∘f₂≈f₂′ ⟩ - P′.i₂ ∘ C₂′.f₂ ∎ + { ≅N = ≅P + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where module C₁ = Cospan c₁ module C₁′ = Cospan c₁′ module C₂ = Cospan c₂ module C₂′ = Cospan c₂′ + P : Pushout C₁.f₂ C₂.f₁ P = pushout C₁.f₂ C₂.f₁ + P′ : Pushout C₁′.f₂ C₂′.f₁ P′ = pushout C₁′.f₂ C₂′.f₁ - module ≈C₁ = Same ≈C₁ - module ≈C₂ = Same ≈C₂ + module ≈C₁ = _≈_ ≈C₁ + module ≈C₂ = _≈_ ≈C₂ P′′ : Pushout (≈C₁.to ∘ C₁′.f₂) (≈C₂.to ∘ C₂′.f₁) P′′ = extend-i₂-iso (extend-i₁-iso P′ (≅.sym ≈C₁.≅N)) (≅.sym ≈C₂.≅N) P″ : Pushout C₁.f₂ C₂.f₁ P″ = pushout-resp-≈ P′′ - (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂′)) - (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁′)) + (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂)) + (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁)) module P = Pushout P module P′ = Pushout P′ ≅P : P.Q ≅ P′.Q ≅P = up-to-iso P P″ module ≅P = _≅_ ≅P open HomReasoning + abstract + from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ C₁.f₁ 𝒞.≈ P′.i₁ ∘ C₁′.f₁ + from∘f₁≈f₁ = begin + ≅P.from ∘ P.i₁ ∘ C₁.f₁ ≈⟨ pullˡ P.universal∘i₁≈h₁ ⟩ + (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁ ≈⟨ pullʳ ≈C₁.from∘f₁≈f₁ ⟩ + P′.i₁ ∘ C₁′.f₁ ∎ + from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ C₂.f₂ 𝒞.≈ P′.i₂ ∘ C₂′.f₂ + from∘f₂≈f₂ = begin + ≅P.from ∘ P.i₂ ∘ C₂.f₂ ≈⟨ pullˡ P.universal∘i₂≈h₂ ⟩ + (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂ ≈⟨ pullʳ ≈C₂.from∘f₂≈f₂ ⟩ + P′.i₂ ∘ C₂′.f₂ ∎ Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e) Cospans = record { Obj = Obj ; _⇒_ = Cospan - ; _≈_ = Same - ; id = id-Cospan + ; _≈_ = _≈_ + ; id = identity ; _∘_ = flip compose ; assoc = compose-assoc ; sym-assoc = compose-sym-assoc ; identityˡ = compose-idˡ ; identityʳ = compose-idʳ ; identity² = compose-id² - ; equiv = record - { refl = same-refl - ; sym = same-sym - ; trans = same-trans - } + ; equiv = ≈-equiv ; ∘-resp-≈ = compose-equiv } diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda index c0c62c7..b527265 100644 --- a/Category/Instance/DecoratedCospans.agda +++ b/Category/Instance/DecoratedCospans.agda @@ -18,15 +18,18 @@ module Category.Instance.DecoratedCospans module 𝒞 = FinitelyCocompleteCategory 𝒞 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) open import Categories.Diagram.Pushout using (Pushout) open import Categories.Diagram.Pushout.Properties 𝒞.U using (up-to-iso) -open import Categories.Functor.Properties using ([_]-resp-≅) +open import Categories.Functor.Properties using ([_]-resp-≅; [_]-resp-square) open import Categories.Morphism.Reasoning using (switch-fromtoˡ; glueTrianglesˡ) open import Cospan.Decorated 𝒞 F using (DecoratedCospan) +open import Relation.Binary using (IsEquivalence) open import Data.Product using (_,_) open import Function using (flip) open import Level using (_⊔_) @@ -50,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 @@ -67,64 +70,80 @@ compose c₁ c₂ = record identity : DecoratedCospan A A identity = record - { cospan = Cospans.id-Cospan + { cospan = Cospan.identity ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ] } -record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where +record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where - module C₁ = DecoratedCospan C₁ - module C₂ = DecoratedCospan C₂ + private + module C₁ = DecoratedCospan C₁ + module C₂ = DecoratedCospan C₂ field - cospans-≈ : Cospans.Same C₁.cospan C₂.cospan + cospans-≈ : C₁.cospan Cospan.≈ C₂.cospan - open Cospans.Same cospans-≈ public - open 𝒟 - open Morphism U using (_≅_) + open Cospan._≈_ cospans-≈ public + open Morphism 𝒟.U using (_≅_) field - same-deco : F₁ ≅N.from ∘ C₁.decoration ≈ C₂.decoration + same-deco : F₁ ≅N.from 𝒟.∘ C₁.decoration 𝒟.≈ C₂.decoration ≅F[N] : F₀ C₁.N ≅ F₀ C₂.N ≅F[N] = [ F′ ]-resp-≅ ≅N -same-refl : {C : DecoratedCospan A B} → Same C C -same-refl = record - { cospans-≈ = Cospans.same-refl - ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ - } - where - open 𝒟 - open HomReasoning +infix 4 _≈_ -same-sym : {C C′ : DecoratedCospan A B} → Same C C′ → Same C′ C -same-sym C≅C′ = record - { cospans-≈ = Cospans.same-sym cospans-≈ - ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) - } - where - open Same C≅C′ - open 𝒟.Equiv - -same-trans : {C C′ C″ : DecoratedCospan A B} → Same C C′ → Same C′ C″ → Same C C″ -same-trans C≈C′ C′≈C″ = record - { cospans-≈ = Cospans.same-trans C≈C′.cospans-≈ C′≈C″.cospans-≈ - ; same-deco = - homomorphism ⟩∘⟨refl ○ - glueTrianglesˡ 𝒟.U C′≈C″.same-deco C≈C′.same-deco - } - where - module C≈C′ = Same C≈C′ - module C′≈C″ = Same C′≈C″ - open 𝒟.HomReasoning +module _ where + + open 𝒟.HomReasoning + open 𝒟.Equiv + open 𝒟 using (identityˡ) + + private + variable + f g h : DecoratedCospan A B + + abstract + + ≈-refl : f ≈ f + ≈-refl = record + { cospans-≈ = Cospan.≈-refl + ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ + } + + ≈-sym : f ≈ g → g ≈ f + ≈-sym f≈g = record + { cospans-≈ = Cospan.≈-sym cospans-≈ + ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) + } + where + open _≈_ f≈g + + ≈-trans : f ≈ g → g ≈ h → f ≈ h + ≈-trans f≈g g≈h = record + { cospans-≈ = Cospan.≈-trans f≈g.cospans-≈ g≈h.cospans-≈ + ; same-deco = + homomorphism ⟩∘⟨refl ○ + glueTrianglesˡ 𝒟.U g≈h.same-deco f≈g.same-deco + } + where + module f≈g = _≈_ f≈g + module g≈h = _≈_ g≈h + + ≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B}) + ≈-equiv = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } compose-assoc : {c₁ : DecoratedCospan A B} {c₂ : DecoratedCospan B C} {c₃ : DecoratedCospan C D} - → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃) -compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record + → compose c₁ (compose c₂ c₃) ≈ compose (compose c₁ c₂) c₃ +compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record { cospans-≈ = Cospans.compose-assoc ; same-deco = deco-assoc } @@ -133,14 +152,19 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record module C₂ = DecoratedCospan c₂ module C₃ = DecoratedCospan c₃ open 𝒞 using (+-assoc; pushout; [_,_]; _+₁_; _+_) renaming (_∘_ to _∘′_; id to id′) + p₁ : Pushout 𝒞.U C₁.f₂ C₂.f₁ p₁ = pushout C₁.f₂ C₂.f₁ + p₂ : Pushout 𝒞.U C₂.f₂ C₃.f₁ p₂ = pushout C₂.f₂ C₃.f₁ module P₁ = Pushout p₁ module P₂ = Pushout p₂ + p₃ : Pushout 𝒞.U P₁.i₂ P₂.i₁ p₃ = pushout P₁.i₂ P₂.i₁ + p₁₃ p₄ : Pushout 𝒞.U C₁.f₂ (P₂.i₁ ∘′ C₂.f₁) p₁₃ = glue-i₂ p₁ p₃ - p₂₃ = glue-i₁ p₂ p₃ p₄ = pushout C₁.f₂ (P₂.i₁ ∘′ C₂.f₁) + p₂₃ p₅ : Pushout 𝒞.U (P₁.i₂ ∘′ C₂.f₂) C₃.f₁ + p₂₃ = glue-i₁ p₂ p₃ p₅ = pushout (P₁.i₂ ∘′ C₂.f₂) C₃.f₁ module P₃ = Pushout p₃ module P₄ = Pushout p₄ @@ -151,36 +175,50 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record module P₄≅P₁₃ = _≅_ (up-to-iso p₄ p₁₃) module P₅≅P₂₃ = _≅_ (up-to-iso p₅ p₂₃) + N M P Q R : 𝒞.Obj N = C₁.N M = C₂.N P = C₃.N Q = P₁.Q R = P₂.Q - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute - - a = C₁.f₂ - b = C₂.f₁ - c = C₂.f₂ - d = C₂.f₁ + f : N 𝒞.⇒ Q f = P₁.i₁ + + g : M 𝒞.⇒ Q g = P₁.i₂ + + h : M 𝒞.⇒ R h = P₂.i₁ + + i : P 𝒞.⇒ R i = P₂.i₂ + j : Q 𝒞.⇒ P₃.Q j = P₃.i₁ + + k : R 𝒞.⇒ P₃.Q k = P₃.i₂ + w : N 𝒞.⇒ P₄.Q w = P₄.i₁ + + x : R 𝒞.⇒ P₄.Q x = P₄.i₂ + + y : Q 𝒞.⇒ P₅.Q y = P₅.i₁ + + z : P 𝒞.⇒ P₅.Q z = P₅.i₂ + l : P₂₃.Q 𝒞.⇒ P₅.Q l = P₅≅P₂₃.to + + m : P₄.Q 𝒞.⇒ P₁₃.Q m = P₄≅P₁₃.from - module +-assoc = _≅_ +-assoc + module +-assoc {m} {n} {o} = _≅_ (+-assoc {m} {n} {o}) module _ where @@ -194,23 +232,19 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record open 𝒞.HomReasoning open 𝒞.Equiv - copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from + copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) 𝒞.≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from copairings = begin - ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ pushˡ assoc ⟩ - l ∘ (m ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ refl⟩∘⟨ ∘[] ⟩∘⟨refl ⟩ - l ∘ [ m ∘ w , m ∘ x ] ∘ (id +₁ [ h , i ]) ≈⟨ refl⟩∘⟨ []-cong₂ (P₄.universal∘i₁≈h₁) (P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ - l ∘ [ j ∘ f , k ] ∘ (id +₁ [ h , i ]) ≈⟨ pullˡ ∘[] ⟩ - [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩ - [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []∘+₁ ⟩ - [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ] ≈⟨ []-cong₂ identityʳ (pullʳ ∘[]) ⟩ - [ y ∘ f , l ∘ [ k ∘ h , k ∘ i ] ] ≈⟨ []-congˡ (refl⟩∘⟨ []-congʳ P₃.commute) ⟨ - [ y ∘ f , l ∘ [ j ∘ g , k ∘ i ] ] ≈⟨ []-congˡ ∘[] ⟩ - [ y ∘ f , [ l ∘ j ∘ g , l ∘ k ∘ i ] ] ≈⟨ []-congˡ ([]-congˡ P₂₃.universal∘i₂≈h₂) ⟩ - [ y ∘ f , [ l ∘ j ∘ g , z ] ] ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩ - [ y ∘ f , [ y ∘ g , z ] ] ≈⟨ []∘assocˡ ⟨ - [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨ - [ y ∘ [ f , g ] , z ∘ id ] ∘ +-assoc.from ≈⟨ pullˡ []∘+₁ ⟨ - [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from ∎ + ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ ∘[] ⟩∘⟨refl ⟩ + [(l ∘ m) ∘ w , (l ∘ m) ∘ x ] ∘ (id +₁ [ h , i ]) ≈⟨ []-cong₂ (pullʳ P₄.universal∘i₁≈h₁) (pullʳ P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ + [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩ + [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []∘+₁ ⟩ + [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ] ≈⟨ []-cong₂ identityʳ ∘[] ⟩ + [ y ∘ f , [ (l ∘ k) ∘ h , (l ∘ k) ∘ i ] ] ≈⟨ []-congˡ ([]-cong₂ (pullʳ (sym P₃.commute)) (assoc ○ P₂₃.universal∘i₂≈h₂)) ⟩ + [ y ∘ f , [ l ∘ j ∘ g , z ] ] ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩ + [ y ∘ f , [ y ∘ g , z ] ] ≈⟨ []∘assocˡ ⟨ + [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨ + [ y ∘ [ f , g ] , z ∘ id ] ∘ +-assoc.from ≈⟨ pullˡ []∘+₁ ⟨ + [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from ∎ module _ where @@ -219,153 +253,160 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record open 𝒟 using (_⊗₀_; _⊗₁_; id; _∘_; _≈_; assoc; sym-assoc; identityʳ; ⊗; identityˡ; triangle; assoc-commute-to; assoc-commute-from) open 𝒟 using (_⇒_; unit) - α⇒ = 𝒟.associator.from - α⇐ = 𝒟.associator.to - - λ⇒ = 𝒟.unitorˡ.from - λ⇐ = 𝒟.unitorˡ.to - - ρ⇒ = 𝒟.unitorʳ.from - ρ⇐ = 𝒟.unitorʳ.to - - module α≅ = 𝒟.associator - module λ≅ = 𝒟.unitorˡ - module ρ≅ = 𝒟.unitorʳ + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐) open 𝒟.Equiv + +-α⇒ : {m n o : 𝒞.Obj} → m + (n + o) 𝒞.⇒ (m + n) + o +-α⇒ = +-assoc.from + +-α⇐ : {m n o : 𝒞.Obj} → (m + n) + o 𝒞.⇒ m + (n + o) +-α⇐ = +-assoc.to - s : unit ⇒ F₀ C₁.N + s : unit ⇒ F₀ N s = C₁.decoration - t : unit ⇒ F₀ C₂.N + t : unit ⇒ F₀ M t = C₂.decoration - u : unit ⇒ F₀ C₃.N + u : unit ⇒ F₀ P u = C₃.decoration - F-copairings : F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈ F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ (+-assoc.from) - F-copairings = begin - F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈⟨ pushˡ homomorphism ⟨ - F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F₁ (id′ +₁ [ h , i ]) ≈⟨ homomorphism ⟨ - F₁ (((l ∘′ m) ∘′ [ w , x ]) ∘′ (id′ +₁ [ h , i ])) ≈⟨ F-resp-≈ copairings ⟩ - F₁ ([ y , z ] ∘′ ([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ homomorphism ⟩ - F₁ [ y , z ] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ refl⟩∘⟨ homomorphism ⟩ - F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ +-assoc.from ∎ - - coherences : φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈ F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐ - coherences = begin - φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈⟨ insertʳ α≅.isoʳ ⟩ - ((φ (N , M + P) ∘ id ⊗₁ φ (M , P)) ∘ α⇒) ∘ α⇐ ≈⟨ assoc ⟩∘⟨refl ⟩ - (φ (N , M + P) ∘ id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐ ≈⟨ assoc ⟩ - φ (N , M + P) ∘ (id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐ ≈⟨ extendʳ associativity ⟨ - F₁ +-assoc.to ∘ (φ (N + M , P) ∘ φ (N , M) ⊗₁ id) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩ - F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐ ∎ - - triangle-to : α⇒ ∘ ρ⇐ ⊗₁ id ≈ id ⊗₁ λ⇐ - triangle-to = begin - α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pullˡ identityˡ ⟨ - id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ ⊗.identity ⟩∘⟨refl ⟨ - id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩⊗⟨ λ≅.isoˡ ⟩∘⟨refl ⟨ - id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨ - (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩ - id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ - id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ - id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id) ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩ - id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id ≈⟨ refl⟩∘⟨ ρ≅.isoʳ ⟩⊗⟨refl ⟩ - id ⊗₁ λ⇐ ∘ id ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗.identity ⟩ - id ⊗₁ λ⇐ ∘ id ≈⟨ identityʳ ⟩ - id ⊗₁ λ⇐ ∎ - - unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ - unitors = begin - s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pushˡ split₂ʳ ⟩ - s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨ - s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨ - s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ extendʳ assoc-commute-from ⟨ - α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨ - α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ - - F-l∘m = F₁ (l ∘′ m) + F[l∘m] : F₀ P₄.Q ⇒ F₀ P₅.Q + F[l∘m] = F₁ (l ∘′ m) + + F[w,x] : F₀ (N + R) ⇒ F₀ P₄.Q F[w,x] = F₁ [ w , x ] + + F[h,i] : F₀ (M + P) ⇒ F₀ R F[h,i] = F₁ [ h , i ] + + F[y,z] : F₀ (Q + P) ⇒ F₀ P₅.Q F[y,z] = F₁ [ y , z ] + + F[f,g] : F₀ (N + M) ⇒ F₀ Q F[f,g] = F₁ [ f , g ] - F-[f,g]+id = F₁ ([ f , g ] +₁ id′) - F-id+[h,i] = F₁ (id′ +₁ [ h , i ]) - φ-N,R = φ (N , R) - φ-M,P = φ (M , P) - φ-N+M,P = φ (N + M , P) - φ-N+M = φ (N , M) - φ-N,M+P = φ (N , M + P) - φ-N,M = φ (N , M) - φ-Q,P = φ (Q , P) + + F[[f,g]+id] : F₀ ((N + M) + P) ⇒ F₀ (Q + P) + F[[f,g]+id] = F₁ ([ f , g ] +₁ id′) + + F[id+[h,i]] : F₀ (N + (M + P)) ⇒ F₀ (N + R) + F[id+[h,i]] = F₁ (id′ +₁ [ h , i ]) + + φ[N,R] : F₀ N ⊗₀ F₀ R 𝒟.⇒ F₀ (N + R) + φ[N,R] = ⊗-homo.η (N , R) + + φ[M,P] : F₀ M ⊗₀ F₀ P 𝒟.⇒ F₀ (M + P) + φ[M,P] = ⊗-homo.η (M , P) + + φ[N+M,P] : F₀ (N + M) ⊗₀ F₀ P 𝒟.⇒ F₀ ((N + M) + P) + φ[N+M,P] = ⊗-homo.η (N + M , P) + + φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M) + φ[N,M] = ⊗-homo.η (N , M) + + φ[N,M+P] : F₀ N ⊗₀ F₀ (M + P) 𝒟.⇒ F₀ (N + (M + P)) + φ[N,M+P] = ⊗-homo.η (N , M + P) + + φ[Q,P] : F₀ Q ⊗₀ F₀ P 𝒟.⇒ F₀ (Q + P) + φ[Q,P] = ⊗-homo.η (Q , P) + + s⊗[t⊗u] : unit 𝒟.⇒ F₀ N ⊗₀ (F₀ M ⊗₀ F₀ P) s⊗[t⊗u] = s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ + + [s⊗t]⊗u : unit 𝒟.⇒ (F₀ N ⊗₀ F₀ M) ⊗₀ F₀ P [s⊗t]⊗u = (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ - deco-assoc - : F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ - ≈ F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ - deco-assoc = begin - F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pullˡ refl ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ-M,P ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨ refl ⟨ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , [ h , i ])) ⟩ - (F-l∘m ∘ F[w,x]) ∘ F-id+[h,i] ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ pullˡ assoc ⟩ - (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ - (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ id ⊗₁ φ-M,P ∘ s⊗[t⊗u] ≈⟨ refl⟩∘⟨ sym-assoc ⟩ - (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ (φ-N,M+P ∘ id ⊗₁ φ-M,P) ∘ s⊗[t⊗u] ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩ - (F[y,z] ∘ F-[f,g]+id ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩ - ((F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨ - (F[y,z] ∘ F-[f,g]+id) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ F₁ id′ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ id ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ identityˡ ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ ((φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ cancelInner α≅.isoˡ ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ assoc ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ - F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ - F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute ([ f , g ] , id′)) ⟨ - F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ F₁ id′ ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨ refl ⟩ - F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ id ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ - F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ - -compose-idʳ : {C : DecoratedCospan A B} → Same (compose identity C) C + abstract + F-copairings : F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]] 𝒟.≈ F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-assoc.from + F-copairings = begin + F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]] ≈⟨ pushˡ homomorphism ⟨ + F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F[id+[h,i]] ≈⟨ [ F′ ]-resp-square copairings ⟩ + F[y,z] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ refl⟩∘⟨ homomorphism ⟩ + F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-assoc.from ∎ + + coherences : φ[N,M+P] ∘ id ⊗₁ φ[M,P] 𝒟.≈ F₁ +-assoc.to ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐ + coherences = begin + φ[N,M+P] ∘ id ⊗₁ φ[M,P] ≈⟨ refl⟩∘⟨ insertʳ 𝒟.associator.isoʳ ⟩ + φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ α⇒) ∘ α⇐ ≈⟨ extendʳ associativity ⟨ + F₁ +-assoc.to ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩ + F₁ +-assoc.to ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐ ∎ + + triangle-to : α⇒ {𝒟.unit} {𝒟.unit} {𝒟.unit} ∘ ρ⇐ ⊗₁ id 𝒟.≈ id ⊗₁ λ⇐ + triangle-to = begin + α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pullˡ identityˡ ⟨ + id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ ⊗.identity ⟩∘⟨refl ⟨ + id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩⊗⟨ 𝒟.unitorˡ.isoˡ ⟩∘⟨refl ⟨ + id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨ + (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩ + id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ + id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id) ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩ + id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id ≈⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟩⊗⟨refl ⟩ + id ⊗₁ λ⇐ ∘ id ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗.identity ⟩ + id ⊗₁ λ⇐ ∘ id ≈⟨ identityʳ ⟩ + id ⊗₁ λ⇐ ∎ + + unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ 𝒟.≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + unitors = begin + s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pushˡ split₂ʳ ⟩ + s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨ + s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨ + s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ extendʳ assoc-commute-from ⟨ + α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨ + α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ + + deco-assoc + : F[l∘m] ∘ (F[w,x] ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐) + 𝒟.≈ F[y,z] ∘ φ[Q,P] ∘ (F[f,g] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + deco-assoc = begin + F[l∘m] ∘ F[w,x] ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pullˡ refl ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (id′ , [ h , i ])) ⟩ + (F[l∘m] ∘ F[w,x]) ∘ F[id+[h,i]] ∘ φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ pullˡ assoc ⟩ + (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ φ[N,M+P] ∘ id ⊗₁ φ[M,P] ∘ s⊗[t⊗u] ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ (φ[N,M+P] ∘ id ⊗₁ φ[M,P]) ∘ s⊗[t⊗u] ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩ + (F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩ + ((F[y,z] ∘ F[[f,g]+id]) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨ + (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ id′ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ id ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ identityˡ ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ ((φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ cancelInner 𝒟.associator.isoˡ ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ assoc ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ + F[y,z] ∘ F[[f,g]+id] ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + F[y,z] ∘ F[[f,g]+id] ∘ φ[N+M,P] ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute ([ f , g ] , id′)) ⟨ + F[y,z] ∘ φ[Q,P] ∘ F[f,g] ⊗₁ F₁ id′ ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟩ + F[y,z] ∘ φ[Q,P] ∘ F[f,g] ⊗₁ id ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + F[y,z] ∘ φ[Q,P] ∘ (F[f,g] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ + +compose-idʳ : {C : DecoratedCospan A B} → compose identity C ≈ C compose-idʳ {A} {_} {C} = record { cospans-≈ = Cospans.compose-idʳ ; same-deco = deco-id } where - open DecoratedCospan C - - open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡) - + open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡; _+_) P = pushout 𝒞.id f₁ P′ = pushout-id-g {g = f₁} ≅P = up-to-iso P P′ - open Morphism 𝒞.U using (_≅_) module ≅P = _≅_ ≅P - open Pushout P - open 𝒞 using (cocartesian) renaming (id to id′; _∘_ to _∘′_) - open CocartesianMonoidal 𝒞.U cocartesian using (⊥+A≅A) - module ⊥+A≅A {a} = _≅_ (⊥+A≅A {a}) - module _ where - open 𝒞 using ( _⇒_ ; _∘_ ; _≈_ ; id ; U @@ -374,17 +415,13 @@ compose-idʳ {A} {_} {C} = record ; ∘[] ; []∘+₁ ; inject₂ ; assoc ; module HomReasoning ; module Dual ; module Equiv ) - open Equiv - open Dual.op-binaryProducts cocartesian using () renaming (⟨⟩-cong₂ to []-cong₂) - open ⇒-Reasoning U open HomReasoning - - copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to ≈ id + copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to 𝒞.≈ id copairing-id = begin ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to ≈⟨ assoc ⟩ (≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id) ∘ ⊥+A≅A.to ≈⟨ assoc ⟩ @@ -394,62 +431,54 @@ compose-idʳ {A} {_} {C} = record [ f₁ ∘ ¡ , id ∘ id ] ∘ ⊥+A≅A.to ≈⟨ []-cong₂ (sym (¡-unique (f₁ ∘ ¡))) identity² ⟩∘⟨refl ⟩ [ ¡ , id ] ∘ ⊥+A≅A.to ≈⟨ inject₂ ⟩ id ∎ - module _ where - open 𝒟 using ( id ; _∘_ ; _≈_ ; _⇒_ ; U ; assoc ; sym-assoc; identityˡ - ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ + ; monoidal ; _⊗₀_; _⊗₁_ ; unit ; unitorˡ ; unitorʳ ) - open ⊗-Reasoning monoidal open ⇒-Reasoning U - - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute - - module λ≅ = unitorˡ - λ⇒ = λ≅.from - λ⇐ = unitorˡ.to - ρ⇐ = unitorʳ.to - - open Coherence monoidal using (λ₁≅ρ₁⇐) + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (λ⇒; λ⇐; ρ⇐) + open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐) open 𝒟.Equiv - s : unit ⇒ F₀ N s = decoration - - cohere-s : φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈ F₁ ⊥+A≅A.to ∘ s - cohere-s = begin - φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ identityˡ ⟨ - id ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ - F₁ id′ ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨ - F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ - F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ - F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε ⊗₁ id) ∘ (id ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ - F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ (⊥ , N) ∘ (ε ⊗₁ id)) ∘ (id ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryˡ ⟩ - F₁ ⊥+A≅A.to ∘ λ⇒ ∘ (id ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ λ₁≅ρ₁⇐ ⟨ - F₁ ⊥+A≅A.to ∘ λ⇒ ∘ (id ⊗₁ s) ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-to ⟨ - F₁ ⊥+A≅A.to ∘ λ⇒ ∘ λ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ λ≅.isoʳ ⟩ - F₁ ⊥+A≅A.to ∘ s ∎ - - deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s - deco-id = begin - F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ id) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , id′)) ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ F₁ ⊥+A≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ - F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘′ ⊥+A≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ - F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ - id ∘ s ≈⟨ identityˡ ⟩ - s ∎ - -compose-idˡ : {C : DecoratedCospan A B} → Same (compose C identity) C + φ[⊥,N] : F₀ ⊥ ⊗₀ F₀ N ⇒ F₀ (⊥ + N) + φ[⊥,N] = ⊗-homo.η (⊥ , N) + φ[A,N] : F₀ A ⊗₀ F₀ N ⇒ F₀ (A + N) + φ[A,N] = ⊗-homo.η (A , N) + abstract + cohere-s : φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ 𝒟.≈ F₁ ⊥+A≅A.to ∘ s + cohere-s = begin + φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ identityˡ ⟨ + id ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ + F₁ id′ ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨ + F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ + F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ + F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ[⊥,N] ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ + F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ[⊥,N] ∘ ε ⊗₁ id) ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryˡ ⟩ + F₁ ⊥+A≅A.to ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ λ₁≅ρ₁⇐ ⟨ + F₁ ⊥+A≅A.to ∘ λ⇒ ∘ id ⊗₁ s ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-to ⟨ + F₁ ⊥+A≅A.to ∘ λ⇒ ∘ λ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ 𝒟.unitorˡ.isoʳ ⟩ + F₁ ⊥+A≅A.to ∘ s ∎ + deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ 𝒟.≈ s + deco-id = begin + F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ⊗₁ id) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (¡ , id′)) ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ[⊥,N] ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ[⊥,N] ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ F₁ ⊥+A≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ + F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘′ ⊥+A≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ + F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ + id ∘ s ≈⟨ identityˡ ⟩ + s ∎ + +compose-idˡ : {C : DecoratedCospan A B} → compose C identity ≈ C compose-idˡ {_} {B} {C} = record { cospans-≈ = Cospans.compose-idˡ ; same-deco = deco-id @@ -497,7 +526,7 @@ compose-idˡ {_} {B} {C} = record open ⇒-Reasoning U open HomReasoning - copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to ≈ id + copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to 𝒞.≈ id copairing-id = begin ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to ≈⟨ assoc ⟩ (≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡) ∘ A+⊥≅A.to ≈⟨ assoc ⟩ @@ -510,11 +539,12 @@ compose-idˡ {_} {B} {C} = record module _ where + open 𝒞 using (_+_) open 𝒟 using ( id ; _∘_ ; _≈_ ; _⇒_ ; U ; assoc ; sym-assoc; identityˡ - ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ + ; monoidal ; _⊗₀_; _⊗₁_ ; unit ; unitorˡ ; unitorʳ ; unitorʳ-commute-to ; module Equiv ) @@ -523,129 +553,146 @@ compose-idˡ {_} {B} {C} = record open ⊗-Reasoning monoidal open ⇒-Reasoning U - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute + φ[N,⊥] : F₀ N ⊗₀ F₀ ⊥ 𝒟.⇒ F₀ (N + ⊥) + φ[N,⊥] = ⊗-homo.η (N , ⊥) - module ρ≅ = unitorʳ - ρ⇒ = ρ≅.from - ρ⇐ = ρ≅.to + φ[N,B] : F₀ N ⊗₀ F₀ B 𝒟.⇒ F₀ (N + B) + φ[N,B] = ⊗-homo.η (N , B) s : unit ⇒ F₀ N s = decoration - cohere-s : φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈ F₁ A+⊥≅A.to ∘ s - cohere-s = begin - φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ identityˡ ⟨ - id ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ - F₁ id′ ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨ - F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ - F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩ - F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (id ⊗₁ ε) ∘ (s ⊗₁ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ - F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ (N , ⊥) ∘ (id ⊗₁ ε)) ∘ (s ⊗₁ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryʳ ⟩ - F₁ A+⊥≅A.to ∘ ρ⇒ ∘ (s ⊗₁ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-to ⟨ - F₁ A+⊥≅A.to ∘ ρ⇒ ∘ ρ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ ρ≅.isoʳ ⟩ - F₁ A+⊥≅A.to ∘ s ∎ - - deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s - deco-id = begin - F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (id ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (F₁ id′ ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , ¡)) ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ F₁ A+⊥≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ - F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘′ A+⊥≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ - F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ - id ∘ s ≈⟨ identityˡ ⟩ - s ∎ - -compose-id² : Same {A} (compose identity identity) identity + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) + + abstract + cohere-s : φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ 𝒟.≈ F₁ A+⊥≅A.to ∘ s + cohere-s = begin + φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ identityˡ ⟨ + id ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ + F₁ id′ ∘ φ[N,⊥] ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨ + F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ + F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩ + F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ[N,⊥] ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ + F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ[N,⊥] ∘ id ⊗₁ ε) ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryʳ ⟩ + F₁ A+⊥≅A.to ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-to ⟨ + F₁ A+⊥≅A.to ∘ ρ⇒ ∘ ρ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ unitorʳ.isoʳ ⟩ + F₁ A+⊥≅A.to ∘ s ∎ + + deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ 𝒟.≈ s + deco-id = begin + F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ F₁ id′ ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (id′ , ¡)) ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ F₁ A+⊥≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ + F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘′ A+⊥≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ + F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ + id ∘ s ≈⟨ identityˡ ⟩ + s ∎ + +compose-id² : compose identity identity ≈ identity {A} compose-id² = compose-idˡ compose-equiv : {c₂ c₂′ : DecoratedCospan B C} {c₁ c₁′ : DecoratedCospan A B} - → Same c₂ c₂′ - → Same c₁ c₁′ - → Same (compose c₁ c₂) (compose c₁′ c₂′) + → c₂ ≈ c₂′ + → c₁ ≈ c₁′ + → compose c₁ c₂ ≈ (compose c₁′ c₂′) compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = record { cospans-≈ = ≅C₂∘C₁ ; same-deco = F≅N∘C₂∘C₁≈C₂′∘C₁′ } where - module ≅C₁ = Same ≅C₁ - module ≅C₂ = Same ≅C₂ + module ≅C₁ = _≈_ ≅C₁ + module ≅C₂ = _≈_ ≅C₂ module C₁ = DecoratedCospan c₁ module C₁′ = DecoratedCospan c₁′ module C₂ = DecoratedCospan c₂ module C₂′ = DecoratedCospan c₂′ ≅C₂∘C₁ = Cospans.compose-equiv ≅C₂.cospans-≈ ≅C₁.cospans-≈ - module ≅C₂∘C₁ = Cospans.Same ≅C₂∘C₁ + module ≅C₂∘C₁ = Cospan._≈_ ≅C₂∘C₁ P = 𝒞.pushout C₁.f₂ C₂.f₁ P′ = 𝒞.pushout C₁′.f₂ C₂′.f₁ module P = Pushout P module P′ = Pushout P′ - s = C₁.decoration - t = C₂.decoration - s′ = C₁′.decoration - t′ = C₂′.decoration + N M N′ M′ : 𝒞.Obj N = C₁.N M = C₂.N N′ = C₁′.N M′ = C₂′.N - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute + s : 𝒟.unit 𝒟.⇒ F₀ N + s = C₁.decoration + t : 𝒟.unit 𝒟.⇒ F₀ M + t = C₂.decoration + + s′ : 𝒟.unit 𝒟.⇒ F₀ N′ + s′ = C₁′.decoration + + t′ : 𝒟.unit 𝒟.⇒ F₀ M′ + t′ = C₂′.decoration + + Q⇒ : ≅C₂∘C₁.C.N 𝒞.⇒ ≅C₂∘C₁.D.N Q⇒ = ≅C₂∘C₁.≅N.from + + N⇒ : ≅C₁.C.N 𝒞.⇒ ≅C₁.D.N N⇒ = ≅C₁.≅N.from + + M⇒ : ≅C₂.C.N 𝒞.⇒ ≅C₂.D.N M⇒ = ≅C₂.≅N.from module _ where - ρ⇒ = 𝒟.unitorʳ.from - ρ⇐ = 𝒟.unitorʳ.to + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (ρ⇒; ρ⇐) - open 𝒞 using ([_,_]; ∘[]; _+₁_; []∘+₁) renaming (_∘_ to _∘′_) + open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁) renaming (_∘_ to _∘′_) open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian using () renaming (⟨⟩-cong₂ to []-cong₂) open 𝒟 + φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M) + φ[N,M] = ⊗-homo.η (N , M) + + φ[N′,M′] : F₀ N′ ⊗₀ F₀ M′ 𝒟.⇒ F₀ (N′ + M′) + φ[N′,M′] = ⊗-homo.η (N′ , M′) + open ⊗-Reasoning monoidal open ⇒-Reasoning U - F≅N∘C₂∘C₁≈C₂′∘C₁′ : F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈ F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐ - F≅N∘C₂∘C₁≈C₂′∘C₁′ = begin - F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ (Q⇒ ∘′ [ P.i₁ , P.i₂ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ∘[] ⟩∘⟨refl ⟩ - F₁ ([ Q⇒ ∘′ P.i₁ , Q⇒ ∘′ P.i₂ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ([]-cong₂ P.universal∘i₁≈h₁ P.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ - F₁ ([ P′.i₁ ∘′ N⇒ , P′.i₂ ∘′ M⇒ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ []∘+₁ ⟩∘⟨refl ⟨ - F₁ ([ P′.i₁ , P′.i₂ ] ∘′ (N⇒ +₁ M⇒)) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ - F₁ [ P′.i₁ , P′.i₂ ] ∘ F₁ (N⇒ +₁ M⇒) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (N⇒ , M⇒)) ⟨ - F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ F₁ N⇒ ⊗₁ F₁ M⇒ ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟨ - F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ (F₁ N⇒ ∘ s) ⊗₁ (F₁ M⇒ ∘ t) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ≅C₁.same-deco ⟩⊗⟨ ≅C₂.same-deco ⟩∘⟨refl ⟩ - F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐ ∎ + abstract + F≅N∘C₂∘C₁≈C₂′∘C₁′ : F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ 𝒟.≈ F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ s′ ⊗₁ t′ ∘ ρ⇐ + F≅N∘C₂∘C₁≈C₂′∘C₁′ = begin + F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ (Q⇒ ∘′ [ P.i₁ , P.i₂ ]) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ∘[] ⟩∘⟨refl ⟩ + F₁ ([ Q⇒ ∘′ P.i₁ , Q⇒ ∘′ P.i₂ ]) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ([]-cong₂ P.universal∘i₁≈h₁ P.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ + F₁ ([ P′.i₁ ∘′ N⇒ , P′.i₂ ∘′ M⇒ ]) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ []∘+₁ ⟩∘⟨refl ⟨ + F₁ ([ P′.i₁ , P′.i₂ ] ∘′ (N⇒ +₁ M⇒)) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ + F₁ [ P′.i₁ , P′.i₂ ] ∘ F₁ (N⇒ +₁ M⇒) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (N⇒ , M⇒)) ⟨ + F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ F₁ N⇒ ⊗₁ F₁ M⇒ ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟨ + F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ (F₁ N⇒ ∘ s) ⊗₁ (F₁ M⇒ ∘ t) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ≅C₁.same-deco ⟩⊗⟨ ≅C₂.same-deco ⟩∘⟨refl ⟩ + F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ s′ ⊗₁ t′ ∘ ρ⇐ ∎ DecoratedCospans : Category o (o ⊔ ℓ ⊔ ℓ′) (ℓ ⊔ e ⊔ e′) DecoratedCospans = record { Obj = 𝒞.Obj ; _⇒_ = DecoratedCospan - ; _≈_ = Same + ; _≈_ = _≈_ ; id = identity ; _∘_ = flip compose ; assoc = compose-assoc - ; sym-assoc = same-sym (compose-assoc) + ; sym-assoc = ≈-sym compose-assoc ; identityˡ = compose-idˡ ; identityʳ = compose-idʳ ; identity² = compose-id² - ; equiv = record - { refl = same-refl - ; sym = same-sym - ; trans = same-trans - } + ; equiv = ≈-equiv ; ∘-resp-≈ = compose-equiv } diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda index 0847165..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 } _×_ diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda index 1452669..c6261bb 100644 --- a/Category/Instance/One/Properties.agda +++ b/Category/Instance/One/Properties.agda @@ -8,7 +8,7 @@ open import Categories.Category.Core using (Category) open import Categories.Category.Instance.One using () renaming (One to One′) One : Category o ℓ e -One = One′ +One = One′ {o} {ℓ} {e} open import Categories.Category.Cocartesian One using (Cocartesian) open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete) @@ -16,20 +16,20 @@ open import Categories.Object.Initial One using (Initial) open import Categories.Category.Cocartesian One using (BinaryCoproducts) -One-Initial : Initial -One-Initial = _ +initial : Initial +initial = _ -One-BinaryCoproducts : BinaryCoproducts -One-BinaryCoproducts = _ +coproducts : BinaryCoproducts +coproducts = _ -One-Cocartesian : Cocartesian -One-Cocartesian = record - { initial = One-Initial - ; coproducts = One-BinaryCoproducts +cocartesian : Cocartesian +cocartesian = record + { initial = initial + ; coproducts = coproducts } -One-FinitelyCocomplete : FinitelyCocomplete -One-FinitelyCocomplete = record - { cocartesian = One-Cocartesian +finitelyCocomplete : FinitelyCocomplete +finitelyCocomplete = record + { cocartesian = cocartesian ; coequalizer = _ } diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda new file mode 100644 index 0000000..fa15295 --- /dev/null +++ b/Category/Instance/Properties/SymMonCat.agda @@ -0,0 +1,166 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level; suc; _⊔_) +module Category.Instance.Properties.SymMonCat {o ℓ e : Level} where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI +import Categories.Functor.Monoidal.Symmetric {o} {o} {ℓ} {ℓ} {e} {e} as SMF + +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) + +open import Categories.Category using (Category; _[_≈_]; _[_∘_]) +open import Categories.Object.Product.Core SymMonCat using (Product) +open import Categories.Object.Terminal SymMonCat using (Terminal) +open import Categories.Category.Instance.One using (One) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Category.Cartesian SymMonCat using (Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts) +open import Categories.Functor.Monoidal.Construction.Product + using () + renaming + ( πˡ-SymmetricMonoidalFunctor to πˡ-SMF + ; πʳ-SymmetricMonoidalFunctor to πʳ-SMF + ; ※-SymmetricMonoidalFunctor to ※-SMF + ) +open import Categories.Category.Monoidal.Construction.Product using (Product-SymmetricMonoidalCategory) +open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u) +open import Data.Product.Base using (_,_; proj₁; proj₂) + +open SMF.Lax using (SymmetricMonoidalFunctor) +open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + +module Cone + {A B X : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor X A} + {G : SymmetricMonoidalFunctor X B} where + + module A = SymmetricMonoidalCategory A + module B = SymmetricMonoidalCategory B + module X = SymmetricMonoidalCategory X + module F = SymmetricMonoidalFunctor X A F + module G = SymmetricMonoidalFunctor X B G + + A×B : SymmetricMonoidalCategory o ℓ e + A×B = (Product-SymmetricMonoidalCategory A B) + + πˡ : SymmetricMonoidalFunctor A×B A + πˡ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + + πʳ : SymmetricMonoidalFunctor A×B B + πʳ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + + module _ where + open Category A.U + open Equiv + open ⇒-Reasoning A.U + open ⊗-Reasoning A.monoidal + project₁ : SymMonCat [ SymMonCat [ πˡ ∘ ※-SMF F G ] ≈ F ] + project₁ = record + { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = identityˡ ○ identityʳ + ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym A.⊗.identity } + } + } + module _ (H : SymmetricMonoidalFunctor X A×B) (eq₁ : SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]) where + private + module H = SymmetricMonoidalFunctor X A×B H + open SymmetricMonoidalNaturalIsomorphism eq₁ + ε-compat₁ : ⇐.η X.unit A.∘ F.ε A.≈ H.ε .proj₁ + ε-compat₁ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ + ⊗-homo-compat₁ + : ∀ {C D} + → ⇐.η (X.⊗.₀ (C , D)) ∘ F.⊗-homo.η (C , D) + ≈ H.⊗-homo.η (C , D) .proj₁ ∘ A.⊗.₁ (⇐.η C , ⇐.η D) + ⊗-homo-compat₁ {C} {D} = + insertʳ + (sym ⊗-distrib-over-∘ + ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D + ○ A.⊗.identity) + ○ (pullʳ (sym ⊗-homo-compat) + ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D))) + ○ identityʳ) ⟩∘⟨refl + + module _ where + open Category B.U + open Equiv + open ⇒-Reasoning B.U + open ⊗-Reasoning B.monoidal + project₂ : SymMonCat [ SymMonCat [ πʳ ∘ ※-SMF F G ] ≈ G ] + project₂ = record + { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = identityˡ ○ identityʳ + ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym B.⊗.identity } + } + } + module _ (H : SymmetricMonoidalFunctor X A×B) (eq₂ : SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]) where + private + module H = SymmetricMonoidalFunctor X A×B H + open SymmetricMonoidalNaturalIsomorphism eq₂ + ε-compat₂ : ⇐.η X.unit ∘ G.ε ≈ H.ε .proj₂ + ε-compat₂ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ + ⊗-homo-compat₂ + : ∀ {C D} + → ⇐.η (X.⊗.₀ (C , D)) ∘ G.⊗-homo.η (C , D) + ≈ H.⊗-homo.η (C , D) .proj₂ ∘ B.⊗.₁ (⇐.η C , ⇐.η D) + ⊗-homo-compat₂ {C} {D} = + insertʳ + (sym ⊗-distrib-over-∘ + ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D + ○ B.⊗.identity) + ○ (pullʳ (sym ⊗-homo-compat) + ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D))) + ○ identityʳ) ⟩∘⟨refl + + unique + : (H : SymmetricMonoidalFunctor X A×B) + → SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ] + → SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ] + → SymMonCat [ ※-SMF F G ≈ H ] + unique H eq₁ eq₂ = record + { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} {H.F} eq₁.U eq₂.U + ; F⇒G-isMonoidal = record + { ε-compat = ε-compat₁ H eq₁ , ε-compat₂ H eq₂ + ; ⊗-homo-compat = ⊗-homo-compat₁ H eq₁ , ⊗-homo-compat₂ H eq₂ + } + } + where + module H = SymmetricMonoidalFunctor X A×B H + module eq₁ = SymmetricMonoidalNaturalIsomorphism eq₁ + module eq₂ = SymmetricMonoidalNaturalIsomorphism eq₂ + +prod-SymMonCat : ∀ {A B} → Product A B +prod-SymMonCat {A} {B} = record + { A×B = Product-SymmetricMonoidalCategory A B + ; π₁ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + ; π₂ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + ; ⟨_,_⟩ = ※-SMF + ; project₁ = λ { {X} {f} {g} → Cone.project₁ {A} {B} {X} {f} {g} } + ; project₂ = λ { {X} {f} {g} → Cone.project₂ {A} {B} {X} {f} {g} } + ; unique = λ { {X} {h} {f} {g} eq₁ eq₂ → Cone.unique {A} {B} {X} {f} {g} h eq₁ eq₂ } + } + +SymMonCat-BinaryProducts : BinaryProducts +SymMonCat-BinaryProducts = record { product = prod-SymMonCat } + +SymMonCat-Terminal : Terminal +SymMonCat-Terminal = record + { ⊤ = record + { U = One + ; monoidal = _ + ; symmetric = _ + } + ; ⊤-is-terminal = _ + } + +SymMonCat-Cartesian : Cartesian +SymMonCat-Cartesian = record + { terminal = SymMonCat-Terminal + ; products = SymMonCat-BinaryProducts + } diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda index fa4d903..995ddf3 100644 --- a/Category/Instance/Setoids/SymmetricMonoidal.agda +++ b/Category/Instance/Setoids/SymmetricMonoidal.agda @@ -1,33 +1,47 @@ {-# OPTIONS --without-K --safe #-} -module Category.Instance.Setoids.SymmetricMonoidal {ℓ} where +open import Level using (Level; _⊔_; suc) +module Category.Instance.Setoids.SymmetricMonoidal {c ℓ : Level} where -open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian; Setoids-Cocartesian) renaming (Setoids-Monoidal to ×-monoidal) -open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids ℓ ℓ) Setoids-Cartesian +open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids c ℓ) Setoids-Cartesian using () renaming (symmetric to ×-symmetric) -open import Level using (suc) -open import Categories.Category.Cocartesian (Setoids ℓ ℓ) +open import Categories.Category.Cocartesian (Setoids c (c ⊔ ℓ)) using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) -open CocartesianMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-monoidal) -open CocartesianSymmetricMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-symmetric) +open CocartesianMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-monoidal) +open CocartesianSymmetricMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-symmetric) -Setoids-× : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) + +opaque + + ×-monoidal′ : Monoidal (Setoids c ℓ) + ×-monoidal′ = ×-monoidal {c} {ℓ} + + ×-symmetric′ : Symmetric ×-monoidal′ + ×-symmetric′ = ×-symmetric + +Setoids-× : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids-× = record - { U = Setoids ℓ ℓ - ; monoidal = ×-monoidal - ; symmetric = ×-symmetric + { U = Setoids c ℓ + ; monoidal = ×-monoidal′ + ; symmetric = ×-symmetric′ } -Setoids-+ : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ +Setoids-+ : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids-+ = record - { U = Setoids ℓ ℓ + { U = Setoids c (c ⊔ ℓ) ; monoidal = +-monoidal ; symmetric = +-symmetric } + +module Setoids-× = SymmetricMonoidalCategory Setoids-× +module Setoids-+ = SymmetricMonoidalCategory Setoids-+ diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda new file mode 100644 index 0000000..e4b136c --- /dev/null +++ b/Category/Instance/SymMonCat.agda @@ -0,0 +1,74 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level; suc; _⊔_) +module Category.Instance.SymMonCat {o ℓ e : Level} where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Functor.Monoidal.Symmetric as SMF +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Morphism as Morphism +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI +import Categories.Category.Monoidal.Utilities as MonoidalUtil +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +open import Relation.Binary.Core using (Rel) + +open import Categories.Category using (Category; _[_,_]; _[_∘_]) +open import Categories.Category.Helper using (categoryHelper) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) + +open SMF.Lax using (SymmetricMonoidalFunctor) +open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + +assoc + : {A B C D : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + {G : SymmetricMonoidalFunctor B C} + {H : SymmetricMonoidalFunctor C D} + → SymmetricMonoidalNaturalIsomorphism + (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F) + (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F)) +assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H} + +identityˡ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F +identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + +identityʳ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F +identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + +Compose + : {A B C : SymmetricMonoidalCategory o ℓ e} + → SymmetricMonoidalFunctor B C + → SymmetricMonoidalFunctor A B + → SymmetricMonoidalFunctor A C +Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G + +∘-resp-≈ + : {A B C : SymmetricMonoidalCategory o ℓ e} + {f h : SymmetricMonoidalFunctor B C} + {g i : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism f h + → SymmetricMonoidalNaturalIsomorphism g i + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i) +∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′ + +SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +SymMonCat = categoryHelper record + { Obj = SymmetricMonoidalCategory o ℓ e + ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e} + ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} } + ; id = λ { {X} → idF-SymmetricMonoidal X } + ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G } + ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} } + ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} } + ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} } + ; equiv = isEquivalence + ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i } + } diff --git a/Category/Monoidal/Instance/Cospans.agda b/Category/Monoidal/Instance/Cospans.agda index 228ddea..a1648db 100644 --- a/Category/Monoidal/Instance/Cospans.agda +++ b/Category/Monoidal/Instance/Cospans.agda @@ -18,8 +18,9 @@ open import Categories.Category.Monoidal.Core using (Monoidal) open import Categories.Functor using (Functor) open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) -open import Category.Instance.Cospans 𝒞 using (Cospans; Cospan) -open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan using (Cospan; cospan) +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC) open import Category.Monoidal.Instance.Cospans.Lift {o} {ℓ} {e} using (module Square) open import Data.Product.Base using (_,_) open import Functor.Instance.Cospan.Stack 𝒞 using (⊗) @@ -61,7 +62,6 @@ CospansMonoidal = record ; pentagon = pentagon } where - module ⊗ = Functor ⊗ module Cospans = Category Cospans module Unitorˡ = Square ⊥+--id module Unitorʳ = Square -+⊥-id @@ -83,16 +83,15 @@ CospansMonoidal = record CospansBraided : Braided CospansMonoidal CospansBraided = record { braiding = niHelper record - { η = λ { (X , Y) → Braiding.FX≅GX′.from {X , Y} } - ; η⁻¹ = λ { (Y , X) → Braiding.FX≅GX′.to {Y , X} } - ; commute = λ { {X , Y} {X′ , Y′} (f , g) → Braiding.from (record { f₁ = f₁ f , f₁ g ; f₂ = f₂ f , f₂ g }) } - ; iso = λ { (X , Y) → Braiding.FX≅GX′.iso {X , Y} } + { η = λ (X , Y) → Braiding.FX≅GX′.from {X , Y} + ; η⁻¹ = λ (Y , X) → Braiding.FX≅GX′.to {Y , X} + ; commute = λ (cospan f₁ f₂ , cospan g₁ g₂) → Braiding.from (cospan (f₁ , g₁) (f₂ , g₂)) + ; iso = λ (X , Y) → Braiding.FX≅GX′.iso {X , Y} } ; hexagon₁ = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym homomorphism ○ sym homomorphism ○ L-resp-≈ hex₁ ○ homomorphism ○ refl⟩∘⟨ homomorphism ; hexagon₂ = sym L-resp-⊗ ⟩∘⟨refl ⟩∘⟨ sym L-resp-⊗ ○ sym homomorphism ⟩∘⟨refl ○ sym homomorphism ○ L-resp-≈ hex₂ ○ homomorphism ○ homomorphism ⟩∘⟨refl } where - open Cospan module Cospans = Category Cospans open Cospans.Equiv open Cospans.HomReasoning diff --git a/Category/Monoidal/Instance/Cospans/Lift.agda b/Category/Monoidal/Instance/Cospans/Lift.agda index fa31fcb..c7e7516 100644 --- a/Category/Monoidal/Instance/Cospans/Lift.agda +++ b/Category/Monoidal/Instance/Cospans/Lift.agda @@ -4,7 +4,7 @@ open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategor module Category.Monoidal.Instance.Cospans.Lift {o ℓ e} where -open import Category.Instance.Cospans using (Cospans; Cospan; Same) +open import Category.Instance.Cospans using (Cospans) open import Categories.Category.Core using (Category) @@ -16,6 +16,7 @@ import Category.Diagram.Pushout as PushoutDiagram′ import Functor.Instance.Cospan.Embed as CospanEmbed open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; module Definitions) +open import Category.Diagram.Cospan using (Cospan; cospan) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_) @@ -26,7 +27,7 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} {𝒟 : FinitelyCocompleteC module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = FinitelyCocompleteCategory 𝒟 - open CospanEmbed 𝒟 using (L; B₁; B∘L; R∘B; ≅-L-R) + open CospanEmbed 𝒟 using (L; B∘L; R∘B; ≅-L-R) module Square {F G : Functor 𝒞.U 𝒟.U} (F≃G : F ≃ G) where @@ -51,21 +52,21 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} {𝒟 : FinitelyCocompleteC open Cospan fg renaming (f₁ to f; f₂ to g) open 𝒟 using (_∘_) - squares⇒cospan : Cospans 𝒟 [ B₁ (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) ≈ B₁ (F.₁ f) (F.₁ g) ] + squares⇒cospan : Cospans 𝒟 [ cospan (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) ≈ cospan (F.₁ f) (F.₁ g) ] squares⇒cospan = record { ≅N = ≅.sym 𝒟.U FX≅GX - ; from∘f₁≈f₁′ = sym (switch-fromtoˡ FX≅GX (⇒.commute f)) - ; from∘f₂≈f₂′ = sym (switch-fromtoˡ FX≅GX (⇒.commute g)) + ; from∘f₁≈f₁ = sym (switch-fromtoˡ FX≅GX (⇒.commute f)) + ; from∘f₂≈f₂ = sym (switch-fromtoˡ FX≅GX (⇒.commute g)) } where open 𝒟.Equiv using (sym) - from : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇒.η Y) ∘ B₁ (F.₁ f) (F.₁ g) ] ≈ Cospans 𝒟 [ B₁ (G.₁ f) (G.₁ g) ∘ L.₁ (⇒.η X) ] ] + from : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇒.η Y) ∘ cospan (F.₁ f) (F.₁ g) ] ≈ Cospans 𝒟 [ cospan (G.₁ f) (G.₁ g) ∘ L.₁ (⇒.η X) ] ] from = sym (switch-tofromˡ FX≅GX′ (refl⟩∘⟨ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan)) where open Cospans.Equiv using (sym) - to : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇐.η Y) ∘ B₁ (G.₁ f) (G.₁ g) ] ≈ Cospans 𝒟 [ B₁ (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.η X) ] ] + to : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇐.η Y) ∘ cospan (G.₁ f) (G.₁ g) ] ≈ Cospans 𝒟 [ cospan (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.η X) ] ] to = switch-fromtoʳ FX≅GX′ (pullʳ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan) where open ⇒-Reasoning (Cospans 𝒟) using (pullʳ) diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda new file mode 100644 index 0000000..3df57ee --- /dev/null +++ b/Category/Monoidal/Instance/DecoratedCospans.agda @@ -0,0 +1,410 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module Category.Monoidal.Instance.DecoratedCospans + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Category.Monoidal.Properties as ⊗-Properties +import Categories.Category.Monoidal.Braided.Properties as σ-Properties + +open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category) +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Monoidal.Braided using (Braided) +open import Categories.Category.Monoidal.Core using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) +open import Categories.Functor.Hom using (Hom[_][_,-]) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Categories.Functor.Monoidal.Construction.Product using (⁂-SymmetricMonoidalFunctor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _ⓘˡ_; niHelper) +open import Categories.NaturalTransformation.Core using (NaturalTransformation; _∘ᵥ_; ntHelper) +open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≋_) +open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (module x+y; module y+x; [x+y]+z; x+[y+z]; assoc-≃) +open import Category.Monoidal.Instance.DecoratedCospans.Lift {o} {ℓ} {e} {o′} {ℓ′} {e′} using (module Square) +open import Cospan.Decorated 𝒞 F using (DecoratedCospan) +open import Data.Product.Base using (_,_) +open import Function.Base using () renaming (id to idf) +open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗) +open import Functor.Instance.DecoratedCospan.Embed 𝒞 F using (L; L-resp-⊗; B₁) + +open import Category.Monoidal.Instance.DecoratedCospans.Products 𝒞 F +open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal) +open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-naturalIsomorphism) + +module LiftUnitorˡ where + module F = SymmetricMonoidalFunctor F + open 𝒞 using (⊥; _+-; i₂; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) + open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐; λ⇒) + ≃₁ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (⊥ +-)) + ≃₁ = ntHelper record + { η = λ { X → record + { to = λ { f → 𝒟.U [ F.⊗-homo.η (⊥ , X) ∘ 𝒟.U [ 𝒟.⊗.₁ (𝒟.U [ F.₁ 𝒞.initial.! ∘ F.ε ] , f) ∘ ρ⇐ ] ] } + ; cong = λ { x → refl⟩∘⟨ refl⟩⊗⟨ x ⟩∘⟨refl } } + } + ; commute = ned + } + where + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + ned : {X Y : 𝒞.Obj} (f : X 𝒞.⇒ Y) {x : 𝒟.unit 𝒟.⇒ F.₀ X} + → F.⊗-homo.η (⊥ , Y) ∘ (F.₁ ¡ 𝒟.∘ F.ε) ⊗₁ (F.F₁ f ∘ x ∘ id) ∘ ρ⇐ + 𝒟.≈ F.₁ (𝒞.id +₁ f) ∘ (F.⊗-homo.η (𝒞.⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐) ∘ id + ned {X} {Y} f {x} = begin + F.⊗-homo.η (⊥ , Y) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ (F.₁ f ∘ x ∘ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl ⟩ + F.⊗-homo.η (⊥ , Y) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ (F.₁ f ∘ x) ∘ ρ⇐ ≈⟨ push-center split₂ˡ ⟩ + F.⊗-homo.η (⊥ , Y) ∘ id ⊗₁ F.₁ f ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐ ≈⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ + F.⊗-homo.η (⊥ , Y) ∘ F.₁ 𝒞.id ⊗₁ F.₁ f ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐ ≈⟨ extendʳ (F.⊗-homo.commute (𝒞.id , f)) ⟩ + F.₁ (𝒞.id +₁ f) ∘ F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐ ≈⟨ refl⟩∘⟨ identityʳ ⟨ + F.₁ (𝒞.id +₁ f) ∘ (F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ x ∘ ρ⇐) ∘ id ∎ + ≃₂ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F idF) + ≃₂ = ntHelper record + { η = λ { X → record { to = idf ; cong = idf } } + ; commute = λ { f → refl } + } + where + open 𝒟.Equiv + open NaturalIsomorphism using (F⇐G) + ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ ⊥+--id))) ∘ᵥ ≃₂ ≋ ≃₁ + ≃₂≋≃₁ {X} {f} = begin + F.₁ λ⇐ ∘ f ∘ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟨ + F.₁ λ⇐ ∘ f ∘ ρ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ coherence₃ ⟩∘⟨refl ⟨ + F.₁ λ⇐ ∘ f ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ 𝒟.unitorˡ-commute-from ⟨ + F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐ ≈⟨ pushˡ (introˡ F.identity) ⟩ + F.₁ 𝒞.id ∘ F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐ ≈⟨ F.F-resp-≈ (-+-.identity) ⟩∘⟨refl ⟨ + F.₁ (𝒞.id +₁ 𝒞.id) ∘ F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐ ≈⟨ F.F-resp-≈ (+₁-cong₂ (¡-unique 𝒞.id) 𝒞.Equiv.refl) ⟩∘⟨refl ⟨ + F.₁ (¡ +₁ 𝒞.id) ∘ F.₁ λ⇐ ∘ λ⇒ ∘ id ⊗₁ f ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨ + F.₁ (¡ +₁ 𝒞.id) ∘ F.⊗-homo.η (⊥ , X) ∘ F.ε ⊗₁ id ∘ id ⊗₁ f ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩ + F.₁ (¡ +₁ 𝒞.id) ∘ F.⊗-homo.η (⊥ , X) ∘ F.ε ⊗₁ f ∘ ρ⇐ ≈⟨ extendʳ (F.⊗-homo.commute (¡ , 𝒞.id)) ⟨ + F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ⊗₁ F.₁ 𝒞.id) ∘ F.ε ⊗₁ f ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ F.identity ⟩∘⟨refl ⟩ + F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ⊗₁ id) ∘ F.ε ⊗₁ f ∘ ρ⇐ ≈⟨ pull-center (sym split₁ˡ) ⟩ + F.⊗-homo.η (⊥ , X) ∘ (F.₁ ¡ ∘ F.ε) ⊗₁ f ∘ ρ⇐ ∎ + where + open Shorthands 𝒞.monoidal using (λ⇐) + open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (unitorˡ) + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ) + open ⊗-Reasoning 𝒟.monoidal + open ⊗-Properties 𝒟.monoidal using (coherence₃) + open ⇒-Reasoning 𝒟.U + module -+- = Functor -+- + module Unitorˡ = Square {𝒞} {𝒞} {𝒟} {𝒟} {F} {F} ⊥+--id ≃₁ ≃₂ ≃₂≋≃₁ +open LiftUnitorˡ using (module Unitorˡ) + +module LiftUnitorʳ where + module F = SymmetricMonoidalFunctor F + open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) + open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐) + ≃₁ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (-+ ⊥)) + ≃₁ = ntHelper record + { η = λ { X → record + { to = λ { f → 𝒟.U [ F.⊗-homo.η (X , ⊥) ∘ 𝒟.U [ 𝒟.⊗.₁ (f , 𝒟.U [ F.₁ 𝒞.initial.! ∘ F.ε ]) ∘ ρ⇐ ] ] } + ; cong = λ { x → refl⟩∘⟨ x ⟩⊗⟨refl ⟩∘⟨refl } } + } + ; commute = ned + } + where + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + ned : {X Y : 𝒞.Obj} (f : X 𝒞.⇒ Y) {x : 𝒟.unit 𝒟.⇒ F.₀ X} + → F.⊗-homo.η (Y , ⊥) ∘ (F.F₁ f ∘ x ∘ id) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ + 𝒟.≈ F.₁ (f +₁ 𝒞.id) ∘ (F.⊗-homo.η (X , ⊥) ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐) ∘ id + ned {X} {Y} f {x} = begin + F.⊗-homo.η (Y , ⊥) ∘ (F.₁ f ∘ x ∘ id) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F.⊗-homo.η (Y , ⊥) ∘ (F.₁ f ∘ x) ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ≈⟨ push-center split₁ˡ ⟩ + F.⊗-homo.η (Y , ⊥) ∘ F.₁ f ⊗₁ id ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ F.identity ⟩∘⟨refl ⟨ + F.⊗-homo.η (Y , ⊥) ∘ F.₁ f ⊗₁ F.₁ 𝒞.id ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ≈⟨ extendʳ (F.⊗-homo.commute (f , 𝒞.id)) ⟩ + F.₁ (f +₁ 𝒞.id) ∘ F.⊗-homo.η (X , ⊥) ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ identityʳ ⟨ + F.₁ (f +₁ 𝒞.id) ∘ (F.⊗-homo.η (X , ⊥) ∘ x ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐) ∘ id ∎ + ≃₂ : NaturalTransformation (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F idF) + ≃₂ = ntHelper record + { η = λ { X → record { to = idf ; cong = idf } } + ; commute = λ { f → refl } + } + where + open 𝒟.Equiv + open NaturalIsomorphism using (F⇐G) + ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ -+⊥-id))) ∘ᵥ ≃₂ ≋ ≃₁ + ≃₂≋≃₁ {X} {f} = begin + F.₁ i₁ ∘ f ∘ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟨ + F.₁ ρ⇐′ ∘ f ∘ ρ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ 𝒟.unitorʳ-commute-from ⟨ + F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐ ≈⟨ pushˡ (introˡ F.identity) ⟩ + F.₁ 𝒞.id ∘ F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐ ≈⟨ F.F-resp-≈ (-+-.identity) ⟩∘⟨refl ⟨ + F.₁ (𝒞.id +₁ 𝒞.id) ∘ F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐ ≈⟨ F.F-resp-≈ (+₁-cong₂ 𝒞.Equiv.refl (¡-unique 𝒞.id)) ⟩∘⟨refl ⟨ + F.₁ (𝒞.id +₁ ¡) ∘ F.₁ ρ⇐′ ∘ ρ⇒ ∘ f ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorʳ) F.unitaryʳ) ⟨ + F.₁ (𝒞.id +₁ ¡) ∘ F.⊗-homo.η (X , ⊥) ∘ id ⊗₁ F.ε ∘ f ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₂₁) ⟩ + F.₁ (𝒞.id +₁ ¡) ∘ F.⊗-homo.η (X , ⊥) ∘ f ⊗₁ F.ε ∘ ρ⇐ ≈⟨ extendʳ (F.⊗-homo.commute (𝒞.id , ¡)) ⟨ + F.⊗-homo.η (X , ⊥) ∘ (F.₁ 𝒞.id ⊗₁ F.₁ ¡) ∘ f ⊗₁ F.ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F.⊗-homo.η (X , ⊥) ∘ (id ⊗₁ F.₁ ¡) ∘ f ⊗₁ F.ε ∘ ρ⇐ ≈⟨ pull-center (sym split₂ˡ) ⟩ + F.⊗-homo.η (X , ⊥) ∘ f ⊗₁ (F.₁ ¡ ∘ F.ε) ∘ ρ⇐ ∎ + where + open Shorthands 𝒞.monoidal using () renaming (ρ⇐ to ρ⇐′) + open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (unitorʳ) + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + module -+- = Functor -+- + module Unitorʳ = Square {𝒞} {𝒞} {𝒟} {𝒟} {F} {F} -+⊥-id ≃₁ ≃₂ ≃₂≋≃₁ +open LiftUnitorʳ using (module Unitorʳ) + +module LiftAssociator where + module F = SymmetricMonoidalFunctor F + open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) + open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐) + ≃₁ : NaturalTransformation (Hom[ [𝒟×𝒟]×𝒟.U ][ [𝒟×𝒟]×𝒟.unit ,-] ∘F [F×F]×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F ([x+y]+z.F {𝒞})) + ≃₁ = ntHelper record + { η = λ { ((X , Y) , Z) → record + { to = λ { ((f , g) , h) → F.⊗-homo.η (X + Y , Z) ∘ ((F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h) ∘ ρ⇐ } + ; cong = λ { {(f , g) , h} {(f′ , g′) , h′} ((x , y) , z) → refl⟩∘⟨ (refl⟩∘⟨ x ⟩⊗⟨ y ⟩∘⟨refl) ⟩⊗⟨ z ⟩∘⟨refl } + } } + ; commute = λ { {(X , Y) , Z} {(X′ , Y′) , Z′} ((x , y) , z) {(f , g) , h} → commute x y z f g h } + } + where + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + commute + : {X Y Z X′ Y′ Z′ : 𝒞.Obj} + (x : 𝒞.U [ X , X′ ]) + (y : 𝒞.U [ Y , Y′ ]) + (z : 𝒞.U [ Z , Z′ ]) + (f : 𝒟.U [ 𝒟.unit , F.₀ X ]) + (g : 𝒟.U [ 𝒟.unit , F.₀ Y ]) + (h : 𝒟.U [ 𝒟.unit , F.₀ Z ]) + → F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.₁ y ∘ g ∘ id) ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐ + ≈ F.₁ ((x +₁ y) +₁ z) ∘ (F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐) ∘ id + commute {X} {Y} {Z} {X′} {Y′} {Z′} x y z f g h = begin + F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.₁ y ∘ g ∘ id) ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl ⟩ + F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ (F.₁ x ∘ f) ⊗₁ (F.₁ y ∘ g) ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ push-center ⊗-distrib-over-∘ ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.⊗-homo.η (X′ , Y′) ∘ F.₁ x ⊗₁ F.₁ y ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ extendʳ (F.⊗-homo.commute (x , y)) ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F.⊗-homo.η (X′ + Y′ , Z′) ∘ (F.₁ (x +₁ y) ∘ F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐ + ≈⟨ push-center ⊗-distrib-over-∘ ⟩ + F.⊗-homo.η (X′ + Y′ , Z′) ∘ F.₁ (x +₁ y) ⊗₁ F.₁ z ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ + ≈⟨ extendʳ (F.⊗-homo.commute (x +₁ y , z)) ⟩ + F.₁ ((x +₁ y) +₁ z) ∘ F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ identityʳ ⟨ + F.₁ ((x +₁ y) +₁ z) ∘ (F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐) ∘ id + ∎ + ≃₂ : NaturalTransformation (Hom[ [𝒟×𝒟]×𝒟.U ][ [𝒟×𝒟]×𝒟.unit ,-] ∘F [F×F]×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (x+[y+z].F {𝒞})) + ≃₂ = ntHelper record + { η = λ { ((X , Y) , Z) → record + { to = λ { ((f , g) , h) → F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐)) ∘ ρ⇐ } + ; cong = λ { {(f , g) , h} {(f′ , g′) , h′} ((x , y) , z) → refl⟩∘⟨ x ⟩⊗⟨ (refl⟩∘⟨ y ⟩⊗⟨ z ⟩∘⟨refl) ⟩∘⟨refl } + } } + ; commute = λ { {(X , Y) , Z} {(X′ , Y′) , Z′} ((x , y) , z) {(f , g) , h} → commute x y z f g h } + } + where + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + commute + : {X Y Z X′ Y′ Z′ : 𝒞.Obj} + (x : 𝒞.U [ X , X′ ]) + (y : 𝒞.U [ Y , Y′ ]) + (z : 𝒞.U [ Z , Z′ ]) + (f : 𝒟.U [ 𝒟.unit , F.₀ X ]) + (g : 𝒟.U [ 𝒟.unit , F.₀ Y ]) + (h : 𝒟.U [ 𝒟.unit , F.₀ Z ]) + → F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ (F.₁ y ∘ g ∘ id) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐) ∘ ρ⇐ + ≈ F.₁ (x +₁ (y +₁ z)) ∘ (F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐) ∘ id + commute {X} {Y} {Z} {X′} {Y′} {Z′} x y z f g h = begin + F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f ∘ id) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ (F.₁ y ∘ g ∘ id) ⊗₁ (F.₁ z ∘ h ∘ id) ∘ ρ⇐) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) ⟩∘⟨refl) ⟩∘⟨refl ⟩ + F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ (F.₁ y ∘ g) ⊗₁ (F.₁ z ∘ h) ∘ ρ⇐) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center ⊗-distrib-over-∘ ⟩∘⟨refl ⟩ + F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f) ⊗₁ (F.⊗-homo.η (Y′ , Z′) ∘ F.₁ y ⊗₁ F.₁ z ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ (F.⊗-homo.commute (y , z)) ⟩∘⟨refl ⟩ + F.⊗-homo.η (X′ , Y′ + Z′) ∘ (F.₁ x ∘ f) ⊗₁ (F.₁ (y +₁ z) ∘ F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ + ≈⟨ push-center ⊗-distrib-over-∘ ⟩ + F.⊗-homo.η (X′ , Y′ + Z′) ∘ F.₁ x ⊗₁ F.₁ (y +₁ z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ + ≈⟨ extendʳ (F.⊗-homo.commute (x , y +₁ z)) ⟩ + F.₁ (x +₁ (y +₁ z)) ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ + ≈⟨ refl⟩∘⟨ identityʳ ⟨ + F.₁ (x +₁ (y +₁ z)) ∘ (F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐) ∘ id + ∎ + open NaturalIsomorphism using (F⇐G) + ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ assoc-≃))) ∘ᵥ ≃₂ ≋ ≃₁ + ≃₂≋≃₁ {(X , Y) , Z} {(f , g) , h} = begin + F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ _) ∘ ρ⇐) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym-assoc ⟩∘⟨refl ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ ((F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟨ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-to ⟨ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (switch-tofromˡ α coherence-inv₁) ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g) ⊗₁ h ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym split₁ʳ) ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ (id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α′) F.associativity) ⟨ + F.⊗-homo.η (X + Y , Z) ∘ F.⊗-homo.η (X , Y) ⊗₁ id ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ (sym split₁ˡ) ⟩ + F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ (f ⊗₁ g) ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ∎ + where + open Shorthands 𝒞.monoidal using () renaming (α⇐ to α⇐′) + open Shorthands 𝒟.monoidal using (α⇒; λ⇐) + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; assoc-commute-from; unitorˡ-commute-to) renaming (unitorˡ to ƛ; associator to α) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using () renaming (associator to α′) + open ⊗-Properties 𝒟.monoidal using (coherence-inv₁; coherence-inv₃) + module Associator = Square {[𝒞×𝒞]×𝒞} {𝒞} {[𝒟×𝒟]×𝒟} {𝒟} {[F×F]×F} {F} {[x+y]+z.F {𝒞}} {x+[y+z].F {𝒞}} (assoc-≃ {𝒞}) ≃₁ ≃₂ ≃₂≋≃₁ +open LiftAssociator using (module Associator) + +module LiftBraiding where + module F = SymmetricMonoidalFunctor F + open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-) + open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐) + ≃₁ : NaturalTransformation (Hom[ 𝒟×𝒟.U ][ 𝒟×𝒟.unit ,-] ∘F F×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (x+y.F {𝒞})) + ≃₁ = ntHelper record + { η = λ { (X , Y) → record + { to = λ { (x , y) → F.⊗-homo.η (X , Y) ∘ x ⊗₁ y ∘ ρ⇐} + ; cong = λ { {x , y} {x′ , y′} (≈x , ≈y) → refl⟩∘⟨ ≈x ⟩⊗⟨ ≈y ⟩∘⟨refl } + } } + ; commute = λ { {X , Y} {X′ , Y′} (x , y) {f , g} → + (extendʳ + (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) + ○ refl⟩∘⟨ ⊗-distrib-over-∘ + ○ extendʳ (F.⊗-homo.commute (x , y)))) + ○ refl⟩∘⟨ extendˡ (sym identityʳ) } + } + where + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_; assoc) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + ≃₂ : NaturalTransformation (Hom[ 𝒟×𝒟.U ][ 𝒟×𝒟.unit ,-] ∘F F×F.F) (Hom[ 𝒟.U ][ 𝒟.unit ,-] ∘F F.F ∘F (y+x.F {𝒞})) + ≃₂ = ntHelper record + { η = λ { (X , Y) → record + { to = λ { (x , y) → F.⊗-homo.η (Y , X) ∘ y ⊗₁ x ∘ ρ⇐} + ; cong = λ { {x , y} {x′ , y′} (≈x , ≈y) → refl⟩∘⟨ ≈y ⟩⊗⟨ ≈x ⟩∘⟨refl } + } } + ; commute = λ { {X , Y} {X′ , Y′} (x , y) {f , g} → + (extendʳ + (refl⟩∘⟨ (refl⟩∘⟨ identityʳ) ⟩⊗⟨ (refl⟩∘⟨ identityʳ) + ○ refl⟩∘⟨ ⊗-distrib-over-∘ + ○ extendʳ (F.⊗-homo.commute (y , x)))) + ○ refl⟩∘⟨ extendˡ (sym identityʳ) } + } + where + open 𝒟.Equiv + open 𝒟 using (sym-assoc; _∘_; id; _⊗₁_; identityʳ; _≈_; assoc) + open ⊗-Reasoning 𝒟.monoidal + open ⇒-Reasoning 𝒟.U + open NaturalIsomorphism using (F⇐G) + open Symmetric 𝒞.symmetric using (braiding) + ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ F.F ⓘˡ braiding)) ∘ᵥ ≃₂ ≋ ≃₁ + ≃₂≋≃₁ {X , Y} {f , g} = + refl⟩∘⟨ (identityʳ ○ sym-assoc) + ○ extendʳ + (extendʳ F.braiding-compat + ○ refl⟩∘⟨ (𝒟.braiding.⇒.commute (g , f))) + ○ refl⟩∘⟨ pullʳ (sym (switch-tofromˡ 𝒟.braiding.FX≅GX braiding-coherence-inv) ○ coherence-inv₃) + where + open σ-Properties 𝒟.braided using (braiding-coherence-inv) + open 𝒟.Equiv + open 𝒟 using (sym-assoc; identityʳ) + open ⊗-Reasoning 𝒟.monoidal + open ⊗-Properties 𝒟.monoidal using (coherence-inv₃) + open ⇒-Reasoning 𝒟.U + module Braiding = Square {𝒞×𝒞} {𝒞} {𝒟×𝒟} {𝒟} {F×F} {F} {x+y.F {𝒞}} {y+x.F {𝒞}} braiding ≃₁ ≃₂ ≃₂≋≃₁ +open LiftBraiding using (module Braiding) + +CospansMonoidal : Monoidal DecoratedCospans +CospansMonoidal = record + { ⊗ = ⊗ + ; unit = ⊥ + ; unitorˡ = [ L ]-resp-≅ ⊥+A≅A + ; unitorʳ = [ L ]-resp-≅ A+⊥≅A + ; associator = [ L ]-resp-≅ (≅.sym +-assoc) + ; unitorˡ-commute-from = λ { {X} {Y} {f} → Unitorˡ.from f } + ; unitorˡ-commute-to = λ { {X} {Y} {f} → Unitorˡ.to f } + ; unitorʳ-commute-from = λ { {X} {Y} {f} → Unitorʳ.from f } + ; unitorʳ-commute-to = λ { {X} {Y} {f} → Unitorʳ.to f } + ; assoc-commute-from = λ { {X} {X′} {f} {Y} {Y′} {g} {Z} {Z′} {h} → Associator.from _ } + ; assoc-commute-to = λ { {X} {X′} {f} {Y} {Y′} {g} {Z} {Z′} {h} → Associator.to _ } + ; triangle = triangle + ; pentagon = pentagon + } + where + open Category DecoratedCospans using (id; module Equiv; module HomReasoning) + open Equiv + open HomReasoning + open 𝒞 using (⊥; Obj; U; +-assoc) + λ⇒ = Unitorˡ.FX≅GX′.from + ρ⇒ = Unitorʳ.FX≅GX′.from + α⇒ = Associator.FX≅GX′.from + open Morphism U using (module ≅) + open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent) + triangle : {X Y : Obj} → DecoratedCospans [ DecoratedCospans [ ⊗.₁ (id {X} , λ⇒) ∘ α⇒ ] ≈ ⊗.₁ (ρ⇒ , id {Y}) ] + triangle = sym L-resp-⊗ ⟩∘⟨refl ○ sym L.homomorphism ○ L.F-resp-≈ tri ○ L-resp-⊗ + pentagon + : {W X Y Z : Obj} + → DecoratedCospans + [ DecoratedCospans [ ⊗.₁ (id {W} , α⇒ {(X , Y) , Z}) ∘ DecoratedCospans [ α⇒ ∘ ⊗.₁ (α⇒ , id) ] ] + ≈ DecoratedCospans [ α⇒ ∘ α⇒ ] ] + pentagon = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym L.homomorphism ○ sym L.homomorphism ○ L.F-resp-≈ pent ○ L.homomorphism + +CospansBraided : Braided CospansMonoidal +CospansBraided = record + { braiding = niHelper record + { η = λ { (X , Y) → Braiding.FX≅GX′.from {X , Y} } + ; η⁻¹ = λ { (Y , X) → Braiding.FX≅GX′.to {Y , X} } + ; commute = λ { {X , Y} {X′ , Y′} (f , g) → Braiding.from (record { cospan = record { f₁ = f₁ f , f₁ g ; f₂ = f₂ f , f₂ g } ; decoration = decoration f , decoration g}) } + ; iso = λ { (X , Y) → Braiding.FX≅GX′.iso {X , Y} } + } + ; hexagon₁ = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym L.homomorphism ○ sym L.homomorphism ○ L-resp-≈ hex₁ ○ L.homomorphism ○ refl⟩∘⟨ L.homomorphism + ; hexagon₂ = sym L-resp-⊗ ⟩∘⟨refl ⟩∘⟨ sym L-resp-⊗ ○ sym L.homomorphism ⟩∘⟨refl ○ sym L.homomorphism ○ L-resp-≈ hex₂ ○ L.homomorphism ○ L.homomorphism ⟩∘⟨refl + } + where + open Symmetric 𝒞.symmetric renaming (hexagon₁ to hex₁; hexagon₂ to hex₂) + open DecoratedCospan + module Cospans = Category DecoratedCospans + open Cospans.Equiv + open Cospans.HomReasoning + open Functor L renaming (F-resp-≈ to L-resp-≈) + +CospansSymmetric : Symmetric CospansMonoidal +CospansSymmetric = record + { braided = CospansBraided + ; commutative = sym homomorphism ○ L-resp-≈ comm ○ identity + } + where + open Symmetric 𝒞.symmetric renaming (commutative to comm) + module Cospans = Category DecoratedCospans + open Cospans.Equiv + open Cospans.HomReasoning + open Functor L renaming (F-resp-≈ to L-resp-≈) diff --git a/Category/Monoidal/Instance/DecoratedCospans/Lift.agda b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda new file mode 100644 index 0000000..c75f0db --- /dev/null +++ b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda @@ -0,0 +1,114 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Monoidal.Instance.DecoratedCospans.Lift {o ℓ e o′ ℓ′ e′} where + +import Categories.Diagram.Pushout as PushoutDiagram +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Category.Diagram.Pushout as PushoutDiagram′ +import Functor.Instance.DecoratedCospan.Embed as CospanEmbed + +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]; module Definitions) +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Functor.Hom using (Hom[_][_,-]) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Categories.NaturalTransformation using (NaturalTransformation; _∘ᵥ_) +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_; _ⓘˡ_) +open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≋_) +open import Function.Bundles using (_⟨$⟩_) +open import Function.Construct.Composition using () renaming (function to _∘′_) +open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout) + +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Instance.Cospans using (Cospans) +open import Category.Instance.DecoratedCospans using (DecoratedCospans) +open import Category.Monoidal.Instance.Cospans.Lift {o} {ℓ} {e} using () renaming (module Square to Square′) +open import Cospan.Decorated using (DecoratedCospan) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module _ + {𝒞 : FinitelyCocompleteCategory o ℓ e} + {𝒟 : FinitelyCocompleteCategory o ℓ e} + {𝒥 : SymmetricMonoidalCategory o′ ℓ′ e′} + {𝒦 : SymmetricMonoidalCategory o′ ℓ′ e′} + {H : SymmetricMonoidalFunctor (smc 𝒞) 𝒥} + {I : SymmetricMonoidalFunctor (smc 𝒟) 𝒦} where + + module 𝒞 = FinitelyCocompleteCategory 𝒞 + module 𝒟 = FinitelyCocompleteCategory 𝒟 + module 𝒥 = SymmetricMonoidalCategory 𝒥 + module 𝒦 = SymmetricMonoidalCategory 𝒦 + module H = SymmetricMonoidalFunctor H + module I = SymmetricMonoidalFunctor I + + open CospanEmbed 𝒟 I using (L; B₁; B∘L; R∘B; ≅-L-R) + open NaturalIsomorphism using (F⇐G) + + module Square + {F G : Functor 𝒞.U 𝒟.U} + (F≃G : F ≃ G) + (⇒H≃I∘F : NaturalTransformation (Hom[ 𝒥.U ][ 𝒥.unit ,-] ∘F H.F) (Hom[ 𝒦.U ][ 𝒦.unit ,-] ∘F I.F ∘F F)) + (⇒H≃I∘G : NaturalTransformation (Hom[ 𝒥.U ][ 𝒥.unit ,-] ∘F H.F) (Hom[ 𝒦.U ][ 𝒦.unit ,-] ∘F I.F ∘F G)) + (≋ : (F⇐G (Hom[ 𝒦.U ][ 𝒦.unit ,-] ⓘˡ (I.F ⓘˡ F≃G))) ∘ᵥ ⇒H≃I∘G ≋ ⇒H≃I∘F) + where + + module F = Functor F + module G = Functor G + module ⇒H≃I∘F = NaturalTransformation ⇒H≃I∘F + module ⇒H≃I∘G = NaturalTransformation ⇒H≃I∘G + + open NaturalIsomorphism F≃G + + IF≃IG : I.F ∘F F ≃ I.F ∘F G + IF≃IG = I.F ⓘˡ F≃G + + open Morphism using (module ≅) renaming (_≅_ to _[_≅_]) + FX≅GX′ : ∀ {Z : 𝒞.Obj} → DecoratedCospans 𝒟 I [ F.₀ Z ≅ G.₀ Z ] + FX≅GX′ = [ L ]-resp-≅ FX≅GX + module FX≅GX {Z} = _[_≅_] (FX≅GX {Z}) + module FX≅GX′ {Z} = _[_≅_] (FX≅GX′ {Z}) + + module _ {X Y : 𝒞.Obj} (fg : DecoratedCospans 𝒞 H [ X , Y ]) where + + open DecoratedCospan fg renaming (f₁ to f; f₂ to g; decoration to s) + open 𝒟 using (_∘_) + + squares⇒cospan + : DecoratedCospans 𝒟 I + [ B₁ (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) (⇒H≃I∘G.η N ⟨$⟩ s) + ≈ B₁ (F.₁ f) (F.₁ g) (⇒H≃I∘F.η N ⟨$⟩ s) + ] + squares⇒cospan = record + { cospans-≈ = Square′.squares⇒cospan F≃G cospan + ; same-deco = refl⟩∘⟨ sym 𝒦.identityʳ ○ ≋ + } + where + open 𝒦.HomReasoning + open 𝒦.Equiv + + module Cospans = Category (DecoratedCospans 𝒟 I) + + from : DecoratedCospans 𝒟 I + [ DecoratedCospans 𝒟 I [ L.₁ (⇒.η Y) ∘ B₁ (F.₁ f) (F.₁ g) (⇒H≃I∘F.η N ⟨$⟩ s) ] + ≈ DecoratedCospans 𝒟 I [ B₁ (G.₁ f) (G.₁ g) (⇒H≃I∘G.η N ⟨$⟩ s) ∘ L.₁ (⇒.η X) ] + ] + from = sym (switch-tofromˡ FX≅GX′ (refl⟩∘⟨ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan)) + where + open Cospans.Equiv using (sym) + open ⇒-Reasoning (DecoratedCospans 𝒟 I) using (switch-tofromˡ) + open Cospans.HomReasoning using (refl⟩∘⟨_; _○_; _⟩∘⟨refl) + + to : DecoratedCospans 𝒟 I + [ DecoratedCospans 𝒟 I [ L.₁ (⇐.η Y) ∘ B₁ (G.₁ f) (G.₁ g) (⇒H≃I∘G.η N ⟨$⟩ s) ] ≈ DecoratedCospans 𝒟 I [ B₁ (F.₁ f) (F.₁ g) (⇒H≃I∘F.η N ⟨$⟩ s) ∘ L.₁ (⇐.η X) ] + ] + to = switch-fromtoʳ FX≅GX′ (pullʳ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan) + where + open ⇒-Reasoning (DecoratedCospans 𝒟 I) using (pullʳ; switch-fromtoʳ) + open Cospans.HomReasoning using (refl⟩∘⟨_; _○_; _⟩∘⟨refl) diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda new file mode 100644 index 0000000..f8ef542 --- /dev/null +++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module Category.Monoidal.Instance.DecoratedCospans.Products + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category) +open import Categories.Category.Core using (Category) +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) +open import Categories.Functor.Monoidal.Properties using (∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Construction.Product using (⁂-SymmetricMonoidalFunctor) +open import Categories.NaturalTransformation.Core using (NaturalTransformation; _∘ᵥ_; ntHelper) +open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian) +open import Category.Instance.Properties.SymMonCat {o′} {ℓ′} {e′} using () renaming (SymMonCat-Cartesian to SymMonCat-Cartesian′) +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC) +open import Category.Cartesian.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat-CC) +open import Data.Product.Base using (_,_) +open import Categories.Functor.Cartesian using (CartesianF) +open import Functor.Cartesian.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o} {ℓ} {e} using (Underlying) + +module SMC = CartesianF Underlying +module SymMonCat-CC = CartesianCategory SymMonCat-CC + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 + +module _ where + + open CartesianCategory FinitelyCocompletes-CC using (products) + open BinaryProducts products using (_×_) + + 𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e + 𝒞×𝒞 = 𝒞 × 𝒞 + + [𝒞×𝒞]×𝒞 : FinitelyCocompleteCategory o ℓ e + [𝒞×𝒞]×𝒞 = (𝒞 × 𝒞) × 𝒞 + +module _ where + + module _ where + + open Cartesian SymMonCat-Cartesian′ using (products) + open BinaryProducts products using (_×_; _⁂_) + + 𝒟×𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′ + 𝒟×𝒟 = 𝒟 × 𝒟 + module 𝒟×𝒟 = SymmetricMonoidalCategory 𝒟×𝒟 + + [𝒟×𝒟]×𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′ + [𝒟×𝒟]×𝒟 = (𝒟 × 𝒟) × 𝒟 + module [𝒟×𝒟]×𝒟 = SymmetricMonoidalCategory [𝒟×𝒟]×𝒟 + + module _ where + + open Cartesian SymMonCat-Cartesian using (products) + open BinaryProducts products using (_×_; _⁂_) + + smc𝒞×𝒞 : SymmetricMonoidalCategory o ℓ e + smc𝒞×𝒞 = smc 𝒞 × smc 𝒞 + + smc[𝒞×𝒞]×𝒞 : SymmetricMonoidalCategory o ℓ e + smc[𝒞×𝒞]×𝒞 = (smc 𝒞×𝒞) × smc 𝒞 + + F×F′ : SymmetricMonoidalFunctor smc𝒞×𝒞 𝒟×𝒟 + F×F′ = ⁂-SymmetricMonoidalFunctor {o′} {ℓ′} {e′} {o′} {ℓ′} {e′} {𝒟} {𝒟} {o} {ℓ} {e} {o} {ℓ} {e} {smc 𝒞} {smc 𝒞} F F + + F×F : SymmetricMonoidalFunctor (smc 𝒞×𝒞) 𝒟×𝒟 + F×F = ∘-SymmetricMonoidal F×F′ from + where + open Morphism SymMonCat-CC.U using (_≅_) + ≅ : smc 𝒞×𝒞 ≅ smc𝒞×𝒞 + ≅ = SMC.×-iso 𝒞 𝒞 + open _≅_ ≅ + module F×F = SymmetricMonoidalFunctor F×F + + [F×F]×F′ : SymmetricMonoidalFunctor smc[𝒞×𝒞]×𝒞 [𝒟×𝒟]×𝒟 + [F×F]×F′ = ⁂-SymmetricMonoidalFunctor {o′} {ℓ′} {e′} {o′} {ℓ′} {e′} {𝒟×𝒟} {𝒟} {o} {ℓ} {e} {o} {ℓ} {e} {smc 𝒞×𝒞} {smc 𝒞} F×F F + + [F×F]×F : SymmetricMonoidalFunctor (smc [𝒞×𝒞]×𝒞) [𝒟×𝒟]×𝒟 + [F×F]×F = ∘-SymmetricMonoidal [F×F]×F′ from + where + open Morphism SymMonCat-CC.U using (_≅_) + ≅ : smc [𝒞×𝒞]×𝒞 ≅ smc[𝒞×𝒞]×𝒞 + ≅ = SMC.×-iso 𝒞×𝒞 𝒞 + open _≅_ ≅ + module [F×F]×F = SymmetricMonoidalFunctor [F×F]×F diff --git a/Category/Monoidal/Instance/Nat.agda b/Category/Monoidal/Instance/Nat.agda new file mode 100644 index 0000000..24b30a6 --- /dev/null +++ b/Category/Monoidal/Instance/Nat.agda @@ -0,0 +1,71 @@ +{-# OPTIONS --without-K --safe #-} + +module Category.Monoidal.Instance.Nat where + +open import Level using (0ℓ) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Category.Instance.Nat using (Nat; Nat-Cartesian; Nat-Cocartesian; Natop) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) +open import Categories.Category.Duality using (coCartesian⇒Cocartesian; Cocartesian⇒coCartesian) + +import Categories.Category.Cartesian.SymmetricMonoidal as CartesianSymmetricMonoidal + +Natop-Cartesian : Cartesian Natop +Natop-Cartesian = Cocartesian⇒coCartesian Nat Nat-Cocartesian + +Natop-Cocartesian : Cocartesian Natop +Natop-Cocartesian = coCartesian⇒Cocartesian Natop Nat-Cartesian + +module Monoidal where + + open MonoidalCategory + open CartesianMonoidal using () renaming (monoidal to ×-monoidal) + open CocartesianMonoidal using (+-monoidal) + + Nat,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,+,0 .U = Nat + Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + + Nat,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,×,1 .U = Nat + Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + + Natop,+,0 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,+,0 .U = Natop + Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + + Natop,×,1 : MonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,×,1 .U = Natop + Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + +module Symmetric where + + open SymmetricMonoidalCategory + open CartesianMonoidal using () renaming (monoidal to ×-monoidal) + open CocartesianMonoidal using (+-monoidal) + open CartesianSymmetricMonoidal using () renaming (symmetric to ×-symmetric) + open CocartesianSymmetricMonoidal using (+-symmetric) + + Nat,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,+,0 .U = Nat + Nat,+,0 .monoidal = +-monoidal Nat Nat-Cocartesian + Nat,+,0 .symmetric = +-symmetric Nat Nat-Cocartesian + + Nat,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Nat,×,1 .U = Nat + Nat,×,1 .monoidal = ×-monoidal Nat-Cartesian + Nat,×,1 .symmetric = ×-symmetric Nat Nat-Cartesian + + Natop,+,0 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,+,0 .U = Natop + Natop,+,0 .monoidal = ×-monoidal Natop-Cartesian + Natop,+,0 .symmetric = ×-symmetric Natop Natop-Cartesian + + Natop,×,1 : SymmetricMonoidalCategory 0ℓ 0ℓ 0ℓ + Natop,×,1 .U = Natop + Natop,×,1 .monoidal = +-monoidal Natop Natop-Cocartesian + Natop,×,1 .symmetric = +-symmetric Natop Natop-Cocartesian + +open Symmetric public |