1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
{-# OPTIONS --without-K --safe #-}
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
module Category.Monoidal.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning.Iso as IsoReasoning
open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; Category)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal)
open import Categories.Category.Cocartesian.SymmetricMonoidal using (module CocartesianSymmetricMonoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Functor using (Functor)
open import Categories.Functor.Properties using ([_]-resp-≅)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
open import Category.Instance.Cospans 𝒞 using (Cospans)
open import Category.Diagram.Cospan using (Cospan; cospan)
open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes-CC)
open import Category.Monoidal.Instance.Cospans.Lift {o} {ℓ} {e} using (module Square)
open import Data.Product.Base using (_,_)
open import Functor.Instance.Cospan.Stack 𝒞 using (⊗)
open import Functor.Instance.Cospan.Embed 𝒞 using (L; L-resp-⊗)
module 𝒞 = FinitelyCocompleteCategory 𝒞
open CocartesianMonoidal 𝒞.cocartesian using (⊥+--id; -+⊥-id; ⊥+A≅A; A+⊥≅A; +-monoidal)
open CocartesianSymmetricMonoidal 𝒞.U 𝒞.cocartesian using (+-symmetric)
open Monoidal +-monoidal using () renaming (triangle to tri; pentagon to pent)
open Symmetric +-symmetric using (braiding) renaming (hexagon₁ to hex₁; hexagon₂ to hex₂; commutative to comm)
open import Categories.Category.Monoidal.Utilities +-monoidal using (associator-naturalIsomorphism)
module _ where
open CartesianCategory FinitelyCocompletes-CC using (_×_)
𝒞×𝒞 : FinitelyCocompleteCategory o ℓ e
𝒞×𝒞 = 𝒞 × 𝒞
[𝒞×𝒞]×𝒞 : FinitelyCocompleteCategory o ℓ e
[𝒞×𝒞]×𝒞 = (𝒞 × 𝒞) × 𝒞
CospansMonoidal : Monoidal Cospans
CospansMonoidal = record
{ ⊗ = ⊗
; unit = ⊥
; unitorˡ = [ L ]-resp-≅ ⊥+A≅A
; unitorʳ = [ L ]-resp-≅ A+⊥≅A
; associator = [ L ]-resp-≅ (≅.sym +-assoc)
; unitorˡ-commute-from = λ { {X} {Y} {f} → Unitorˡ.from f }
; unitorˡ-commute-to = λ { {X} {Y} {f} → Unitorˡ.to f }
; unitorʳ-commute-from = λ { {X} {Y} {f} → Unitorʳ.from f }
; unitorʳ-commute-to = λ { {X} {Y} {f} → Unitorʳ.to f }
; assoc-commute-from = Associator.from _
; assoc-commute-to = Associator.to _
; triangle = triangle
; pentagon = pentagon
}
where
module Cospans = Category Cospans
module Unitorˡ = Square ⊥+--id
module Unitorʳ = Square -+⊥-id
module Associator = Square {[𝒞×𝒞]×𝒞} {𝒞} associator-naturalIsomorphism
open Cospans.HomReasoning
open Cospans using (id)
open Cospans.Equiv
open Functor L renaming (F-resp-≈ to L-resp-≈)
open 𝒞 using (⊥; Obj; U; +-assoc)
open Morphism U using (module ≅)
λ⇒ = Unitorˡ.FX≅GX′.from
ρ⇒ = Unitorʳ.FX≅GX′.from
α⇒ = Associator.FX≅GX′.from
triangle : {X Y : Obj} → Cospans [ Cospans [ ⊗.₁ (id {X} , λ⇒) ∘ α⇒ ] ≈ ⊗.₁ (ρ⇒ , id {Y}) ]
triangle = sym L-resp-⊗ ⟩∘⟨refl ○ sym homomorphism ○ L-resp-≈ tri ○ L-resp-⊗
pentagon : {W X Y Z : Obj} → Cospans [ Cospans [ ⊗.₁ (id {W} , α⇒ {(X , Y) , Z}) ∘ Cospans [ α⇒ ∘ ⊗.₁ (α⇒ , id) ] ] ≈ Cospans [ α⇒ ∘ α⇒ ] ]
pentagon = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym homomorphism ○ sym homomorphism ○ L-resp-≈ pent ○ homomorphism
CospansBraided : Braided CospansMonoidal
CospansBraided = record
{ braiding = niHelper record
{ η = λ (X , Y) → Braiding.FX≅GX′.from {X , Y}
; η⁻¹ = λ (Y , X) → Braiding.FX≅GX′.to {Y , X}
; commute = λ (cospan f₁ f₂ , cospan g₁ g₂) → Braiding.from (cospan (f₁ , g₁) (f₂ , g₂))
; iso = λ (X , Y) → Braiding.FX≅GX′.iso {X , Y}
}
; hexagon₁ = sym L-resp-⊗ ⟩∘⟨ refl ⟩∘⟨ sym L-resp-⊗ ○ refl⟩∘⟨ sym homomorphism ○ sym homomorphism ○ L-resp-≈ hex₁ ○ homomorphism ○ refl⟩∘⟨ homomorphism
; hexagon₂ = sym L-resp-⊗ ⟩∘⟨refl ⟩∘⟨ sym L-resp-⊗ ○ sym homomorphism ⟩∘⟨refl ○ sym homomorphism ○ L-resp-≈ hex₂ ○ homomorphism ○ homomorphism ⟩∘⟨refl
}
where
module Cospans = Category Cospans
open Cospans.Equiv
open Cospans.HomReasoning
module Braiding = Square {𝒞×𝒞} {𝒞} braiding
open Functor L renaming (F-resp-≈ to L-resp-≈)
CospansSymmetric : Symmetric CospansMonoidal
CospansSymmetric = record
{ braided = CospansBraided
; commutative = sym homomorphism ○ L-resp-≈ comm ○ identity
}
where
module Cospans = Category Cospans
open Cospans.Equiv
open Cospans.HomReasoning
open Functor L renaming (F-resp-≈ to L-resp-≈)
|
