diff options
Diffstat (limited to 'Category/Instance')
| -rw-r--r-- | Category/Instance/Cospans.agda | 281 | ||||
| -rw-r--r-- | Category/Instance/DecoratedCospans.agda | 633 | ||||
| -rw-r--r-- | Category/Instance/FinitelyCocompletes.agda | 18 | ||||
| -rw-r--r-- | Category/Instance/One/Properties.agda | 24 | ||||
| -rw-r--r-- | Category/Instance/Properties/FinitelyCocompletes.agda | 210 | ||||
| -rw-r--r-- | Category/Instance/Properties/SymMonCat.agda | 166 | ||||
| -rw-r--r-- | Category/Instance/Setoids/SymmetricMonoidal.agda | 40 | ||||
| -rw-r--r-- | Category/Instance/SymMonCat.agda | 74 |
8 files changed, 750 insertions, 696 deletions
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda index d54499d..d17a58d 100644 --- a/Category/Instance/Cospans.agda +++ b/Category/Instance/Cospans.agda @@ -7,7 +7,9 @@ open import Level using (_⊔_) module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where -open FinitelyCocompleteCategory 𝒞 +module 𝒞 = FinitelyCocompleteCategory 𝒞 +open 𝒞 using (U; pushout) +open Category U hiding (_≈_) open import Categories.Diagram.Pushout U using (Pushout) open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso) @@ -15,8 +17,8 @@ open import Categories.Morphism U using (_≅_; module ≅) open import Categories.Morphism.Reasoning U using ( switch-fromtoˡ - ; glueTrianglesˡ ; pullˡ ; pullʳ + ; cancelˡ ) open import Category.Diagram.Pushout U @@ -26,254 +28,213 @@ open import Category.Diagram.Pushout U ; extend-i₁-iso ; extend-i₂-iso ) -private +open import Category.Diagram.Cospan 𝒞 using (Cospan; compose; compose-3; identity; _≈_; cospan; ≈-trans; ≈-sym; ≈-equiv) +private variable - A B C D X Y Z : Obj - f g h : A ⇒ B - -record Cospan (A B : Obj) : Set (o ⊔ ℓ) where - - field - {N} : Obj - f₁ : A ⇒ N - f₂ : B ⇒ N - -compose : Cospan A B → Cospan B C → Cospan A C -compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ } - where - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module p = pushout C₁.f₂ C₂.f₁ - -id-Cospan : Cospan A A -id-Cospan = record { f₁ = id ; f₂ = id } - -compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D -compose-3 c₁ c₂ c₃ = record { f₁ = P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ ; f₂ = P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ } - where - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module C₃ = Cospan c₃ - module P₁ = pushout C₁.f₂ C₂.f₁ - module P₂ = pushout C₂.f₂ C₃.f₁ - module P₃ = pushout P₁.i₂ P₂.i₁ + A B C D : Obj -record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where - - module C = Cospan C - module C′ = Cospan C′ - - field - ≅N : C.N ≅ C′.N - - open _≅_ ≅N public - module ≅N = _≅_ ≅N - - field - from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁ - from∘f₂≈f₂′ : from ∘ C.f₂ ≈ C′.f₂ - -same-refl : {C : Cospan A B} → Same C C -same-refl = record - { ≅N = ≅.refl - ; from∘f₁≈f₁′ = identityˡ - ; from∘f₂≈f₂′ = identityˡ - } - -same-sym : {C C′ : Cospan A B} → Same C C′ → Same C′ C -same-sym C≅C′ = record - { ≅N = ≅.sym ≅N - ; from∘f₁≈f₁′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁′) - ; from∘f₂≈f₂′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂′) - } - where - open Same C≅C′ - -same-trans : {C C′ C″ : Cospan A B} → Same C C′ → Same C′ C″ → Same C C″ -same-trans C≈C′ C′≈C″ = record - { ≅N = ≅.trans C≈C′.≅N C′≈C″.≅N - ; from∘f₁≈f₁′ = glueTrianglesˡ C′≈C″.from∘f₁≈f₁′ C≈C′.from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = glueTrianglesˡ C′≈C″.from∘f₂≈f₂′ C≈C′.from∘f₂≈f₂′ - } - where - module C≈C′ = Same C≈C′ - module C′≈C″ = Same C′≈C″ +private + variable + f g h : Cospan A B -compose-idˡ : {C : Cospan A B} → Same (compose C id-Cospan) C -compose-idˡ {_} {_} {C} = record +compose-idˡ : compose f identity ≈ f +compose-idˡ {f = cospan {N} f₁ f₂} = record { ≅N = ≅P - ; from∘f₁≈f₁′ = begin - ≅P.from ∘ P.i₁ ∘ C.f₁ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₁) ∘ C.f₁ ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩ - id ∘ C.f₁ ≈⟨ identityˡ ⟩ - C.f₁ ∎ - ; from∘f₂≈f₂′ = begin - ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ - ≅P.from ∘ P.i₂ ≈⟨ P.universal∘i₂≈h₂ ⟩ - C.f₂ ∎ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C = Cospan C - P = pushout C.f₂ id + P P′ : Pushout f₂ id + P = pushout f₂ id + P′ = pushout-f-id {f = f₂} module P = Pushout P - P′ = pushout-f-id {f = C.f₂} + ≅P : P.Q ≅ N ≅P = up-to-iso P P′ module ≅P = _≅_ ≅P - -compose-idʳ : {C : Cospan A B} → Same (compose id-Cospan C) C -compose-idʳ {_} {_} {C} = record + abstract + from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ f₁ 𝒞.≈ f₁ + from∘f₁≈f₁ = begin + ≅P.from ∘ P.i₁ ∘ f₁ ≈⟨ cancelˡ P.universal∘i₁≈h₁ ⟩ + f₁ ∎ + from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ id 𝒞.≈ f₂ + from∘f₂≈f₂ = begin + ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + ≅P.from ∘ P.i₂ ≈⟨ P.universal∘i₂≈h₂ ⟩ + f₂ ∎ + +compose-idʳ : compose identity f ≈ f +compose-idʳ {f = cospan {N} f₁ f₂} = record { ≅N = ≅P - ; from∘f₁≈f₁′ = begin - ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ - ≅P.from ∘ P.i₁ ≈⟨ P.universal∘i₁≈h₁ ⟩ - C.f₁ ∎ - ; from∘f₂≈f₂′ = begin - ≅P.from ∘ P.i₂ ∘ C.f₂ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₂) ∘ C.f₂ ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩ - id ∘ C.f₂ ≈⟨ identityˡ ⟩ - C.f₂ ∎ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C = Cospan C - P = pushout id C.f₁ + P P′ : Pushout id f₁ + P = pushout id f₁ module P = Pushout P - P′ = pushout-id-g {g = C.f₁} + P′ = pushout-id-g {g = f₁} + ≅P : P.Q ≅ N ≅P = up-to-iso P P′ module ≅P = _≅_ ≅P - -compose-id² : Same {A} (compose id-Cospan id-Cospan) id-Cospan + abstract + from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ id 𝒞.≈ f₁ + from∘f₁≈f₁ = begin + ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + ≅P.from ∘ P.i₁ ≈⟨ P.universal∘i₁≈h₁ ⟩ + f₁ ∎ + from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ f₂ 𝒞.≈ f₂ + from∘f₂≈f₂ = begin + ≅P.from ∘ P.i₂ ∘ f₂ ≈⟨ cancelˡ P.universal∘i₂≈h₂ ⟩ + f₂ ∎ + +compose-id² : compose identity identity ≈ identity {A} compose-id² = compose-idˡ -compose-3-right - : {c₁ : Cospan A B} - {c₂ : Cospan B C} - {c₃ : Cospan C D} - → Same (compose c₁ (compose c₂ c₃)) (compose-3 c₁ c₂ c₃) -compose-3-right {_} {_} {_} {_} {c₁} {c₂} {c₃} = record - { ≅N = up-to-iso P₄′ P₄ - ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc - ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl +compose-3-right : compose f (compose g h) ≈ compose-3 f g h +compose-3-right {f = f} {g = g} {h = h} = record + { ≅N = ≅N + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module C₃ = Cospan c₃ + module C₁ = Cospan f + module C₂ = Cospan g + module C₃ = Cospan h + P₁ : Pushout C₁.f₂ C₂.f₁ P₁ = pushout C₁.f₂ C₂.f₁ + P₂ : Pushout C₂.f₂ C₃.f₁ P₂ = pushout C₂.f₂ C₃.f₁ module P₁ = Pushout P₁ module P₂ = Pushout P₂ + P₃ : Pushout P₁.i₂ P₂.i₁ P₃ = pushout P₁.i₂ P₂.i₁ module P₃ = Pushout P₃ + P₄ P₄′ : Pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁) P₄ = glue-i₂ P₁ P₃ - module P₄ = Pushout P₄ P₄′ = pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁) + module P₄ = Pushout P₄ module P₄′ = Pushout P₄′ - -compose-3-left - : {c₁ : Cospan A B} - {c₂ : Cospan B C} - {c₃ : Cospan C D} - → Same (compose (compose c₁ c₂) c₃) (compose-3 c₁ c₂ c₃) -compose-3-left {_} {_} {_} {_} {c₁} {c₂} {c₃} = record + ≅N : P₄′.Q ≅ P₄.Q + ≅N = up-to-iso P₄′ P₄ + module ≅N = _≅_ ≅N + abstract + from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ C₁.f₁ 𝒞.≈ P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ + from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc + from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ P₂.i₂ ∘ C₃.f₂ 𝒞.≈ P₄.i₂ ∘ P₂.i₂ ∘ C₃.f₂ + from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl + +compose-3-left : compose (compose f g) h ≈ compose-3 f g h +compose-3-left {f = f} {g = g} {h = h} = record { ≅N = up-to-iso P₄′ P₄ - ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl - ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open HomReasoning - module C₁ = Cospan c₁ - module C₂ = Cospan c₂ - module C₃ = Cospan c₃ + module C₁ = Cospan f + module C₂ = Cospan g + module C₃ = Cospan h + P₁ : Pushout C₁.f₂ C₂.f₁ P₁ = pushout C₁.f₂ C₂.f₁ + P₂ : Pushout C₂.f₂ C₃.f₁ P₂ = pushout C₂.f₂ C₃.f₁ module P₁ = Pushout P₁ module P₂ = Pushout P₂ + P₃ : Pushout P₁.i₂ P₂.i₁ P₃ = pushout P₁.i₂ P₂.i₁ module P₃ = Pushout P₃ + P₄ P₄′ : Pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁ P₄ = glue-i₁ P₂ P₃ - module P₄ = Pushout P₄ P₄′ = pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁ + module P₄ = Pushout P₄ module P₄′ = Pushout P₄′ + ≅N : P₄′.Q ≅ P₄.Q + ≅N = up-to-iso P₄′ P₄ + module ≅N = _≅_ ≅N + abstract + from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ P₁.i₁ ∘ C₁.f₁ 𝒞.≈ P₄.i₁ ∘ P₁.i₁ ∘ C₁.f₁ + from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl + from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ C₃.f₂ 𝒞.≈ P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ + from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc compose-assoc : {c₁ : Cospan A B} {c₂ : Cospan B C} {c₃ : Cospan C D} - → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃) -compose-assoc = same-trans compose-3-right (same-sym compose-3-left) + → compose c₁ (compose c₂ c₃) ≈ (compose (compose c₁ c₂) c₃) +compose-assoc = ≈-trans compose-3-right (≈-sym compose-3-left) compose-sym-assoc : {c₁ : Cospan A B} {c₂ : Cospan B C} {c₃ : Cospan C D} - → Same (compose (compose c₁ c₂) c₃) (compose c₁ (compose c₂ c₃)) -compose-sym-assoc = same-trans compose-3-left (same-sym compose-3-right) + → compose (compose c₁ c₂) c₃ ≈ compose c₁ (compose c₂ c₃) +compose-sym-assoc = ≈-trans compose-3-left (≈-sym compose-3-right) compose-equiv : {c₂ c₂′ : Cospan B C} {c₁ c₁′ : Cospan A B} - → Same c₂ c₂′ - → Same c₁ c₁′ - → Same (compose c₁ c₂) (compose c₁′ c₂′) + → c₂ ≈ c₂′ + → c₁ ≈ c₁′ + → compose c₁ c₂ ≈ compose c₁′ c₂′ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≈C₂ ≈C₁ = record - { ≅N = up-to-iso P P″ - ; from∘f₁≈f₁′ = begin - ≅P.from ∘ P.i₁ ∘ C₁.f₁ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₁) ∘ C₁.f₁ ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩ - (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁ ≈⟨ assoc ⟩ - P′.i₁ ∘ ≈C₁.from ∘ C₁.f₁ ≈⟨ refl⟩∘⟨ ≈C₁.from∘f₁≈f₁′ ⟩ - P′.i₁ ∘ C₁′.f₁ ∎ - ; from∘f₂≈f₂′ = begin - ≅P.from ∘ P.i₂ ∘ C₂.f₂ ≈⟨ assoc ⟨ - (≅P.from ∘ P.i₂) ∘ C₂.f₂ ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩ - (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂ ≈⟨ assoc ⟩ - P′.i₂ ∘ ≈C₂.from ∘ C₂.f₂ ≈⟨ refl⟩∘⟨ ≈C₂.from∘f₂≈f₂′ ⟩ - P′.i₂ ∘ C₂′.f₂ ∎ + { ≅N = ≅P + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where module C₁ = Cospan c₁ module C₁′ = Cospan c₁′ module C₂ = Cospan c₂ module C₂′ = Cospan c₂′ + P : Pushout C₁.f₂ C₂.f₁ P = pushout C₁.f₂ C₂.f₁ + P′ : Pushout C₁′.f₂ C₂′.f₁ P′ = pushout C₁′.f₂ C₂′.f₁ - module ≈C₁ = Same ≈C₁ - module ≈C₂ = Same ≈C₂ + module ≈C₁ = _≈_ ≈C₁ + module ≈C₂ = _≈_ ≈C₂ P′′ : Pushout (≈C₁.to ∘ C₁′.f₂) (≈C₂.to ∘ C₂′.f₁) P′′ = extend-i₂-iso (extend-i₁-iso P′ (≅.sym ≈C₁.≅N)) (≅.sym ≈C₂.≅N) P″ : Pushout C₁.f₂ C₂.f₁ P″ = pushout-resp-≈ P′′ - (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂′)) - (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁′)) + (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂)) + (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁)) module P = Pushout P module P′ = Pushout P′ ≅P : P.Q ≅ P′.Q ≅P = up-to-iso P P″ module ≅P = _≅_ ≅P open HomReasoning + abstract + from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ C₁.f₁ 𝒞.≈ P′.i₁ ∘ C₁′.f₁ + from∘f₁≈f₁ = begin + ≅P.from ∘ P.i₁ ∘ C₁.f₁ ≈⟨ pullˡ P.universal∘i₁≈h₁ ⟩ + (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁ ≈⟨ pullʳ ≈C₁.from∘f₁≈f₁ ⟩ + P′.i₁ ∘ C₁′.f₁ ∎ + from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ C₂.f₂ 𝒞.≈ P′.i₂ ∘ C₂′.f₂ + from∘f₂≈f₂ = begin + ≅P.from ∘ P.i₂ ∘ C₂.f₂ ≈⟨ pullˡ P.universal∘i₂≈h₂ ⟩ + (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂ ≈⟨ pullʳ ≈C₂.from∘f₂≈f₂ ⟩ + P′.i₂ ∘ C₂′.f₂ ∎ Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e) Cospans = record { Obj = Obj ; _⇒_ = Cospan - ; _≈_ = Same - ; id = id-Cospan + ; _≈_ = _≈_ + ; id = identity ; _∘_ = flip compose ; assoc = compose-assoc ; sym-assoc = compose-sym-assoc ; identityˡ = compose-idˡ ; identityʳ = compose-idʳ ; identity² = compose-id² - ; equiv = record - { refl = same-refl - ; sym = same-sym - ; trans = same-trans - } + ; equiv = ≈-equiv ; ∘-resp-≈ = compose-equiv } diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda index c0c62c7..b527265 100644 --- a/Category/Instance/DecoratedCospans.agda +++ b/Category/Instance/DecoratedCospans.agda @@ -18,15 +18,18 @@ module Category.Instance.DecoratedCospans module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = SymmetricMonoidalCategory 𝒟 +import Categories.Category.Monoidal.Utilities as ⊗-Util import Category.Instance.Cospans 𝒞 as Cospans +import Category.Diagram.Cospan 𝒞 as Cospan open import Categories.Category using (Category; _[_∘_]) open import Categories.Category.Cocartesian using (module CocartesianMonoidal) open import Categories.Diagram.Pushout using (Pushout) open import Categories.Diagram.Pushout.Properties 𝒞.U using (up-to-iso) -open import Categories.Functor.Properties using ([_]-resp-≅) +open import Categories.Functor.Properties using ([_]-resp-≅; [_]-resp-square) open import Categories.Morphism.Reasoning using (switch-fromtoˡ; glueTrianglesˡ) open import Cospan.Decorated 𝒞 F using (DecoratedCospan) +open import Relation.Binary using (IsEquivalence) open import Data.Product using (_,_) open import Function using (flip) open import Level using (_⊔_) @@ -50,7 +53,7 @@ private compose : DecoratedCospan A B → DecoratedCospan B C → DecoratedCospan A C compose c₁ c₂ = record - { cospan = Cospans.compose C₁.cospan C₂.cospan + { cospan = Cospan.compose C₁.cospan C₂.cospan ; decoration = F₁ [ i₁ , i₂ ] ∘ φ ∘ s⊗t } where @@ -67,64 +70,80 @@ compose c₁ c₂ = record identity : DecoratedCospan A A identity = record - { cospan = Cospans.id-Cospan + { cospan = Cospan.identity ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ] } -record Same (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where +record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where - module C₁ = DecoratedCospan C₁ - module C₂ = DecoratedCospan C₂ + private + module C₁ = DecoratedCospan C₁ + module C₂ = DecoratedCospan C₂ field - cospans-≈ : Cospans.Same C₁.cospan C₂.cospan + cospans-≈ : C₁.cospan Cospan.≈ C₂.cospan - open Cospans.Same cospans-≈ public - open 𝒟 - open Morphism U using (_≅_) + open Cospan._≈_ cospans-≈ public + open Morphism 𝒟.U using (_≅_) field - same-deco : F₁ ≅N.from ∘ C₁.decoration ≈ C₂.decoration + same-deco : F₁ ≅N.from 𝒟.∘ C₁.decoration 𝒟.≈ C₂.decoration ≅F[N] : F₀ C₁.N ≅ F₀ C₂.N ≅F[N] = [ F′ ]-resp-≅ ≅N -same-refl : {C : DecoratedCospan A B} → Same C C -same-refl = record - { cospans-≈ = Cospans.same-refl - ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ - } - where - open 𝒟 - open HomReasoning +infix 4 _≈_ -same-sym : {C C′ : DecoratedCospan A B} → Same C C′ → Same C′ C -same-sym C≅C′ = record - { cospans-≈ = Cospans.same-sym cospans-≈ - ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) - } - where - open Same C≅C′ - open 𝒟.Equiv - -same-trans : {C C′ C″ : DecoratedCospan A B} → Same C C′ → Same C′ C″ → Same C C″ -same-trans C≈C′ C′≈C″ = record - { cospans-≈ = Cospans.same-trans C≈C′.cospans-≈ C′≈C″.cospans-≈ - ; same-deco = - homomorphism ⟩∘⟨refl ○ - glueTrianglesˡ 𝒟.U C′≈C″.same-deco C≈C′.same-deco - } - where - module C≈C′ = Same C≈C′ - module C′≈C″ = Same C′≈C″ - open 𝒟.HomReasoning +module _ where + + open 𝒟.HomReasoning + open 𝒟.Equiv + open 𝒟 using (identityˡ) + + private + variable + f g h : DecoratedCospan A B + + abstract + + ≈-refl : f ≈ f + ≈-refl = record + { cospans-≈ = Cospan.≈-refl + ; same-deco = F-identity ⟩∘⟨refl ○ identityˡ + } + + ≈-sym : f ≈ g → g ≈ f + ≈-sym f≈g = record + { cospans-≈ = Cospan.≈-sym cospans-≈ + ; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco) + } + where + open _≈_ f≈g + + ≈-trans : f ≈ g → g ≈ h → f ≈ h + ≈-trans f≈g g≈h = record + { cospans-≈ = Cospan.≈-trans f≈g.cospans-≈ g≈h.cospans-≈ + ; same-deco = + homomorphism ⟩∘⟨refl ○ + glueTrianglesˡ 𝒟.U g≈h.same-deco f≈g.same-deco + } + where + module f≈g = _≈_ f≈g + module g≈h = _≈_ g≈h + + ≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B}) + ≈-equiv = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } compose-assoc : {c₁ : DecoratedCospan A B} {c₂ : DecoratedCospan B C} {c₃ : DecoratedCospan C D} - → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃) -compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record + → compose c₁ (compose c₂ c₃) ≈ compose (compose c₁ c₂) c₃ +compose-assoc {A} {B} {C} {D} {c₁} {c₂} {c₃} = record { cospans-≈ = Cospans.compose-assoc ; same-deco = deco-assoc } @@ -133,14 +152,19 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record module C₂ = DecoratedCospan c₂ module C₃ = DecoratedCospan c₃ open 𝒞 using (+-assoc; pushout; [_,_]; _+₁_; _+_) renaming (_∘_ to _∘′_; id to id′) + p₁ : Pushout 𝒞.U C₁.f₂ C₂.f₁ p₁ = pushout C₁.f₂ C₂.f₁ + p₂ : Pushout 𝒞.U C₂.f₂ C₃.f₁ p₂ = pushout C₂.f₂ C₃.f₁ module P₁ = Pushout p₁ module P₂ = Pushout p₂ + p₃ : Pushout 𝒞.U P₁.i₂ P₂.i₁ p₃ = pushout P₁.i₂ P₂.i₁ + p₁₃ p₄ : Pushout 𝒞.U C₁.f₂ (P₂.i₁ ∘′ C₂.f₁) p₁₃ = glue-i₂ p₁ p₃ - p₂₃ = glue-i₁ p₂ p₃ p₄ = pushout C₁.f₂ (P₂.i₁ ∘′ C₂.f₁) + p₂₃ p₅ : Pushout 𝒞.U (P₁.i₂ ∘′ C₂.f₂) C₃.f₁ + p₂₃ = glue-i₁ p₂ p₃ p₅ = pushout (P₁.i₂ ∘′ C₂.f₂) C₃.f₁ module P₃ = Pushout p₃ module P₄ = Pushout p₄ @@ -151,36 +175,50 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record module P₄≅P₁₃ = _≅_ (up-to-iso p₄ p₁₃) module P₅≅P₂₃ = _≅_ (up-to-iso p₅ p₂₃) + N M P Q R : 𝒞.Obj N = C₁.N M = C₂.N P = C₃.N Q = P₁.Q R = P₂.Q - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute - - a = C₁.f₂ - b = C₂.f₁ - c = C₂.f₂ - d = C₂.f₁ + f : N 𝒞.⇒ Q f = P₁.i₁ + + g : M 𝒞.⇒ Q g = P₁.i₂ + + h : M 𝒞.⇒ R h = P₂.i₁ + + i : P 𝒞.⇒ R i = P₂.i₂ + j : Q 𝒞.⇒ P₃.Q j = P₃.i₁ + + k : R 𝒞.⇒ P₃.Q k = P₃.i₂ + w : N 𝒞.⇒ P₄.Q w = P₄.i₁ + + x : R 𝒞.⇒ P₄.Q x = P₄.i₂ + + y : Q 𝒞.⇒ P₅.Q y = P₅.i₁ + + z : P 𝒞.⇒ P₅.Q z = P₅.i₂ + l : P₂₃.Q 𝒞.⇒ P₅.Q l = P₅≅P₂₃.to + + m : P₄.Q 𝒞.⇒ P₁₃.Q m = P₄≅P₁₃.from - module +-assoc = _≅_ +-assoc + module +-assoc {m} {n} {o} = _≅_ (+-assoc {m} {n} {o}) module _ where @@ -194,23 +232,19 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record open 𝒞.HomReasoning open 𝒞.Equiv - copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from + copairings : ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) 𝒞.≈ [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from copairings = begin - ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ pushˡ assoc ⟩ - l ∘ (m ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ refl⟩∘⟨ ∘[] ⟩∘⟨refl ⟩ - l ∘ [ m ∘ w , m ∘ x ] ∘ (id +₁ [ h , i ]) ≈⟨ refl⟩∘⟨ []-cong₂ (P₄.universal∘i₁≈h₁) (P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ - l ∘ [ j ∘ f , k ] ∘ (id +₁ [ h , i ]) ≈⟨ pullˡ ∘[] ⟩ - [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩ - [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []∘+₁ ⟩ - [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ] ≈⟨ []-cong₂ identityʳ (pullʳ ∘[]) ⟩ - [ y ∘ f , l ∘ [ k ∘ h , k ∘ i ] ] ≈⟨ []-congˡ (refl⟩∘⟨ []-congʳ P₃.commute) ⟨ - [ y ∘ f , l ∘ [ j ∘ g , k ∘ i ] ] ≈⟨ []-congˡ ∘[] ⟩ - [ y ∘ f , [ l ∘ j ∘ g , l ∘ k ∘ i ] ] ≈⟨ []-congˡ ([]-congˡ P₂₃.universal∘i₂≈h₂) ⟩ - [ y ∘ f , [ l ∘ j ∘ g , z ] ] ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩ - [ y ∘ f , [ y ∘ g , z ] ] ≈⟨ []∘assocˡ ⟨ - [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨ - [ y ∘ [ f , g ] , z ∘ id ] ∘ +-assoc.from ≈⟨ pullˡ []∘+₁ ⟨ - [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from ∎ + ((l ∘ m) ∘ [ w , x ]) ∘ (id +₁ [ h , i ]) ≈⟨ ∘[] ⟩∘⟨refl ⟩ + [(l ∘ m) ∘ w , (l ∘ m) ∘ x ] ∘ (id +₁ [ h , i ]) ≈⟨ []-cong₂ (pullʳ P₄.universal∘i₁≈h₁) (pullʳ P₄.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ + [ l ∘ j ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []-congʳ (pullˡ P₂₃.universal∘i₁≈h₁) ⟩∘⟨refl ⟩ + [ y ∘ f , l ∘ k ] ∘ (id +₁ [ h , i ]) ≈⟨ []∘+₁ ⟩ + [ (y ∘ f) ∘ id , (l ∘ k) ∘ [ h , i ] ] ≈⟨ []-cong₂ identityʳ ∘[] ⟩ + [ y ∘ f , [ (l ∘ k) ∘ h , (l ∘ k) ∘ i ] ] ≈⟨ []-congˡ ([]-cong₂ (pullʳ (sym P₃.commute)) (assoc ○ P₂₃.universal∘i₂≈h₂)) ⟩ + [ y ∘ f , [ l ∘ j ∘ g , z ] ] ≈⟨ []-congˡ ([]-congʳ (pullˡ P₂₃.universal∘i₁≈h₁)) ⟩ + [ y ∘ f , [ y ∘ g , z ] ] ≈⟨ []∘assocˡ ⟨ + [ [ y ∘ f , y ∘ g ] , z ] ∘ +-assoc.from ≈⟨ []-cong₂ ∘[] identityʳ ⟩∘⟨refl ⟨ + [ y ∘ [ f , g ] , z ∘ id ] ∘ +-assoc.from ≈⟨ pullˡ []∘+₁ ⟨ + [ y , z ] ∘ ([ f , g ] +₁ id) ∘ +-assoc.from ∎ module _ where @@ -219,153 +253,160 @@ compose-assoc {_} {_} {_} {_} {c₁} {c₂} {c₃} = record open 𝒟 using (_⊗₀_; _⊗₁_; id; _∘_; _≈_; assoc; sym-assoc; identityʳ; ⊗; identityˡ; triangle; assoc-commute-to; assoc-commute-from) open 𝒟 using (_⇒_; unit) - α⇒ = 𝒟.associator.from - α⇐ = 𝒟.associator.to - - λ⇒ = 𝒟.unitorˡ.from - λ⇐ = 𝒟.unitorˡ.to - - ρ⇒ = 𝒟.unitorʳ.from - ρ⇐ = 𝒟.unitorʳ.to - - module α≅ = 𝒟.associator - module λ≅ = 𝒟.unitorˡ - module ρ≅ = 𝒟.unitorʳ + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐) open 𝒟.Equiv + +-α⇒ : {m n o : 𝒞.Obj} → m + (n + o) 𝒞.⇒ (m + n) + o +-α⇒ = +-assoc.from + +-α⇐ : {m n o : 𝒞.Obj} → (m + n) + o 𝒞.⇒ m + (n + o) +-α⇐ = +-assoc.to - s : unit ⇒ F₀ C₁.N + s : unit ⇒ F₀ N s = C₁.decoration - t : unit ⇒ F₀ C₂.N + t : unit ⇒ F₀ M t = C₂.decoration - u : unit ⇒ F₀ C₃.N + u : unit ⇒ F₀ P u = C₃.decoration - F-copairings : F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈ F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ (+-assoc.from) - F-copairings = begin - F₁ (l ∘′ m) ∘ F₁ [ w , x ] ∘ F₁ (id′ +₁ [ h , i ]) ≈⟨ pushˡ homomorphism ⟨ - F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F₁ (id′ +₁ [ h , i ]) ≈⟨ homomorphism ⟨ - F₁ (((l ∘′ m) ∘′ [ w , x ]) ∘′ (id′ +₁ [ h , i ])) ≈⟨ F-resp-≈ copairings ⟩ - F₁ ([ y , z ] ∘′ ([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ homomorphism ⟩ - F₁ [ y , z ] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ refl⟩∘⟨ homomorphism ⟩ - F₁ [ y , z ] ∘ F₁ ([ f , g ] +₁ id′) ∘ F₁ +-assoc.from ∎ - - coherences : φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈ F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐ - coherences = begin - φ (N , M + P) ∘ id ⊗₁ φ (M , P) ≈⟨ insertʳ α≅.isoʳ ⟩ - ((φ (N , M + P) ∘ id ⊗₁ φ (M , P)) ∘ α⇒) ∘ α⇐ ≈⟨ assoc ⟩∘⟨refl ⟩ - (φ (N , M + P) ∘ id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐ ≈⟨ assoc ⟩ - φ (N , M + P) ∘ (id ⊗₁ φ (M , P) ∘ α⇒) ∘ α⇐ ≈⟨ extendʳ associativity ⟨ - F₁ +-assoc.to ∘ (φ (N + M , P) ∘ φ (N , M) ⊗₁ id) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩ - F₁ +-assoc.to ∘ φ (N + M , P) ∘ φ (N , M) ⊗₁ id ∘ α⇐ ∎ - - triangle-to : α⇒ ∘ ρ⇐ ⊗₁ id ≈ id ⊗₁ λ⇐ - triangle-to = begin - α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pullˡ identityˡ ⟨ - id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ ⊗.identity ⟩∘⟨refl ⟨ - id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩⊗⟨ λ≅.isoˡ ⟩∘⟨refl ⟨ - id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨ - (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩ - id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ - id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ - id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id) ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩ - id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id ≈⟨ refl⟩∘⟨ ρ≅.isoʳ ⟩⊗⟨refl ⟩ - id ⊗₁ λ⇐ ∘ id ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗.identity ⟩ - id ⊗₁ λ⇐ ∘ id ≈⟨ identityʳ ⟩ - id ⊗₁ λ⇐ ∎ - - unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ - unitors = begin - s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pushˡ split₂ʳ ⟩ - s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨ - s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨ - s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ extendʳ assoc-commute-from ⟨ - α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨ - α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ - - F-l∘m = F₁ (l ∘′ m) + F[l∘m] : F₀ P₄.Q ⇒ F₀ P₅.Q + F[l∘m] = F₁ (l ∘′ m) + + F[w,x] : F₀ (N + R) ⇒ F₀ P₄.Q F[w,x] = F₁ [ w , x ] + + F[h,i] : F₀ (M + P) ⇒ F₀ R F[h,i] = F₁ [ h , i ] + + F[y,z] : F₀ (Q + P) ⇒ F₀ P₅.Q F[y,z] = F₁ [ y , z ] + + F[f,g] : F₀ (N + M) ⇒ F₀ Q F[f,g] = F₁ [ f , g ] - F-[f,g]+id = F₁ ([ f , g ] +₁ id′) - F-id+[h,i] = F₁ (id′ +₁ [ h , i ]) - φ-N,R = φ (N , R) - φ-M,P = φ (M , P) - φ-N+M,P = φ (N + M , P) - φ-N+M = φ (N , M) - φ-N,M+P = φ (N , M + P) - φ-N,M = φ (N , M) - φ-Q,P = φ (Q , P) + + F[[f,g]+id] : F₀ ((N + M) + P) ⇒ F₀ (Q + P) + F[[f,g]+id] = F₁ ([ f , g ] +₁ id′) + + F[id+[h,i]] : F₀ (N + (M + P)) ⇒ F₀ (N + R) + F[id+[h,i]] = F₁ (id′ +₁ [ h , i ]) + + φ[N,R] : F₀ N ⊗₀ F₀ R 𝒟.⇒ F₀ (N + R) + φ[N,R] = ⊗-homo.η (N , R) + + φ[M,P] : F₀ M ⊗₀ F₀ P 𝒟.⇒ F₀ (M + P) + φ[M,P] = ⊗-homo.η (M , P) + + φ[N+M,P] : F₀ (N + M) ⊗₀ F₀ P 𝒟.⇒ F₀ ((N + M) + P) + φ[N+M,P] = ⊗-homo.η (N + M , P) + + φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M) + φ[N,M] = ⊗-homo.η (N , M) + + φ[N,M+P] : F₀ N ⊗₀ F₀ (M + P) 𝒟.⇒ F₀ (N + (M + P)) + φ[N,M+P] = ⊗-homo.η (N , M + P) + + φ[Q,P] : F₀ Q ⊗₀ F₀ P 𝒟.⇒ F₀ (Q + P) + φ[Q,P] = ⊗-homo.η (Q , P) + + s⊗[t⊗u] : unit 𝒟.⇒ F₀ N ⊗₀ (F₀ M ⊗₀ F₀ P) s⊗[t⊗u] = s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ + + [s⊗t]⊗u : unit 𝒟.⇒ (F₀ N ⊗₀ F₀ M) ⊗₀ F₀ P [s⊗t]⊗u = (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ - deco-assoc - : F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ - ≈ F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ - deco-assoc = begin - F-l∘m ∘ F[w,x] ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pullˡ refl ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ s ⊗₁ (F[h,i] ∘ φ-M,P ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ-M,P ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨ refl ⟨ - (F-l∘m ∘ F[w,x]) ∘ φ-N,R ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , [ h , i ])) ⟩ - (F-l∘m ∘ F[w,x]) ∘ F-id+[h,i] ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ pullˡ assoc ⟩ - (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ (id ⊗₁ φ-M,P ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ - (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ φ-N,M+P ∘ id ⊗₁ φ-M,P ∘ s⊗[t⊗u] ≈⟨ refl⟩∘⟨ sym-assoc ⟩ - (F-l∘m ∘ F[w,x] ∘ F-id+[h,i]) ∘ (φ-N,M+P ∘ id ⊗₁ φ-M,P) ∘ s⊗[t⊗u] ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩ - (F[y,z] ∘ F-[f,g]+id ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩ - ((F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨ - (F[y,z] ∘ F-[f,g]+id) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ F₁ id′ ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ id ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ identityˡ ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ ((φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ cancelInner α≅.isoˡ ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ (φ-N+M,P ∘ φ-N,M ⊗₁ id) ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ assoc ⟩ - (F[y,z] ∘ F-[f,g]+id) ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ - F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ φ-N,M ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ - F[y,z] ∘ F-[f,g]+id ∘ φ-N+M,P ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute ([ f , g ] , id′)) ⟨ - F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ F₁ id′ ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨ refl ⟩ - F[y,z] ∘ φ-Q,P ∘ F[f,g] ⊗₁ id ∘ (φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ - F[y,z] ∘ φ-Q,P ∘ (F[f,g] ∘ φ-N,M ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ - -compose-idʳ : {C : DecoratedCospan A B} → Same (compose identity C) C + abstract + F-copairings : F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]] 𝒟.≈ F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-assoc.from + F-copairings = begin + F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]] ≈⟨ pushˡ homomorphism ⟨ + F₁ ((l ∘′ m) ∘′ [ w , x ]) ∘ F[id+[h,i]] ≈⟨ [ F′ ]-resp-square copairings ⟩ + F[y,z] ∘ F₁ (([ f , g ] +₁ id′) ∘′ +-assoc.from) ≈⟨ refl⟩∘⟨ homomorphism ⟩ + F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-assoc.from ∎ + + coherences : φ[N,M+P] ∘ id ⊗₁ φ[M,P] 𝒟.≈ F₁ +-assoc.to ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐ + coherences = begin + φ[N,M+P] ∘ id ⊗₁ φ[M,P] ≈⟨ refl⟩∘⟨ insertʳ 𝒟.associator.isoʳ ⟩ + φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ α⇒) ∘ α⇐ ≈⟨ extendʳ associativity ⟨ + F₁ +-assoc.to ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩ + F₁ +-assoc.to ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐ ∎ + + triangle-to : α⇒ {𝒟.unit} {𝒟.unit} {𝒟.unit} ∘ ρ⇐ ⊗₁ id 𝒟.≈ id ⊗₁ λ⇐ + triangle-to = begin + α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pullˡ identityˡ ⟨ + id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ ⊗.identity ⟩∘⟨refl ⟨ + id ⊗₁ id ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩⊗⟨ 𝒟.unitorˡ.isoˡ ⟩∘⟨refl ⟨ + id ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ identityʳ ⟩⊗⟨refl ⟩∘⟨refl ⟨ + (id ∘ id) ⊗₁ (λ⇐ ∘ λ⇒) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pushˡ ⊗-distrib-over-∘ ⟩ + id ⊗₁ λ⇐ ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ pullˡ triangle ⟩ + id ⊗₁ λ⇐ ∘ ρ⇒ ⊗₁ id ∘ ρ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ (id ∘ id) ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ identityˡ ⟩ + id ⊗₁ λ⇐ ∘ (ρ⇒ ∘ ρ⇐) ⊗₁ id ≈⟨ refl⟩∘⟨ 𝒟.unitorʳ.isoʳ ⟩⊗⟨refl ⟩ + id ⊗₁ λ⇐ ∘ id ⊗₁ id ≈⟨ refl⟩∘⟨ ⊗.identity ⟩ + id ⊗₁ λ⇐ ∘ id ≈⟨ identityʳ ⟩ + id ⊗₁ λ⇐ ∎ + + unitors : s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ 𝒟.≈ α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + unitors = begin + s ⊗₁ (t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pushˡ split₂ʳ ⟩ + s ⊗₁ t ⊗₁ u ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ λ₁≅ρ₁⇐ ⟩∘⟨refl ⟨ + s ⊗₁ t ⊗₁ u ∘ id ⊗₁ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ triangle-to ⟨ + s ⊗₁ t ⊗₁ u ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ extendʳ assoc-commute-from ⟨ + α⇒ ∘ (s ⊗₁ t) ⊗₁ u ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟨ + α⇒ ∘ (s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ + + deco-assoc + : F[l∘m] ∘ (F[w,x] ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐) + 𝒟.≈ F[y,z] ∘ φ[Q,P] ∘ (F[f,g] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ + deco-assoc = begin + F[l∘m] ∘ F[w,x] ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ pullˡ refl ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ s ⊗₁ (F[h,i] ∘ φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩∘⟨refl ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ (id ⊗₁ F[h,i] ∘ s ⊗₁ (φ[M,P] ∘ t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ split₂ˡ) ⟩∘⟨refl ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ (id ⊗₁ F[h,i] ∘ id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ id ⊗₁ F[h,i] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ + (F[l∘m] ∘ F[w,x]) ∘ φ[N,R] ∘ F₁ id′ ⊗₁ F[h,i] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (id′ , [ h , i ])) ⟩ + (F[l∘m] ∘ F[w,x]) ∘ F[id+[h,i]] ∘ φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ pullˡ assoc ⟩ + (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ φ[N,M+P] ∘ (id ⊗₁ φ[M,P] ∘ s ⊗₁ (t ⊗₁ u ∘ ρ⇐)) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩ + (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ φ[N,M+P] ∘ id ⊗₁ φ[M,P] ∘ s⊗[t⊗u] ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + (F[l∘m] ∘ F[w,x] ∘ F[id+[h,i]]) ∘ (φ[N,M+P] ∘ id ⊗₁ φ[M,P]) ∘ s⊗[t⊗u] ≈⟨ F-copairings ⟩∘⟨ coherences ⟩∘⟨ unitors ⟩ + (F[y,z] ∘ F[[f,g]+id] ∘ F₁ +-α⇒) ∘ (F₁ +-α⇐ ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ sym-assoc ⟩∘⟨ assoc ⟩ + ((F[y,z] ∘ F[[f,g]+id]) ∘ F₁ +-α⇒) ∘ F₁ +-α⇐ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ +-α⇒ ∘ F₁ +-α⇐ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ pushˡ homomorphism ⟨ + (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ (+-α⇒ ∘′ +-α⇐) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-resp-≈ +-assoc.isoʳ ⟩∘⟨refl ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ F₁ id′ ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ F-identity ⟩∘⟨refl ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ id ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ identityˡ ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ sym-assoc ⟩∘⟨refl ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ ((φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ α⇐) ∘ α⇒ ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ cancelInner 𝒟.associator.isoˡ ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ (φ[N+M,P] ∘ φ[N,M] ⊗₁ id) ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ assoc ⟩ + (F[y,z] ∘ F[[f,g]+id]) ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ assoc ⟩ + F[y,z] ∘ F[[f,g]+id] ∘ φ[N+M,P] ∘ φ[N,M] ⊗₁ id ∘ [s⊗t]⊗u ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + F[y,z] ∘ F[[f,g]+id] ∘ φ[N+M,P] ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute ([ f , g ] , id′)) ⟨ + F[y,z] ∘ φ[Q,P] ∘ F[f,g] ⊗₁ F₁ id′ ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟩ + F[y,z] ∘ φ[Q,P] ∘ F[f,g] ⊗₁ id ∘ (φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨ + F[y,z] ∘ φ[Q,P] ∘ (F[f,g] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ u ∘ ρ⇐ ∎ + +compose-idʳ : {C : DecoratedCospan A B} → compose identity C ≈ C compose-idʳ {A} {_} {C} = record { cospans-≈ = Cospans.compose-idʳ ; same-deco = deco-id } where - open DecoratedCospan C - - open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡) - + open 𝒞 using (pushout; [_,_]; ⊥; _+₁_; ¡; _+_) P = pushout 𝒞.id f₁ P′ = pushout-id-g {g = f₁} ≅P = up-to-iso P P′ - open Morphism 𝒞.U using (_≅_) module ≅P = _≅_ ≅P - open Pushout P - open 𝒞 using (cocartesian) renaming (id to id′; _∘_ to _∘′_) - open CocartesianMonoidal 𝒞.U cocartesian using (⊥+A≅A) - module ⊥+A≅A {a} = _≅_ (⊥+A≅A {a}) - module _ where - open 𝒞 using ( _⇒_ ; _∘_ ; _≈_ ; id ; U @@ -374,17 +415,13 @@ compose-idʳ {A} {_} {C} = record ; ∘[] ; []∘+₁ ; inject₂ ; assoc ; module HomReasoning ; module Dual ; module Equiv ) - open Equiv - open Dual.op-binaryProducts cocartesian using () renaming (⟨⟩-cong₂ to []-cong₂) - open ⇒-Reasoning U open HomReasoning - - copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to ≈ id + copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to 𝒞.≈ id copairing-id = begin ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id)) ∘ ⊥+A≅A.to ≈⟨ assoc ⟩ (≅P.from ∘ [ i₁ , i₂ ]) ∘ (¡ +₁ id) ∘ ⊥+A≅A.to ≈⟨ assoc ⟩ @@ -394,62 +431,54 @@ compose-idʳ {A} {_} {C} = record [ f₁ ∘ ¡ , id ∘ id ] ∘ ⊥+A≅A.to ≈⟨ []-cong₂ (sym (¡-unique (f₁ ∘ ¡))) identity² ⟩∘⟨refl ⟩ [ ¡ , id ] ∘ ⊥+A≅A.to ≈⟨ inject₂ ⟩ id ∎ - module _ where - open 𝒟 using ( id ; _∘_ ; _≈_ ; _⇒_ ; U ; assoc ; sym-assoc; identityˡ - ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ + ; monoidal ; _⊗₀_; _⊗₁_ ; unit ; unitorˡ ; unitorʳ ) - open ⊗-Reasoning monoidal open ⇒-Reasoning U - - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute - - module λ≅ = unitorˡ - λ⇒ = λ≅.from - λ⇐ = unitorˡ.to - ρ⇐ = unitorʳ.to - - open Coherence monoidal using (λ₁≅ρ₁⇐) + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (λ⇒; λ⇐; ρ⇐) + open Coherence 𝒟.monoidal using (λ₁≅ρ₁⇐) open 𝒟.Equiv - s : unit ⇒ F₀ N s = decoration - - cohere-s : φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈ F₁ ⊥+A≅A.to ∘ s - cohere-s = begin - φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ identityˡ ⟨ - id ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ - F₁ id′ ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨ - F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ - F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ - F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ (⊥ , N) ∘ (ε ⊗₁ id) ∘ (id ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ - F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ (⊥ , N) ∘ (ε ⊗₁ id)) ∘ (id ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryˡ ⟩ - F₁ ⊥+A≅A.to ∘ λ⇒ ∘ (id ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ λ₁≅ρ₁⇐ ⟨ - F₁ ⊥+A≅A.to ∘ λ⇒ ∘ (id ⊗₁ s) ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-to ⟨ - F₁ ⊥+A≅A.to ∘ λ⇒ ∘ λ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ λ≅.isoʳ ⟩ - F₁ ⊥+A≅A.to ∘ s ∎ - - deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s - deco-id = begin - F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ id) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (A , N) ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , id′)) ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ (⊥ , N) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ F₁ ⊥+A≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ - F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘′ ⊥+A≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ - F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ - id ∘ s ≈⟨ identityˡ ⟩ - s ∎ - -compose-idˡ : {C : DecoratedCospan A B} → Same (compose C identity) C + φ[⊥,N] : F₀ ⊥ ⊗₀ F₀ N ⇒ F₀ (⊥ + N) + φ[⊥,N] = ⊗-homo.η (⊥ , N) + φ[A,N] : F₀ A ⊗₀ F₀ N ⇒ F₀ (A + N) + φ[A,N] = ⊗-homo.η (A , N) + abstract + cohere-s : φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ 𝒟.≈ F₁ ⊥+A≅A.to ∘ s + cohere-s = begin + φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ identityˡ ⟨ + id ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ + F₁ id′ ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ F-resp-≈ ⊥+A≅A.isoˡ ⟩∘⟨refl ⟨ + F₁ (⊥+A≅A.to ∘′ ⊥+A≅A.from) ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ + F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ[⊥,N] ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ + F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ φ[⊥,N] ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ + F₁ ⊥+A≅A.to ∘ F₁ ⊥+A≅A.from ∘ (φ[⊥,N] ∘ ε ⊗₁ id) ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryˡ ⟩ + F₁ ⊥+A≅A.to ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ λ₁≅ρ₁⇐ ⟨ + F₁ ⊥+A≅A.to ∘ λ⇒ ∘ id ⊗₁ s ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ 𝒟.unitorˡ-commute-to ⟨ + F₁ ⊥+A≅A.to ∘ λ⇒ ∘ λ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ 𝒟.unitorˡ.isoʳ ⟩ + F₁ ⊥+A≅A.to ∘ s ∎ + deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ 𝒟.≈ s + deco-id = begin + F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ⊗₁ id) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ F-identity ⟩∘⟨refl ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[A,N] ∘ (F₁ ¡ ⊗₁ F₁ id′) ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (¡ , id′)) ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (¡ +₁ id′) ∘ φ[⊥,N] ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ φ[⊥,N] ∘ (ε ⊗₁ s) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘ F₁ ⊥+A≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ + F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (¡ +₁ id′)) ∘′ ⊥+A≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ + F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ + id ∘ s ≈⟨ identityˡ ⟩ + s ∎ + +compose-idˡ : {C : DecoratedCospan A B} → compose C identity ≈ C compose-idˡ {_} {B} {C} = record { cospans-≈ = Cospans.compose-idˡ ; same-deco = deco-id @@ -497,7 +526,7 @@ compose-idˡ {_} {B} {C} = record open ⇒-Reasoning U open HomReasoning - copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to ≈ id + copairing-id : ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to 𝒞.≈ id copairing-id = begin ((≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡)) ∘ A+⊥≅A.to ≈⟨ assoc ⟩ (≅P.from ∘ [ i₁ , i₂ ]) ∘ (id +₁ ¡) ∘ A+⊥≅A.to ≈⟨ assoc ⟩ @@ -510,11 +539,12 @@ compose-idˡ {_} {B} {C} = record module _ where + open 𝒞 using (_+_) open 𝒟 using ( id ; _∘_ ; _≈_ ; _⇒_ ; U ; assoc ; sym-assoc; identityˡ - ; monoidal ; _⊗₁_ ; unit ; unitorˡ ; unitorʳ + ; monoidal ; _⊗₀_; _⊗₁_ ; unit ; unitorˡ ; unitorʳ ; unitorʳ-commute-to ; module Equiv ) @@ -523,129 +553,146 @@ compose-idˡ {_} {B} {C} = record open ⊗-Reasoning monoidal open ⇒-Reasoning U - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute + φ[N,⊥] : F₀ N ⊗₀ F₀ ⊥ 𝒟.⇒ F₀ (N + ⊥) + φ[N,⊥] = ⊗-homo.η (N , ⊥) - module ρ≅ = unitorʳ - ρ⇒ = ρ≅.from - ρ⇐ = ρ≅.to + φ[N,B] : F₀ N ⊗₀ F₀ B 𝒟.⇒ F₀ (N + B) + φ[N,B] = ⊗-homo.η (N , B) s : unit ⇒ F₀ N s = decoration - cohere-s : φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈ F₁ A+⊥≅A.to ∘ s - cohere-s = begin - φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ identityˡ ⟨ - id ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ - F₁ id′ ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨ - F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ - F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩ - F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ (N , ⊥) ∘ (id ⊗₁ ε) ∘ (s ⊗₁ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ - F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ (N , ⊥) ∘ (id ⊗₁ ε)) ∘ (s ⊗₁ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryʳ ⟩ - F₁ A+⊥≅A.to ∘ ρ⇒ ∘ (s ⊗₁ id) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-to ⟨ - F₁ A+⊥≅A.to ∘ ρ⇒ ∘ ρ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ ρ≅.isoʳ ⟩ - F₁ A+⊥≅A.to ∘ s ∎ - - deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s - deco-id = begin - F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (id ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ (N , B) ∘ (F₁ id′ ⊗₁ F₁ ¡) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (id′ , ¡)) ⟩ - F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ (N , ⊥) ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ - F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ F₁ A+⊥≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ - F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘′ A+⊥≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ - F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ - id ∘ s ≈⟨ identityˡ ⟩ - s ∎ - -compose-id² : Same {A} (compose identity identity) identity + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (α⇒; α⇐; λ⇒; λ⇐; ρ⇒; ρ⇐) + + abstract + cohere-s : φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ 𝒟.≈ F₁ A+⊥≅A.to ∘ s + cohere-s = begin + φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ identityˡ ⟨ + id ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ F-identity ⟩∘⟨refl ⟨ + F₁ id′ ∘ φ[N,⊥] ∘ (s ⊗₁ ε) ∘ ρ⇐ ≈⟨ F-resp-≈ A+⊥≅A.isoˡ ⟩∘⟨refl ⟨ + F₁ (A+⊥≅A.to ∘′ A+⊥≅A.from) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ + F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩ + F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ φ[N,⊥] ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ + F₁ A+⊥≅A.to ∘ F₁ A+⊥≅A.from ∘ (φ[N,⊥] ∘ id ⊗₁ ε) ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ unitaryʳ ⟩ + F₁ A+⊥≅A.to ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ unitorʳ-commute-to ⟨ + F₁ A+⊥≅A.to ∘ ρ⇒ ∘ ρ⇐ ∘ s ≈⟨ refl⟩∘⟨ cancelˡ unitorʳ.isoʳ ⟩ + F₁ A+⊥≅A.to ∘ s ∎ + + deco-id : F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ 𝒟.≈ s + deco-id = begin + F₁ ≅P.from ∘ F₁ [ i₁ , i₂ ] ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F-identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ φ[N,B] ∘ F₁ id′ ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (id′ , ¡)) ⟩ + F₁ (≅P.from ∘′ [ i₁ , i₂ ]) ∘ F₁ (id′ +₁ ¡) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ φ[N,⊥] ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ cohere-s ⟩ + F₁ ((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘ F₁ A+⊥≅A.to ∘ s ≈⟨ pushˡ homomorphism ⟨ + F₁ (((≅P.from ∘′ [ i₁ , i₂ ]) ∘′ (id′ +₁ ¡)) ∘′ A+⊥≅A.to) ∘ s ≈⟨ F-resp-≈ copairing-id ⟩∘⟨refl ⟩ + F₁ id′ ∘ s ≈⟨ F-identity ⟩∘⟨refl ⟩ + id ∘ s ≈⟨ identityˡ ⟩ + s ∎ + +compose-id² : compose identity identity ≈ identity {A} compose-id² = compose-idˡ compose-equiv : {c₂ c₂′ : DecoratedCospan B C} {c₁ c₁′ : DecoratedCospan A B} - → Same c₂ c₂′ - → Same c₁ c₁′ - → Same (compose c₁ c₂) (compose c₁′ c₂′) + → c₂ ≈ c₂′ + → c₁ ≈ c₁′ + → compose c₁ c₂ ≈ (compose c₁′ c₂′) compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = record { cospans-≈ = ≅C₂∘C₁ ; same-deco = F≅N∘C₂∘C₁≈C₂′∘C₁′ } where - module ≅C₁ = Same ≅C₁ - module ≅C₂ = Same ≅C₂ + module ≅C₁ = _≈_ ≅C₁ + module ≅C₂ = _≈_ ≅C₂ module C₁ = DecoratedCospan c₁ module C₁′ = DecoratedCospan c₁′ module C₂ = DecoratedCospan c₂ module C₂′ = DecoratedCospan c₂′ ≅C₂∘C₁ = Cospans.compose-equiv ≅C₂.cospans-≈ ≅C₁.cospans-≈ - module ≅C₂∘C₁ = Cospans.Same ≅C₂∘C₁ + module ≅C₂∘C₁ = Cospan._≈_ ≅C₂∘C₁ P = 𝒞.pushout C₁.f₂ C₂.f₁ P′ = 𝒞.pushout C₁′.f₂ C₂′.f₁ module P = Pushout P module P′ = Pushout P′ - s = C₁.decoration - t = C₂.decoration - s′ = C₁′.decoration - t′ = C₂′.decoration + N M N′ M′ : 𝒞.Obj N = C₁.N M = C₂.N N′ = C₁′.N M′ = C₂′.N - φ = ⊗-homo.η - φ-commute = ⊗-homo.commute + s : 𝒟.unit 𝒟.⇒ F₀ N + s = C₁.decoration + t : 𝒟.unit 𝒟.⇒ F₀ M + t = C₂.decoration + + s′ : 𝒟.unit 𝒟.⇒ F₀ N′ + s′ = C₁′.decoration + + t′ : 𝒟.unit 𝒟.⇒ F₀ M′ + t′ = C₂′.decoration + + Q⇒ : ≅C₂∘C₁.C.N 𝒞.⇒ ≅C₂∘C₁.D.N Q⇒ = ≅C₂∘C₁.≅N.from + + N⇒ : ≅C₁.C.N 𝒞.⇒ ≅C₁.D.N N⇒ = ≅C₁.≅N.from + + M⇒ : ≅C₂.C.N 𝒞.⇒ ≅C₂.D.N M⇒ = ≅C₂.≅N.from module _ where - ρ⇒ = 𝒟.unitorʳ.from - ρ⇐ = 𝒟.unitorʳ.to + open ⊗-Util 𝒟.monoidal using (module Shorthands) + open Shorthands using (ρ⇒; ρ⇐) - open 𝒞 using ([_,_]; ∘[]; _+₁_; []∘+₁) renaming (_∘_ to _∘′_) + open 𝒞 using ([_,_]; ∘[]; _+_; _+₁_; []∘+₁) renaming (_∘_ to _∘′_) open 𝒞.Dual.op-binaryProducts 𝒞.cocartesian using () renaming (⟨⟩-cong₂ to []-cong₂) open 𝒟 + φ[N,M] : F₀ N ⊗₀ F₀ M 𝒟.⇒ F₀ (N + M) + φ[N,M] = ⊗-homo.η (N , M) + + φ[N′,M′] : F₀ N′ ⊗₀ F₀ M′ 𝒟.⇒ F₀ (N′ + M′) + φ[N′,M′] = ⊗-homo.η (N′ , M′) + open ⊗-Reasoning monoidal open ⇒-Reasoning U - F≅N∘C₂∘C₁≈C₂′∘C₁′ : F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈ F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐ - F≅N∘C₂∘C₁≈C₂′∘C₁′ = begin - F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ - F₁ (Q⇒ ∘′ [ P.i₁ , P.i₂ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ∘[] ⟩∘⟨refl ⟩ - F₁ ([ Q⇒ ∘′ P.i₁ , Q⇒ ∘′ P.i₂ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ([]-cong₂ P.universal∘i₁≈h₁ P.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ - F₁ ([ P′.i₁ ∘′ N⇒ , P′.i₂ ∘′ M⇒ ]) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ []∘+₁ ⟩∘⟨refl ⟨ - F₁ ([ P′.i₁ , P′.i₂ ] ∘′ (N⇒ +₁ M⇒)) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ - F₁ [ P′.i₁ , P′.i₂ ] ∘ F₁ (N⇒ +₁ M⇒) ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (N⇒ , M⇒)) ⟨ - F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ F₁ N⇒ ⊗₁ F₁ M⇒ ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟨ - F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ (F₁ N⇒ ∘ s) ⊗₁ (F₁ M⇒ ∘ t) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ≅C₁.same-deco ⟩⊗⟨ ≅C₂.same-deco ⟩∘⟨refl ⟩ - F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐ ∎ + abstract + F≅N∘C₂∘C₁≈C₂′∘C₁′ : F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ 𝒟.≈ F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ s′ ⊗₁ t′ ∘ ρ⇐ + F≅N∘C₂∘C₁≈C₂′∘C₁′ = begin + F₁ Q⇒ ∘ F₁ [ P.i₁ , P.i₂ ] ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟨ + F₁ (Q⇒ ∘′ [ P.i₁ , P.i₂ ]) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ∘[] ⟩∘⟨refl ⟩ + F₁ ([ Q⇒ ∘′ P.i₁ , Q⇒ ∘′ P.i₂ ]) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ ([]-cong₂ P.universal∘i₁≈h₁ P.universal∘i₂≈h₂) ⟩∘⟨refl ⟩ + F₁ ([ P′.i₁ ∘′ N⇒ , P′.i₂ ∘′ M⇒ ]) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ F-resp-≈ []∘+₁ ⟩∘⟨refl ⟨ + F₁ ([ P′.i₁ , P′.i₂ ] ∘′ (N⇒ +₁ M⇒)) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ pushˡ homomorphism ⟩ + F₁ [ P′.i₁ , P′.i₂ ] ∘ F₁ (N⇒ +₁ M⇒) ∘ φ[N,M] ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (⊗-homo.commute (N⇒ , M⇒)) ⟨ + F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ F₁ N⇒ ⊗₁ F₁ M⇒ ∘ s ⊗₁ t ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟨ + F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ (F₁ N⇒ ∘ s) ⊗₁ (F₁ M⇒ ∘ t) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ≅C₁.same-deco ⟩⊗⟨ ≅C₂.same-deco ⟩∘⟨refl ⟩ + F₁ [ P′.i₁ , P′.i₂ ] ∘ φ[N′,M′] ∘ s′ ⊗₁ t′ ∘ ρ⇐ ∎ DecoratedCospans : Category o (o ⊔ ℓ ⊔ ℓ′) (ℓ ⊔ e ⊔ e′) DecoratedCospans = record { Obj = 𝒞.Obj ; _⇒_ = DecoratedCospan - ; _≈_ = Same + ; _≈_ = _≈_ ; id = identity ; _∘_ = flip compose ; assoc = compose-assoc - ; sym-assoc = same-sym (compose-assoc) + ; sym-assoc = ≈-sym compose-assoc ; identityˡ = compose-idˡ ; identityʳ = compose-idʳ ; identity² = compose-id² - ; equiv = record - { refl = same-refl - ; sym = same-sym - ; trans = same-trans - } + ; equiv = ≈-equiv ; ∘-resp-≈ = compose-equiv } diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda index 0847165..9bee58e 100644 --- a/Category/Instance/FinitelyCocompletes.agda +++ b/Category/Instance/FinitelyCocompletes.agda @@ -1,29 +1,31 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level) + +open import Level using (Level; suc; _⊔_) + module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where +import Category.Instance.One.Properties as OneProps + open import Categories.Category using (_[_,_]) open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Helper using (categoryHelper) -open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) open import Categories.Category.Core using (Category) +open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Instance.Cats using (Cats) open import Categories.Category.Instance.One using (One; One-⊤) +open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products) open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat) open import Categories.Diagram.Coequalizer using (IsCoequalizer) open import Categories.Functor using (Functor) renaming (id to idF) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) open import Categories.Object.Coproduct using (IsCoproduct) open import Categories.Object.Initial using (IsInitial) open import Categories.Object.Product.Core using (Product) -open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×) -open import Category.Instance.One.Properties using (One-FinitelyCocomplete) open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′) -open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) open import Function.Base using (id; flip) -open import Level using (Level; suc; _⊔_) +open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact) FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) FinitelyCocompletes = categoryHelper record @@ -48,7 +50,7 @@ FinitelyCocompletes = categoryHelper record One-FCC : FinitelyCocompleteCategory o ℓ e One-FCC = record { U = One - ; finCo = One-FinitelyCocomplete + ; finCo = OneProps.finitelyCocomplete } _×_ diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda index 1452669..c6261bb 100644 --- a/Category/Instance/One/Properties.agda +++ b/Category/Instance/One/Properties.agda @@ -8,7 +8,7 @@ open import Categories.Category.Core using (Category) open import Categories.Category.Instance.One using () renaming (One to One′) One : Category o ℓ e -One = One′ +One = One′ {o} {ℓ} {e} open import Categories.Category.Cocartesian One using (Cocartesian) open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete) @@ -16,20 +16,20 @@ open import Categories.Object.Initial One using (Initial) open import Categories.Category.Cocartesian One using (BinaryCoproducts) -One-Initial : Initial -One-Initial = _ +initial : Initial +initial = _ -One-BinaryCoproducts : BinaryCoproducts -One-BinaryCoproducts = _ +coproducts : BinaryCoproducts +coproducts = _ -One-Cocartesian : Cocartesian -One-Cocartesian = record - { initial = One-Initial - ; coproducts = One-BinaryCoproducts +cocartesian : Cocartesian +cocartesian = record + { initial = initial + ; coproducts = coproducts } -One-FinitelyCocomplete : FinitelyCocomplete -One-FinitelyCocomplete = record - { cocartesian = One-Cocartesian +finitelyCocomplete : FinitelyCocomplete +finitelyCocomplete = record + { cocartesian = cocartesian ; coequalizer = _ } diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda deleted file mode 100644 index dedfa16..0000000 --- a/Category/Instance/Properties/FinitelyCocompletes.agda +++ /dev/null @@ -1,210 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Level using (Level) -module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where - -import Categories.Morphism.Reasoning as ⇒-Reasoning - -open import Categories.Category.BinaryProducts using (BinaryProducts) -open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_) -open import Categories.Diagram.Coequalizer using (IsCoequalizer) -open import Categories.Functor.Core using (Functor) -open import Categories.Functor using (_∘F_) renaming (id to idF) -open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) -open import Categories.Object.Initial using (IsInitial) -open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) -open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) -open import Functor.Exact using (IsRightExact; RightExactFunctor) -open import Level using (_⊔_; suc) - -FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) -FinitelyCocompletes-CC = record - { U = FinitelyCocompletes - ; cartesian = FinitelyCocompletes-Cartesian - } - -module FinCoCom = CartesianCategory FinitelyCocompletes-CC -open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) -- hiding (unique) - -module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where - - private - module 𝒞 = FinitelyCocompleteCategory 𝒞 - module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞) - - open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-) - open Equiv - - private - module -+- = Functor -+- - - +-resp-⊥ - : {(A , B) : 𝒞×𝒞.Obj} - → IsInitial 𝒞×𝒞.U (A , B) - → IsInitial 𝒞.U (A + B) - +-resp-⊥ {A , B} A,B-isInitial = record - { ! = [ A-isInitial.! , B-isInitial.! ] - ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } - } - where - open IsRightExact - open RightExactFunctor - module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial) - module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial) - - +-resp-+ - : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} - {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)} - {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} - → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂) - → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂) - +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record - { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] } - ; inject₁ = inject₁ - ; inject₂ = inject₂ - ; unique = unique - } - where - open IsRightExact - open RightExactFunctor - module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct)) - module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct)) - open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂) - open 𝒞 using (Obj; _≈_; module HomReasoning; assoc) - open HomReasoning - open ⇒-Reasoning 𝒞.U - inject₁ - : {X : Obj} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁ - inject₁ {_} {h₁} {h₂} = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈⟨ []∘+₁ ⟩ - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩ - [ h₁ ∘ i₁ , h₁ ∘ i₂ ] ≈⟨ +-g-η ⟩ - h₁ ∎ - inject₂ - : {X : Obj} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂ - inject₂ {_} {h₁} {h₂} = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈⟨ []∘+₁ ⟩ - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩ - [ h₂ ∘ i₁ , h₂ ∘ i₂ ] ≈⟨ +-g-η ⟩ - h₂ ∎ - unique - : {X : Obj} - {i : C₁ + C₂ ⇒ X} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁) - (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂) - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i - unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩ - [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ +-g-η ⟩ - i ∎ - where - eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁ - eq₁-₁ = begin - (i ∘ i₁) ∘ i₁-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩ - h₁ ∘ i₁ ∎ - eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁ - eq₂-₁ = begin - (i ∘ i₁) ∘ i₂-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩ - h₂ ∘ i₁ ∎ - eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂ - eq₁-₂ = begin - (i ∘ i₂) ∘ i₁-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩ - h₁ ∘ i₂ ∎ - eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂ - eq₂-₂ = begin - (i ∘ i₂) ∘ i₂-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩ - h₂ ∘ i₂ ∎ - - +-resp-coeq - : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} - {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)} - {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} - → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) - → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂) - +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record - { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism - ; coequalize = coequalize - ; universal = universal _ - ; unique = uniq _ - } - where - open IsRightExact - open RightExactFunctor - module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq) - module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq) - open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η) - open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc) - open 𝒞.HomReasoning - open ⇒-Reasoning 𝒞.U - - module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where - - eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁ - eq₁ = begin - (k ∘ i₁) ∘ f₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩ - k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩ - (k ∘ i₁) ∘ g₁ ∎ - - eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂ - eq₂ = begin - (k ∘ i₂) ∘ f₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩ - k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩ - (k ∘ i₂) ∘ g₂ ∎ - - coequalize : C₁ + C₂ ⇒ X - coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] - - universal : k ≈ coequalize ∘ (h₁ +₁ h₂) - universal = begin - k ≈⟨ +-g-η ⟨ - [ k ∘ i₁ , k ∘ i₂ ] ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩ - [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨ - coequalize ∘ (h₁ +₁ h₂) ∎ - - uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize - uniq {i} eq′ = begin - i ≈⟨ +-g-η ⟨ - [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩ - [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎ - where - eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁ - eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁ - eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂ - eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂ - -module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where - - open FinCoCom using (_⇒_; _∘_; id) - module 𝒞 = FinitelyCocompleteCategory 𝒞 - - -+- : 𝒞 × 𝒞 ⇒ 𝒞 - -+- = record - { F = 𝒞.-+- - ; isRightExact = record - { F-resp-⊥ = +-resp-⊥ 𝒞 - ; F-resp-+ = +-resp-+ 𝒞 - ; F-resp-coeq = +-resp-coeq 𝒞 - } - } - - [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 - [x+y]+z = -+- ∘ (-+- ×₁ id) - - x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 - x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda new file mode 100644 index 0000000..fa15295 --- /dev/null +++ b/Category/Instance/Properties/SymMonCat.agda @@ -0,0 +1,166 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level; suc; _⊔_) +module Category.Instance.Properties.SymMonCat {o ℓ e : Level} where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI +import Categories.Functor.Monoidal.Symmetric {o} {o} {ℓ} {ℓ} {e} {e} as SMF + +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) + +open import Categories.Category using (Category; _[_≈_]; _[_∘_]) +open import Categories.Object.Product.Core SymMonCat using (Product) +open import Categories.Object.Terminal SymMonCat using (Terminal) +open import Categories.Category.Instance.One using (One) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Category.Cartesian SymMonCat using (Cartesian) +open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts) +open import Categories.Functor.Monoidal.Construction.Product + using () + renaming + ( πˡ-SymmetricMonoidalFunctor to πˡ-SMF + ; πʳ-SymmetricMonoidalFunctor to πʳ-SMF + ; ※-SymmetricMonoidalFunctor to ※-SMF + ) +open import Categories.Category.Monoidal.Construction.Product using (Product-SymmetricMonoidalCategory) +open import Categories.Category.Product.Properties using () renaming (project₁ to p₁; project₂ to p₂; unique to u) +open import Data.Product.Base using (_,_; proj₁; proj₂) + +open SMF.Lax using (SymmetricMonoidalFunctor) +open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + +module Cone + {A B X : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor X A} + {G : SymmetricMonoidalFunctor X B} where + + module A = SymmetricMonoidalCategory A + module B = SymmetricMonoidalCategory B + module X = SymmetricMonoidalCategory X + module F = SymmetricMonoidalFunctor X A F + module G = SymmetricMonoidalFunctor X B G + + A×B : SymmetricMonoidalCategory o ℓ e + A×B = (Product-SymmetricMonoidalCategory A B) + + πˡ : SymmetricMonoidalFunctor A×B A + πˡ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + + πʳ : SymmetricMonoidalFunctor A×B B + πʳ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + + module _ where + open Category A.U + open Equiv + open ⇒-Reasoning A.U + open ⊗-Reasoning A.monoidal + project₁ : SymMonCat [ SymMonCat [ πˡ ∘ ※-SMF F G ] ≈ F ] + project₁ = record + { U = p₁ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = identityˡ ○ identityʳ + ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym A.⊗.identity } + } + } + module _ (H : SymmetricMonoidalFunctor X A×B) (eq₁ : SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ]) where + private + module H = SymmetricMonoidalFunctor X A×B H + open SymmetricMonoidalNaturalIsomorphism eq₁ + ε-compat₁ : ⇐.η X.unit A.∘ F.ε A.≈ H.ε .proj₁ + ε-compat₁ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ + ⊗-homo-compat₁ + : ∀ {C D} + → ⇐.η (X.⊗.₀ (C , D)) ∘ F.⊗-homo.η (C , D) + ≈ H.⊗-homo.η (C , D) .proj₁ ∘ A.⊗.₁ (⇐.η C , ⇐.η D) + ⊗-homo-compat₁ {C} {D} = + insertʳ + (sym ⊗-distrib-over-∘ + ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D + ○ A.⊗.identity) + ○ (pullʳ (sym ⊗-homo-compat) + ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D))) + ○ identityʳ) ⟩∘⟨refl + + module _ where + open Category B.U + open Equiv + open ⇒-Reasoning B.U + open ⊗-Reasoning B.monoidal + project₂ : SymMonCat [ SymMonCat [ πʳ ∘ ※-SMF F G ] ≈ G ] + project₂ = record + { U = p₂ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} + ; F⇒G-isMonoidal = record + { ε-compat = identityˡ ○ identityʳ + ; ⊗-homo-compat = λ { {C} {D} → identityˡ ○ refl⟩∘⟨ sym B.⊗.identity } + } + } + module _ (H : SymmetricMonoidalFunctor X A×B) (eq₂ : SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ]) where + private + module H = SymmetricMonoidalFunctor X A×B H + open SymmetricMonoidalNaturalIsomorphism eq₂ + ε-compat₂ : ⇐.η X.unit ∘ G.ε ≈ H.ε .proj₂ + ε-compat₂ = refl⟩∘⟨ sym ε-compat ○ cancelˡ (iso.isoˡ X.unit) ○ identityʳ + ⊗-homo-compat₂ + : ∀ {C D} + → ⇐.η (X.⊗.₀ (C , D)) ∘ G.⊗-homo.η (C , D) + ≈ H.⊗-homo.η (C , D) .proj₂ ∘ B.⊗.₁ (⇐.η C , ⇐.η D) + ⊗-homo-compat₂ {C} {D} = + insertʳ + (sym ⊗-distrib-over-∘ + ○ iso.isoʳ C ⟩⊗⟨ iso.isoʳ D + ○ B.⊗.identity) + ○ (pullʳ (sym ⊗-homo-compat) + ○ cancelˡ (iso.isoˡ (X.⊗.₀ (C , D))) + ○ identityʳ) ⟩∘⟨refl + + unique + : (H : SymmetricMonoidalFunctor X A×B) + → SymMonCat [ SymMonCat [ πˡ ∘ H ] ≈ F ] + → SymMonCat [ SymMonCat [ πʳ ∘ H ] ≈ G ] + → SymMonCat [ ※-SMF F G ≈ H ] + unique H eq₁ eq₂ = record + { U = u {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A.U} {B.U} {X.U} {F.F} {G.F} {H.F} eq₁.U eq₂.U + ; F⇒G-isMonoidal = record + { ε-compat = ε-compat₁ H eq₁ , ε-compat₂ H eq₂ + ; ⊗-homo-compat = ⊗-homo-compat₁ H eq₁ , ⊗-homo-compat₂ H eq₂ + } + } + where + module H = SymmetricMonoidalFunctor X A×B H + module eq₁ = SymmetricMonoidalNaturalIsomorphism eq₁ + module eq₂ = SymmetricMonoidalNaturalIsomorphism eq₂ + +prod-SymMonCat : ∀ {A B} → Product A B +prod-SymMonCat {A} {B} = record + { A×B = Product-SymmetricMonoidalCategory A B + ; π₁ = πˡ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + ; π₂ = πʳ-SMF {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} + ; ⟨_,_⟩ = ※-SMF + ; project₁ = λ { {X} {f} {g} → Cone.project₁ {A} {B} {X} {f} {g} } + ; project₂ = λ { {X} {f} {g} → Cone.project₂ {A} {B} {X} {f} {g} } + ; unique = λ { {X} {h} {f} {g} eq₁ eq₂ → Cone.unique {A} {B} {X} {f} {g} h eq₁ eq₂ } + } + +SymMonCat-BinaryProducts : BinaryProducts +SymMonCat-BinaryProducts = record { product = prod-SymMonCat } + +SymMonCat-Terminal : Terminal +SymMonCat-Terminal = record + { ⊤ = record + { U = One + ; monoidal = _ + ; symmetric = _ + } + ; ⊤-is-terminal = _ + } + +SymMonCat-Cartesian : Cartesian +SymMonCat-Cartesian = record + { terminal = SymMonCat-Terminal + ; products = SymMonCat-BinaryProducts + } diff --git a/Category/Instance/Setoids/SymmetricMonoidal.agda b/Category/Instance/Setoids/SymmetricMonoidal.agda index fa4d903..995ddf3 100644 --- a/Category/Instance/Setoids/SymmetricMonoidal.agda +++ b/Category/Instance/Setoids/SymmetricMonoidal.agda @@ -1,33 +1,47 @@ {-# OPTIONS --without-K --safe #-} -module Category.Instance.Setoids.SymmetricMonoidal {ℓ} where +open import Level using (Level; _⊔_; suc) +module Category.Instance.Setoids.SymmetricMonoidal {c ℓ : Level} where -open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian; Setoids-Cocartesian) renaming (Setoids-Monoidal to ×-monoidal) -open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids ℓ ℓ) Setoids-Cartesian +open import Categories.Category.Cartesian.SymmetricMonoidal (Setoids c ℓ) Setoids-Cartesian using () renaming (symmetric to ×-symmetric) -open import Level using (suc) -open import Categories.Category.Cocartesian (Setoids ℓ ℓ) +open import Categories.Category.Cocartesian (Setoids c (c ⊔ ℓ)) using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) -open CocartesianMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-monoidal) -open CocartesianSymmetricMonoidal (Setoids-Cocartesian {ℓ} {ℓ}) using (+-symmetric) +open CocartesianMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-monoidal) +open CocartesianSymmetricMonoidal (Setoids-Cocartesian {c} {ℓ}) using (+-symmetric) -Setoids-× : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) + +opaque + + ×-monoidal′ : Monoidal (Setoids c ℓ) + ×-monoidal′ = ×-monoidal {c} {ℓ} + + ×-symmetric′ : Symmetric ×-monoidal′ + ×-symmetric′ = ×-symmetric + +Setoids-× : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids-× = record - { U = Setoids ℓ ℓ - ; monoidal = ×-monoidal - ; symmetric = ×-symmetric + { U = Setoids c ℓ + ; monoidal = ×-monoidal′ + ; symmetric = ×-symmetric′ } -Setoids-+ : SymmetricMonoidalCategory (suc ℓ) ℓ ℓ +Setoids-+ : SymmetricMonoidalCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ) Setoids-+ = record - { U = Setoids ℓ ℓ + { U = Setoids c (c ⊔ ℓ) ; monoidal = +-monoidal ; symmetric = +-symmetric } + +module Setoids-× = SymmetricMonoidalCategory Setoids-× +module Setoids-+ = SymmetricMonoidalCategory Setoids-+ diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda new file mode 100644 index 0000000..e4b136c --- /dev/null +++ b/Category/Instance/SymMonCat.agda @@ -0,0 +1,74 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --lossy-unification #-} + +open import Level using (Level; suc; _⊔_) +module Category.Instance.SymMonCat {o ℓ e : Level} where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Functor.Monoidal.Symmetric as SMF +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Morphism as Morphism +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI +import Categories.Category.Monoidal.Utilities as MonoidalUtil +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +open import Relation.Binary.Core using (Rel) + +open import Categories.Category using (Category; _[_,_]; _[_∘_]) +open import Categories.Category.Helper using (categoryHelper) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) + +open SMF.Lax using (SymmetricMonoidalFunctor) +open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) + +assoc + : {A B C D : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + {G : SymmetricMonoidalFunctor B C} + {H : SymmetricMonoidalFunctor C D} + → SymmetricMonoidalNaturalIsomorphism + (∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F) + (∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F)) +assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H} + +identityˡ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F +identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + +identityʳ + : {A B : SymmetricMonoidalCategory o ℓ e} + {F : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F +identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F} + +Compose + : {A B C : SymmetricMonoidalCategory o ℓ e} + → SymmetricMonoidalFunctor B C + → SymmetricMonoidalFunctor A B + → SymmetricMonoidalFunctor A C +Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G + +∘-resp-≈ + : {A B C : SymmetricMonoidalCategory o ℓ e} + {f h : SymmetricMonoidalFunctor B C} + {g i : SymmetricMonoidalFunctor A B} + → SymmetricMonoidalNaturalIsomorphism f h + → SymmetricMonoidalNaturalIsomorphism g i + → SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i) +∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′ + +SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) +SymMonCat = categoryHelper record + { Obj = SymmetricMonoidalCategory o ℓ e + ; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e} + ; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} } + ; id = λ { {X} → idF-SymmetricMonoidal X } + ; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G } + ; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} } + ; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} } + ; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} } + ; equiv = isEquivalence + ; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i } + } |