aboutsummaryrefslogtreecommitdiff
path: root/Category
diff options
context:
space:
mode:
Diffstat (limited to 'Category')
-rw-r--r--Category/Construction/CMonoids.agda57
-rw-r--r--Category/Construction/CMonoids/Properties.agda74
-rw-r--r--Category/Construction/Monoids/Properties.agda108
-rw-r--r--Category/Diagram/Cospan.agda117
-rw-r--r--Category/Instance/Cospans.agda281
-rw-r--r--Category/Instance/DecoratedCospans.agda633
-rw-r--r--Category/Instance/FinitelyCocompletes.agda19
-rw-r--r--Category/Instance/One/Properties.agda24
-rw-r--r--Category/Instance/Setoids/SymmetricMonoidal.agda40
-rw-r--r--Category/Monoidal/Instance/Cospans.agda15
-rw-r--r--Category/Monoidal/Instance/Cospans/Lift.agda15
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans.agda17
-rw-r--r--Category/Monoidal/Instance/DecoratedCospans/Lift.agda2
-rw-r--r--Category/Monoidal/Instance/Nat.agda71
14 files changed, 959 insertions, 514 deletions
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 2766df2..9bee58e 100644
--- a/Category/Instance/FinitelyCocompletes.agda
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -1,29 +1,31 @@
{-# OPTIONS --without-K --safe #-}
-open import Level using (Level)
+
+open import Level using (Level; suc; _⊔_)
+
module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where
+import Category.Instance.One.Properties as OneProps
+
open import Categories.Category using (_[_,_])
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Helper using (categoryHelper)
-open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
open import Categories.Category.Core using (Category)
+open import Categories.Category.Helper using (categoryHelper)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.One using (One; One-⊤)
+open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat)
open import Categories.Diagram.Coequalizer using (IsCoequalizer)
open import Categories.Functor using (Functor) renaming (id to idF)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
open import Categories.Object.Coproduct using (IsCoproduct)
open import Categories.Object.Initial using (IsInitial)
open import Categories.Object.Product.Core using (Product)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×)
-open import Category.Instance.One.Properties using (One-FinitelyCocomplete)
open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′)
-open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
open import Function.Base using (id; flip)
-open import Level using (Level; suc; _⊔_)
+open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
FinitelyCocompletes = categoryHelper record
@@ -48,7 +50,7 @@ FinitelyCocompletes = categoryHelper record
One-FCC : FinitelyCocompleteCategory o ℓ e
One-FCC = record
{ U = One
- ; finCo = One-FinitelyCocomplete
+ ; finCo = OneProps.finitelyCocomplete
}
_×_
@@ -62,7 +64,6 @@ _×_ 𝒞 𝒟 = record
where
module 𝒞 = FinitelyCocompleteCategory 𝒞
module 𝒟 = FinitelyCocompleteCategory 𝒟
-{-# INJECTIVE_FOR_INFERENCE _×_ #-}
module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
diff --git a/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/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/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
index c570e54..3df57ee 100644
--- a/Category/Monoidal/Instance/DecoratedCospans.agda
+++ b/Category/Monoidal/Instance/DecoratedCospans.agda
@@ -55,7 +55,6 @@ open CocartesianMonoidal 𝒞.U 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+
open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-naturalIsomorphism)
module LiftUnitorˡ where
- module ⊗ = Functor ⊗
module F = SymmetricMonoidalFunctor F
open 𝒞 using (⊥; _+-; i₂; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐; λ⇒)
@@ -77,7 +76,7 @@ module LiftUnitorˡ where
𝒟.≈ 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 (sym split₂ˡ) ⟩
+ 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ʳ ⟨
@@ -117,7 +116,6 @@ module LiftUnitorˡ where
open LiftUnitorˡ using (module Unitorˡ)
module LiftUnitorʳ where
- module ⊗ = Functor ⊗
module F = SymmetricMonoidalFunctor F
open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐)
@@ -139,7 +137,7 @@ module LiftUnitorʳ where
𝒟.≈ 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 (sym split₁ˡ) ⟩
+ 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ʳ ⟨
@@ -177,7 +175,6 @@ module LiftUnitorʳ where
open LiftUnitorʳ using (module Unitorʳ)
module LiftAssociator where
- module ⊗ = Functor ⊗
module F = SymmetricMonoidalFunctor F
open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐)
@@ -208,11 +205,11 @@ module LiftAssociator where
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 (sym ⊗-distrib-over-∘) ⟩⊗⟨refl ⟩∘⟨refl ⟩
+ ≈⟨ 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 (sym ⊗-distrib-over-∘) ⟩
+ ≈⟨ 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 ∘ ρ⇐
@@ -246,11 +243,11 @@ module LiftAssociator where
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 (sym ⊗-distrib-over-∘) ⟩∘⟨refl ⟩
+ ≈⟨ 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 (sym ⊗-distrib-over-∘) ⟩
+ ≈⟨ 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 ∘ ρ⇐) ∘ ρ⇐
@@ -288,7 +285,6 @@ module LiftAssociator where
open LiftAssociator using (module Associator)
module LiftBraiding where
- module ⊗ = Functor ⊗
module F = SymmetricMonoidalFunctor F
open 𝒞 using (⊥; -+_; i₁; _+_; _+₁_; ¡; +₁-cong₂; ¡-unique; -+-)
open Shorthands 𝒟.monoidal using (ρ⇒; ρ⇐)
@@ -364,7 +360,6 @@ CospansMonoidal = record
; pentagon = pentagon
}
where
- module ⊗ = Functor ⊗
open Category DecoratedCospans using (id; module Equiv; module HomReasoning)
open Equiv
open HomReasoning
diff --git a/Category/Monoidal/Instance/DecoratedCospans/Lift.agda b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda
index 70795dd..c75f0db 100644
--- a/Category/Monoidal/Instance/DecoratedCospans/Lift.agda
+++ b/Category/Monoidal/Instance/DecoratedCospans/Lift.agda
@@ -23,7 +23,7 @@ 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; Cospan)
+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)
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 08:14:23 +0000