aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Category/Instance/Cospans.agda300
-rw-r--r--Category/Instance/DecoratedCospans.agda630
2 files changed, 511 insertions, 419 deletions
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index d54499d..ae6d359 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -7,16 +7,20 @@ 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)
+open import Relation.Binary using (IsEquivalence)
open import Categories.Morphism U using (_≅_; module ≅)
open import Categories.Morphism.Reasoning U
using
( switch-fromtoˡ
; glueTrianglesˡ
; pullˡ ; pullʳ
+ ; cancelˡ
)
open import Category.Diagram.Pushout U 
@@ -26,254 +30,296 @@ open import Category.Diagram.Pushout U 
; extend-i₁-iso ; extend-i₂-iso
)
-private
-
- variable
- A B C D X Y Z : Obj
- f g h : A ⇒ B
-
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
+
compose : Cospan A B → Cospan B C → Cospan A C
-compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ }
+compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
where
- module C₁ = Cospan c₁
- module C₂ = Cospan c₂
- module p = pushout C₁.f₂ C₂.f₁
+ open pushout g h
-id-Cospan : Cospan A A
-id-Cospan = record { f₁ = id ; f₂ = id }
+identity : Cospan A A
+identity = cospan id 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₂ }
+compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
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 f₂ g₁
+ module P₂ = pushout g₂ h₁
module P₃ = pushout P₁.i₂ P₂.i₁
-record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where
+record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
module C = Cospan C
- module C′ = Cospan C′
+ module D = Cospan D
field
- ≅N : C.N ≅ C′.N
+ ≅N : C.N ≅ D.N
open _≅_ ≅N public
module ≅N = _≅_ ≅N
field
- from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁
- from∘f₂≈f₂′ : from ∘ C.f₂ ≈ C′.f₂
+ from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
+ from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
+
+private
+ variable
+ f g h : Cospan A B
-same-refl : {C : Cospan A B} → Same C C
-same-refl = record
+≈-refl : f ≈ f
+≈-refl {f = cospan f₁ f₂} = record
{ ≅N = ≅.refl
- ; from∘f₁≈f₁′ = identityˡ
- ; from∘f₂≈f₂′ = identityˡ
+ ; 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ˡ
-same-sym : {C C′ : Cospan A B} → Same C C′ → Same C′ C
-same-sym C≅C′ = record
+≈-sym : f ≈ g → g ≈ f
+≈-sym f≈g = 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₂′)
+ ; from∘f₁≈f₁ = a
+ ; from∘f₂≈f₂ = b
}
- where
- open Same C≅C′
+ 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₂)
-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₂′
+≈-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
- module C≈C′ = Same C≈C′
- module C′≈C″ = Same C′≈C″
+ 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₂
-compose-idˡ : {C : Cospan A B} → Same (compose C id-Cospan) C
-compose-idˡ {_} {_} {C} = record
+≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
+≈-equiv = record
+ { refl = ≈-refl
+ ; sym = ≈-sym
+ ; trans = ≈-trans
+ }
+
+compose-idˡ : compose f identity ≈ f
+compose-idˡ {f = cospan {N} f₁ f₂} = record
{ ≅N = ≅P
- ; 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
+ 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ʳ : {C : Cospan A B} → Same (compose id-Cospan C) C
-compose-idʳ {_} {_} {C} = record
+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
+ 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² : Same {A} (compose id-Cospan id-Cospan) id-Cospan
+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₄′
+ ≅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
- : {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
+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..7e63f81 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -18,15 +18,17 @@ module Category.Instance.DecoratedCospans
module 𝒞 = FinitelyCocompleteCategory 𝒞
module 𝒟 = SymmetricMonoidalCategory 𝒟
+import Categories.Category.Monoidal.Utilities as ⊗-Util
import Category.Instance.Cospans 𝒞 as Cospans
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 (_⊔_)
@@ -67,64 +69,80 @@ compose c₁ c₂ = record
identity : DecoratedCospan A A
identity = record
- { cospan = Cospans.id-Cospan
+ { cospan = Cospans.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 Cospans.≈ C₂.cospan
- open Cospans.Same cospans-≈ public
- open 𝒟
- open Morphism U using (_≅_)
+ open Cospans._≈_ 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-≈ = Cospans.≈-refl
+ ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ
+ }
+
+ ≈-sym : f ≈ g → g ≈ f
+ ≈-sym f≈g = record
+ { cospans-≈ = Cospans.≈-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-≈ = Cospans.≈-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 +151,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 +174,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 +231,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 +252,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 +414,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 +430,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 +525,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 +538,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 +552,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₁ = Cospans._≈_ ≅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
}
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 21:51:44 +0000