diff options
Diffstat (limited to 'Functor/Instance')
| -rw-r--r-- | Functor/Instance/Cospan/Embed.agda | 103 | ||||
| -rw-r--r-- | Functor/Instance/Cospan/Stack.agda | 98 | ||||
| -rw-r--r-- | Functor/Instance/Decorate.agda | 165 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Embed.agda | 275 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Stack.agda | 430 | ||||
| -rw-r--r-- | Functor/Instance/Endo/List.agda | 15 | ||||
| -rw-r--r-- | Functor/Instance/List.agda | 67 | ||||
| -rw-r--r-- | Functor/Instance/Monoidalize.agda | 43 | ||||
| -rw-r--r-- | Functor/Instance/Multiset.agda | 72 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 56 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 60 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Preimage.agda | 65 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 81 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 79 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 110 | ||||
| -rw-r--r-- | Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda | 229 |
16 files changed, 1844 insertions, 104 deletions
diff --git a/Functor/Instance/Cospan/Embed.agda b/Functor/Instance/Cospan/Embed.agda index 77f0361..6dbc04a 100644 --- a/Functor/Instance/Cospan/Embed.agda +++ b/Functor/Instance/Cospan/Embed.agda @@ -1,4 +1,5 @@ {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) @@ -14,9 +15,10 @@ open import Categories.Category using (_[_,_]; _[_∘_]; _[_≈_]) open import Categories.Category.Core using (Category) open import Categories.Functor.Core using (Functor) open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan 𝒞 using (cospan) open import Data.Product.Base using (_,_) open import Function.Base using (id) -open import Functor.Instance.Cospan.Stack using (⊗) +open import Functor.Instance.Cospan.Stack 𝒞 using (⊗) module 𝒞 = FinitelyCocompleteCategory 𝒞 module Cospans = Category Cospans @@ -28,24 +30,26 @@ open Morphism U using (module ≅; _≅_) open PushoutProperties U using (up-to-iso) open Pushout′ U using (pushout-id-g; pushout-f-id) -L₁ : {A B : 𝒞.Obj} → U [ A , B ] → Cospans [ A , B ] -L₁ f = record - { f₁ = f - ; f₂ = 𝒞.id - } +private + variable + A B C : 𝒞.Obj + W X Y Z : 𝒞.Obj + +L₁ : U [ A , B ] → Cospans [ A , B ] +L₁ f = cospan f 𝒞.id -L-identity : {A : 𝒞.Obj} → L₁ 𝒞.id ≈ Cospans.id {A} +L-identity : L₁ 𝒞.id ≈ Cospans.id {A} L-identity = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identity² } -L-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] +L-homomorphism : {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] L-homomorphism {X} {Y} {Z} {f} {g} = record { ≅N = up-to-iso P′ P - ; from∘f₁≈f₁′ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) - ; from∘f₂≈f₂′ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₁≈f₁ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) + ; from∘f₂≈f₂ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ } where open ⇒-Reasoning U @@ -57,11 +61,11 @@ L-homomorphism {X} {Y} {Z} {f} {g} = record module P = Pushout P module P′ = Pushout P′ -L-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] +L-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] L-resp-≈ {A} {B} {f} {g} f≈g = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ ○ f≈g - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identityˡ ○ f≈g + ; from∘f₂≈f₂ = 𝒞.identity² } where open 𝒞.HomReasoning @@ -75,24 +79,21 @@ L = record ; F-resp-≈ = L-resp-≈ } -R₁ : {A B : 𝒞.Obj} → U [ B , A ] → Cospans [ A , B ] -R₁ g = record - { f₁ = 𝒞.id - ; f₂ = g - } +R₁ : U [ B , A ] → Cospans [ A , B ] +R₁ g = cospan 𝒞.id g -R-identity : {A : 𝒞.Obj} → R₁ 𝒞.id ≈ Cospans.id {A} +R-identity : R₁ 𝒞.id ≈ Cospans.id {A} R-identity = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identity² } -R-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] -R-homomorphism {X} {Y} {Z} {f} {g} = record +R-homomorphism : {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] +R-homomorphism {f} {g} = record { ≅N = up-to-iso P′ P - ; from∘f₁≈f₁′ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ - ; from∘f₂≈f₂′ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) + ; from∘f₁≈f₁ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₂≈f₂ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) } where open ⇒-Reasoning U @@ -104,11 +105,11 @@ R-homomorphism {X} {Y} {Z} {f} {g} = record module P = Pushout P module P′ = Pushout P′ -R-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] -R-resp-≈ {A} {B} {f} {g} f≈g = record +R-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] +R-resp-≈ {f} {g} f≈g = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ f≈g + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identityˡ ○ f≈g } where open 𝒞.HomReasoning @@ -122,17 +123,11 @@ R = record ; F-resp-≈ = R-resp-≈ } -B₁ : {A B C : 𝒞.Obj} → U [ A , C ] → U [ B , C ] → Cospans [ A , B ] -B₁ f g = record - { f₁ = f - ; f₂ = g - } - -B∘L : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ B₁ g h ∘ L₁ f ] ≈ B₁ (U [ g ∘ f ]) h -B∘L {W} {X} {Y} {Z} {f} {g} {h} = record +B∘L : {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ cospan g h ∘ L₁ f ] ≈ cospan (U [ g ∘ f ]) h +B∘L {f} {g} {h} = record { ≅N = up-to-iso P P′ - ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) - ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) + ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ } where open ⇒-Reasoning U @@ -144,11 +139,11 @@ B∘L {W} {X} {Y} {Z} {f} {g} {h} = record module P = Pushout P module P′ = Pushout P′ -R∘B : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ B₁ f g ] ≈ B₁ f (U [ g ∘ h ]) -R∘B {W} {X} {Y} {Z} {f} {g} {h} = record +R∘B : {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ cospan f g ] ≈ cospan f (U [ g ∘ h ]) +R∘B {f} {g} {h} = record { ≅N = up-to-iso P P′ - ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ - ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) + ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) } where open ⇒-Reasoning U @@ -164,20 +159,18 @@ module _ where open _≅_ - ≅-L-R : ∀ {X Y : 𝒞.Obj} (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) - ≅-L-R {X} {Y} X≅Y = record + ≅-L-R : (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) + ≅-L-R X≅Y = record { ≅N = X≅Y - ; from∘f₁≈f₁′ = isoʳ X≅Y - ; from∘f₂≈f₂′ = 𝒞.identityʳ + ; from∘f₁≈f₁ = isoʳ X≅Y + ; from∘f₂≈f₂ = 𝒞.identityʳ } -module ⊗ = Functor (⊗ 𝒞) - -L-resp-⊗ : {X Y X′ Y′ : 𝒞.Obj} {a : U [ X , X′ ]} {b : U [ Y , Y′ ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) -L-resp-⊗ {X} {Y} {X′} {Y′} {a} {b} = record +L-resp-⊗ : {a : U [ W , X ]} {b : U [ Y , Z ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) +L-resp-⊗ {a} {b} = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ - ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) + ; from∘f₁≈f₁ = 𝒞.identityˡ + ; from∘f₂≈f₂ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) } where open 𝒞.HomReasoning diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda index b7664dc..b72219b 100644 --- a/Functor/Instance/Cospan/Stack.agda +++ b/Functor/Instance/Cospan/Stack.agda @@ -9,11 +9,13 @@ import Categories.Diagram.Pushout.Properties as PushoutProperties import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as ⇒-Reasoning -open import Categories.Category.Core using (Category) +open import Categories.Category using (Category) +open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor) -open import Category.Instance.Cospans 𝒞 using (Cospan; Cospans; Same; id-Cospan; compose) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan 𝒞 as Cospan using (Cospan; identity; compose; _⊗_) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using () renaming (_×_ to _×′_) -open import Category.Instance.Properties.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) +open import Category.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout) open import Level using (Level; _⊔_; suc) @@ -32,27 +34,19 @@ open DiagramPushout U×U using () renaming (Pushout to Pushout′) open import Categories.Category.Monoidal.Utilities monoidal using (_⊗ᵢ_) -together : {A A′ B B′ : Obj} → Cospan A B → Cospan A′ B′ → Cospan (A + A′) (B + B′) -together A⇒B A⇒B′ = record - { f₁ = f₁ A⇒B +₁ f₁ A⇒B′ - ; f₂ = f₂ A⇒B +₁ f₂ A⇒B′ - } - where - open Cospan - -id⊗id≈id : {A B : Obj} → Same (together (id-Cospan {A}) (id-Cospan {B})) (id-Cospan {A + B}) +id⊗id≈id : {A B : Obj} → identity {A} ⊗ identity {B} Cospan.≈ identity {A + B} id⊗id≈id {A} {B} = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = from∘f≈f′ - ; from∘f₂≈f₂′ = from∘f≈f′ + ; from∘f₁≈f₁ = from∘f≈f + ; from∘f₂≈f₂ = from∘f≈f } where open Morphism U using (module ≅) open HomReasoning open 𝒞 using (+-η; []-cong₂) open coproduct {A} {B} using (i₁; i₂) - from∘f≈f′ : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id - from∘f≈f′ = begin + from∘f≈f : id ∘ [ i₁ ∘ id , i₂ ∘ id ] 𝒞.≈ id + from∘f≈f = begin id ∘ [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ identityˡ ⟩ [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ []-cong₂ identityʳ identityʳ ⟩ [ i₁ , i₂ ] ≈⟨ +-η ⟩ @@ -64,14 +58,14 @@ homomorphism → (B⇒C : Cospan B C) → (A⇒B′ : Cospan A′ B′) → (B⇒C′ : Cospan B′ C′) - → Same (together (compose A⇒B B⇒C) (compose A⇒B′ B⇒C′)) (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′) ) + → compose A⇒B B⇒C ⊗ compose A⇒B′ B⇒C′ Cospan.≈ compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′) homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record { ≅N = ≅N - ; from∘f₁≈f₁′ = from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = from∘f₂≈f₂′ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where - open Cospan + open Cospan.Cospan open Pushout open HomReasoning open ⇒-Reasoning U @@ -89,56 +83,62 @@ homomorphism A⇒B B⇒C A⇒B′ B⇒C′ = record P₃′ = IsPushout⇒Pushout (-+-.F-resp-pushout P₁×P₂.isPushout) ≅N : Q P₃′ ≅ Q P₃ ≅N = up-to-iso P₃′ P₃ - from∘f₁≈f₁′ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′)) - from∘f₁≈f₁′ = begin + from∘f₁≈f₁ : from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈ f₁ (compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′)) + from∘f₁≈f₁ = begin from ≅N ∘ (f₁ (compose A⇒B B⇒C) +₁ f₁ (compose A⇒B′ B⇒C′)) ≈⟨ Equiv.refl ⟩ from ≅N ∘ ((i₁ P₁ ∘ f₁ A⇒B) +₁ (i₁ P₂ ∘ f₁ A⇒B′)) ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨ from ≅N ∘ (i₁ P₁ +₁ i₁ P₂) ∘ (f₁ A⇒B +₁ f₁ A⇒B′) ≈⟨ Equiv.refl ⟩ - from ≅N ∘ i₁ P₃′ ∘ f₁ (together A⇒B A⇒B′) ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩ - i₁ P₃ ∘ f₁ (together A⇒B A⇒B′) ∎ - from∘f₂≈f₂′ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (together A⇒B A⇒B′) (together B⇒C B⇒C′)) - from∘f₂≈f₂′ = begin + from ≅N ∘ i₁ P₃′ ∘ f₁ (A⇒B ⊗ A⇒B′) ≈⟨ pullˡ (universal∘i₁≈h₁ P₃′) ⟩ + i₁ P₃ ∘ f₁ (A⇒B ⊗ A⇒B′) ∎ + from∘f₂≈f₂ : from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈ f₂ (compose (A⇒B ⊗ A⇒B′) (B⇒C ⊗ B⇒C′)) + from∘f₂≈f₂ = begin from ≅N ∘ (f₂ (compose A⇒B B⇒C) +₁ f₂ (compose A⇒B′ B⇒C′)) ≈⟨ Equiv.refl ⟩ from ≅N ∘ ((i₂ P₁ ∘ f₂ B⇒C) +₁ (i₂ P₂ ∘ f₂ B⇒C′)) ≈⟨ refl⟩∘⟨ +₁∘+₁ ⟨ from ≅N ∘ (i₂ P₁ +₁ i₂ P₂) ∘ (f₂ B⇒C +₁ f₂ B⇒C′) ≈⟨ Equiv.refl ⟩ - from ≅N ∘ i₂ P₃′ ∘ f₂ (together B⇒C B⇒C′) ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩ - i₂ P₃ ∘ f₂ (together B⇒C B⇒C′) ∎ + from ≅N ∘ i₂ P₃′ ∘ f₂ (B⇒C ⊗ B⇒C′) ≈⟨ pullˡ (universal∘i₂≈h₂ P₃′) ⟩ + i₂ P₃ ∘ f₂ (B⇒C ⊗ B⇒C′) ∎ ⊗-resp-≈ : {A A′ B B′ : Obj} {f f′ : Cospan A B} {g g′ : Cospan A′ B′} - → Same f f′ - → Same g g′ - → Same (together f g) (together f′ g′) + → f Cospan.≈ f′ + → g Cospan.≈ g′ + → f ⊗ g Cospan.≈ f′ ⊗ g′ ⊗-resp-≈ {_} {_} {_} {_} {f} {f′} {g} {g′} ≈f ≈g = record { ≅N = ≈f.≅N ⊗ᵢ ≈g.≅N - ; from∘f₁≈f₁′ = from∘f₁≈f₁′ - ; from∘f₂≈f₂′ = from∘f₂≈f₂′ + ; from∘f₁≈f₁ = from∘f₁≈f₁ + ; from∘f₂≈f₂ = from∘f₂≈f₂ } where open 𝒞 using (-+-) - module ≈f = Same ≈f - module ≈g = Same ≈g + module ≈f = Cospan._≈_ ≈f + module ≈g = Cospan._≈_ ≈g open HomReasoning - open Cospan + open Cospan.Cospan open 𝒞 using (+₁-cong₂; +₁∘+₁) - from∘f₁≈f₁′ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′ - from∘f₁≈f₁′ = begin + from∘f₁≈f₁ : (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈ f₁ f′ +₁ f₁ g′ + from∘f₁≈f₁ = begin (≈f.from +₁ ≈g.from) ∘ (f₁ f +₁ f₁ g) ≈⟨ +₁∘+₁ ⟩ - (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g) ≈⟨ +₁-cong₂ (≈f.from∘f₁≈f₁′) (≈g.from∘f₁≈f₁′) ⟩ + (≈f.from ∘ f₁ f) +₁ (≈g.from ∘ f₁ g) ≈⟨ +₁-cong₂ ≈f.from∘f₁≈f₁ ≈g.from∘f₁≈f₁ ⟩ f₁ f′ +₁ f₁ g′ ∎ - from∘f₂≈f₂′ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′ - from∘f₂≈f₂′ = begin + from∘f₂≈f₂ : (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈ f₂ f′ +₁ f₂ g′ + from∘f₂≈f₂ = begin (≈f.from +₁ ≈g.from) ∘ (f₂ f +₁ f₂ g) ≈⟨ +₁∘+₁ ⟩ - (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g) ≈⟨ +₁-cong₂ (≈f.from∘f₂≈f₂′) (≈g.from∘f₂≈f₂′) ⟩ + (≈f.from ∘ f₂ f) +₁ (≈g.from ∘ f₂ g) ≈⟨ +₁-cong₂ ≈f.from∘f₂≈f₂ ≈g.from∘f₂≈f₂ ⟩ f₂ f′ +₁ f₂ g′ ∎ +private + ⊗′ : Bifunctor Cospans Cospans Cospans + ⊗′ = record + { F₀ = λ (A , A′) → A + A′ + ; F₁ = λ (f , g) → f ⊗ g + ; identity = λ { {x , y} → id⊗id≈id {x} {y} } + ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } + ; F-resp-≈ = λ (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g + } + ⊗ : Bifunctor Cospans Cospans Cospans -⊗ = record - { F₀ = λ { (A , A′) → A + A′ } - ; F₁ = λ { (f , g) → together f g } - ; identity = λ { {x , y} → id⊗id≈id {x} {y} } - ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } - ; F-resp-≈ = λ { (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g } - } +⊗ = ⊗′ + +module ⊗ = Functor ⊗ diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda new file mode 100644 index 0000000..fedddba --- /dev/null +++ b/Functor/Instance/Decorate.agda @@ -0,0 +1,165 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} + +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Data.Product.Base using (_,_) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module Functor.Instance.Decorate + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Category.Diagram.Cospan 𝒞 as Cospan + +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Functor.Core using (Functor) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Function.Base using () renaming (id to idf) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) +open import Functor.Instance.Cospan.Stack 𝒞 using (module ⊗) +open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using () renaming (module ⊗ to ⊗′) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 +module F = SymmetricMonoidalFunctor F +module Cospans = Category Cospans +module DecoratedCospans = Category DecoratedCospans +module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian + +-- For every cospan there exists a free decorated cospan +-- i.e. the original cospan with the discrete decoration + +private + variable + A A′ B B′ C C′ D : 𝒞.Obj + f : Cospans [ A , B ] + g : Cospans [ C , D ] + +decorate : Cospans [ A , B ] → DecoratedCospans [ A , B ] +decorate f = record + { cospan = f + ; decoration = F₁ ¡ ∘ ε + } + where + open 𝒞 using (¡) + open 𝒟 using (_∘_) + open F using (ε; F₁) + +identity : DecoratedCospans [ decorate (Cospans.id {A}) ≈ DecoratedCospans.id ] +identity = record + { cospans-≈ = Cospans.Equiv.refl + ; same-deco = elimˡ F.identity + } + where + open ⇒-Reasoning 𝒟.U + +homomorphism : DecoratedCospans [ decorate (Cospans [ g ∘ f ]) ≈ DecoratedCospans [ decorate g ∘ decorate f ] ] +homomorphism {g} {f} = record + { cospans-≈ = Cospans.Equiv.refl + ; same-deco = same-deco + } + where + + open Cospan.Cospan f using (N; f₂) + open Cospan.Cospan g using () renaming (N to M; f₁ to g₁) + + open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + + open DiagramPushout 𝒞.U using (Pushout) + open Pushout (pushout f₂ g₁) using (i₁; i₂) + open mc𝒞 using (unitorˡ) + open unitorˡ using () renaming (to to λ⇐′) + + same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ F.ε ≈ F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ + same-deco = begin + F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈⟨ elimˡ F.identity ⟩ + F₁ ¡ ∘ ε ≈⟨ F.F-resp-≈ (¡-unique _) ⟩∘⟨refl ⟩ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ≈⟨ refl⟩∘⟨ introʳ λ-.isoʳ ⟩ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ + F₁ ([ i₁ , i₂ ]′ 𝒞.∘ ¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ F.homomorphism ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ push-center F.homomorphism ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩ + F₁ [ i₁ , i₂ ]′ ∘ F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , ¡)) ⟨ + F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ + F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ∎ + +F-resp-≈ : Cospans [ f ≈ g ] → DecoratedCospans [ decorate f ≈ decorate g ] +F-resp-≈ f≈g = record + { cospans-≈ = f≈g + ; same-deco = pullˡ (sym F.homomorphism) ○ sym (F.F-resp-≈ (¡-unique _)) ⟩∘⟨refl + } + where + open ⇒-Reasoning 𝒟.U + open 𝒟.Equiv + open 𝒟.HomReasoning + open 𝒞 using (¡-unique) + +Decorate : Functor Cospans DecoratedCospans +Decorate = record + { F₀ = idf + ; F₁ = decorate + ; identity = identity + ; homomorphism = homomorphism + ; F-resp-≈ = F-resp-≈ + } + +Decorate-resp-⊗ : DecoratedCospans [ decorate (⊗.₁ (f , g)) ≈ ⊗′.₁ (decorate f , decorate g) ] +Decorate-resp-⊗ {f} {g} = record + { cospans-≈ = Cospan.≈-refl + ; same-deco = same-deco + } + where + + open Cospan.Cospan f using (N) + open Cospan.Cospan g using () renaming (N to M) + + open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + open mc𝒞 using (unitorˡ) + open unitorˡ using () renaming (to to λ⇐′) + + same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ + same-deco = begin + F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈⟨ elimˡ F.identity ⟩ + F₁ ¡ ∘ ε ≈⟨ F.F-resp-≈ (¡-unique _) ⟩∘⟨refl ⟩ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ≈⟨ refl⟩∘⟨ introʳ λ-.isoʳ ⟩ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟩ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ ε ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟨ + F₁ (¡ +₁ ¡ 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ pushˡ F.homomorphism ⟩ + F₁ (¡ +₁ ¡) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟨ + F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ id ∘ id ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym serialize₁₂) ⟩ + F₁ (¡ +₁ ¡) ∘ φ (⊥ , ⊥) ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ extendʳ (φ-commute (¡ , ¡)) ⟨ + φ (N , M) ∘ F₁ ¡ ⊗₁ F₁ ¡ ∘ ε ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) ⟩ + φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ∎ diff --git a/Functor/Instance/DecoratedCospan/Embed.agda b/Functor/Instance/DecoratedCospan/Embed.agda new file mode 100644 index 0000000..77b16fa --- /dev/null +++ b/Functor/Instance/DecoratedCospan/Embed.agda @@ -0,0 +1,275 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory; SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module Functor.Instance.DecoratedCospan.Embed + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Category.Diagram.Pushout as Pushout′ +import Category.Diagram.Cospan as Cospan +import Functor.Instance.Cospan.Embed 𝒞 as Embed + +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) + +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Diagram.Pushout.Properties as PushoutProperties +import Categories.Morphism as Morphism + +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Functor using (Functor; _∘F_) +open import Data.Product using (_,_) +open import Function using () renaming (id to idf) +open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using (⊗) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 +module F = SymmetricMonoidalFunctor F +module Cospans = Category Cospans +module DecoratedCospans = Category DecoratedCospans +module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian + +open import Functor.Instance.Decorate 𝒞 F using (Decorate; Decorate-resp-⊗) + +private + variable + A B C D E H : 𝒞.Obj + f : 𝒞.U [ A , B ] + g : 𝒞.U [ C , D ] + h : 𝒞.U [ E , H ] + +L : Functor 𝒞.U DecoratedCospans +L = Decorate ∘F Embed.L + +R : Functor 𝒞.op DecoratedCospans +R = Decorate ∘F Embed.R + +B₁ : 𝒞.U [ A , C ] → 𝒞.U [ B , C ] → 𝒟.U [ 𝒟.unit , F.F₀ C ] → DecoratedCospans [ A , B ] +B₁ f g s = record + { cospan = Cospan.cospan f g + ; decoration = s + } + +module _ where + + module L = Functor L + module R = Functor R + + module Codiagonal where + + open mc𝒞 using (unitorˡ; unitorʳ; +-monoidal) public + open unitorˡ using () renaming (to to λ⇐′) public + open unitorʳ using () renaming (to to ρ⇐′) public + open 𝒞 using (U; _+_; []-cong₂; []∘+₁; ∘-distribˡ-[]; inject₁; inject₂; ¡) + renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open HomReasoning + open ⇒-Reasoning 𝒞.U + + μ : {X : Obj} → X + X ⇒ X + μ = [ id , id ]′ + + μ∘+ : {X Y Z : Obj} {f : X ⇒ Z} {g : Y ⇒ Z} → [ f , g ]′ ≈ μ ∘ f +₁ g + μ∘+ = []-cong₂ (sym identityˡ) (sym identityˡ) ○ sym []∘+₁ + + μ∘¡ˡ : {X : Obj} → μ ∘ ¡ +₁ id ∘ λ⇐′ ≈ id {X} + μ∘¡ˡ = begin + μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩ + [ ¡ , id ]′ ∘ λ⇐′ ≈⟨ inject₂ ⟩ + id ∎ + + μ∘¡ʳ : {X : Obj} → μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈ id {X} + μ∘¡ʳ = begin + μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ pullˡ (sym μ∘+) ⟩ + [ id , ¡ ]′ ∘ ρ⇐′ ≈⟨ inject₁ ⟩ + id ∎ + + + μ-natural : {X Y : Obj} {f : X ⇒ Y} → f ∘ μ ≈ μ ∘ f +₁ f + μ-natural = ∘-distribˡ-[] ○ []-cong₂ (identityʳ ○ sym identityˡ) (identityʳ ○ sym identityˡ) ○ sym []∘+₁ + + B∘L : {A B M C : 𝒞.Obj} + → {f : 𝒞.U [ A , B ]} + → {g : 𝒞.U [ B , M ]} + → {h : 𝒞.U [ C , M ]} + → {s : 𝒟.U [ 𝒟.unit , F.₀ M ]} + → DecoratedCospans [ DecoratedCospans [ B₁ g h s ∘ L.₁ f ] ≈ B₁ (𝒞.U [ g ∘ f ]) h s ] + B∘L {A} {B} {M} {C} {f} {g} {h} {s} = record + { cospans-≈ = Embed.B∘L + ; same-deco = same-deco + } + where + + module _ where + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open 𝒞 using (U) + open Category U + open mc𝒞 using (unitorˡ; unitorˡ-commute-to; +-monoidal) public + open unitorˡ using () renaming (to to λ⇐′) public + open ⊗-Reasoning +-monoidal + open ⇒-Reasoning 𝒞.U + open Equiv + + open Pushout′ 𝒞.U using (pushout-id-g) + open PushoutProperties 𝒞.U using (up-to-iso) + open DiagramPushout 𝒞.U using (Pushout) + P P′ : Pushout 𝒞.id g + P = pushout 𝒞.id g + P′ = pushout-id-g + module P = Pushout P + module P′ = Pushout P′ + open Morphism 𝒞.U using (_≅_) + open _≅_ using (from) + open P using (i₁ ; i₂; universal∘i₂≈h₂) public + + open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ˡ) + + ≅ : P.Q ⇒ M + ≅ = up-to-iso P P′ .from + + ≅∘[]∘¡+id : ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈ id + ≅∘[]∘¡+id = begin + ((≅ ∘ [ i₁ , i₂ ]′) ∘ ¡ +₁ id) ∘ λ⇐′ ≈⟨ assoc²αε ⟩ + ≅ ∘ [ i₁ , i₂ ]′ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩ + ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ refl⟩∘⟨ pull-center (sym split₁ʳ) ⟩ + ≅ ∘ μ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′ ≈⟨ extendʳ μ-natural ⟩ + μ ∘ ≅ +₁ ≅ ∘ (i₁ ∘ ¡) +₁ i₂ ∘ λ⇐′ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩ + μ ∘ (≅ ∘ i₁ ∘ ¡) +₁ (≅ ∘ i₂) ∘ λ⇐′ ≈⟨ refl⟩∘⟨ sym (¡-unique (≅ ∘ i₁ ∘ ¡)) ⟩⊗⟨ universal∘i₂≈h₂ ⟩∘⟨refl ⟩ + μ ∘ ¡ +₁ id ∘ λ⇐′ ≈⟨ μ∘¡ˡ ⟩ + id ∎ + + open 𝒟 using (U; monoidal; _⊗₁_; unitorˡ-commute-from) renaming (module unitorˡ to λ-) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + + same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈ s + same-deco = begin + F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ id ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym F.identity ⟩∘⟨refl ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (B , M) ∘ F₁ ¡ ⊗₁ F₁ 𝒞.id ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (¡ , 𝒞.id)) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ φ (⊥ , M) ∘ ε ⊗₁ id ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorˡ) F.unitaryˡ) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) ∘ F₁ λ⇐′ ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ λ⇒ ∘ id ⊗₁ s ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorˡ-commute-from ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ monoidal ⟨ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ∘ λ⇒ ∘ λ⇐ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ λ-.isoʳ) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ ¡ +₁ 𝒞.id) 𝒞.∘ λ⇐′) ∘ s ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘¡+id ○ F.identity) ⟩ + s ∎ + + R∘B : {A N B C : 𝒞.Obj} + → {f : 𝒞.U [ A , N ]} + → {g : 𝒞.U [ B , N ]} + → {h : 𝒞.U [ C , B ]} + → {s : 𝒟.U [ 𝒟.unit , F.₀ N ]} + → DecoratedCospans [ DecoratedCospans [ R.₁ h ∘ B₁ f g s ] ≈ B₁ f (𝒞.U [ g ∘ h ]) s ] + R∘B {A} {N} {B} {C} {f} {g} {h} {s} = record + { cospans-≈ = Embed.R∘B + ; same-deco = same-deco + } + where + + module _ where + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open 𝒞 using (U) + open Category U + open mc𝒞 using (unitorʳ; unitorˡ; unitorˡ-commute-to; +-monoidal) public + open unitorˡ using () renaming (to to λ⇐′) public + open unitorʳ using () renaming (to to ρ⇐′) public + open ⊗-Reasoning +-monoidal + open ⇒-Reasoning 𝒞.U + open Equiv + + open Pushout′ 𝒞.U using (pushout-f-id) + open PushoutProperties 𝒞.U using (up-to-iso) + open DiagramPushout 𝒞.U using (Pushout) + P P′ : Pushout g 𝒞.id + P = pushout g 𝒞.id + P′ = pushout-f-id + module P = Pushout P + module P′ = Pushout P′ + open Morphism 𝒞.U using (_≅_) + open _≅_ using (from) + open P using (i₁ ; i₂; universal∘i₁≈h₁) public + + open Codiagonal using (μ; μ-natural; μ∘+; μ∘¡ʳ) + + ≅ : P.Q ⇒ N + ≅ = up-to-iso P P′ .from + + ≅∘[]∘id+¡ : ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈ id + ≅∘[]∘id+¡ = begin + ((≅ ∘ [ i₁ , i₂ ]′) ∘ id +₁ ¡) ∘ ρ⇐′ ≈⟨ assoc²αε ⟩ + ≅ ∘ [ i₁ , i₂ ]′ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ pushˡ μ∘+ ⟩ + ≅ ∘ μ ∘ i₁ +₁ i₂ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ pull-center merge₂ʳ ⟩ + ≅ ∘ μ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ extendʳ μ-natural ⟩ + μ ∘ ≅ +₁ ≅ ∘ i₁ +₁ (i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩ + μ ∘ (≅ ∘ i₁) +₁ (≅ ∘ i₂ ∘ ¡) ∘ ρ⇐′ ≈⟨ refl⟩∘⟨ universal∘i₁≈h₁ ⟩⊗⟨ sym (¡-unique (≅ ∘ i₂ ∘ ¡)) ⟩∘⟨refl ⟩ + μ ∘ id +₁ ¡ ∘ ρ⇐′ ≈⟨ μ∘¡ʳ ⟩ + id ∎ + + open 𝒟 using (U; monoidal; _⊗₁_; unitorʳ-commute-from) renaming (module unitorˡ to λ-; module unitorʳ to ρ) + open 𝒞 using (¡; ⊥; ¡-unique; pushout) renaming ([_,_] to [_,_]′; _+₁_ to infixr 10 _+₁_ ) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁; ε) + open Shorthands monoidal + + same-deco : F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈ s + same-deco = begin + F₁ ≅ ∘ F₁ [ i₁ , i₂ ]′ ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ s ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym F.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ φ (N , B) ∘ F₁ 𝒞.id ⊗₁ F₁ ¡ ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (φ-commute (𝒞.id , ¡)) ⟩ + F₁ (≅ 𝒞.∘ [ i₁ , i₂ ]′) ∘ F₁ (𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ s ⊗₁ ε ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ φ (N , ⊥) ∘ id ⊗₁ ε ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ unitorʳ) F.unitaryʳ) ⟩ + F₁ ((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) ∘ F₁ ρ⇐′ ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ ρ⇒ ∘ s ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ extendʳ unitorʳ-commute-from ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ∘ ρ⇒ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ (sym-assoc ○ cancelʳ ρ.isoʳ) ⟩ + F₁ (((≅ 𝒞.∘ [ i₁ , i₂ ]′) 𝒞.∘ 𝒞.id +₁ ¡) 𝒞.∘ ρ⇐′) ∘ s ≈⟨ elimˡ (F.F-resp-≈ ≅∘[]∘id+¡ ○ F.identity) ⟩ + s ∎ + + open Morphism 𝒞.U using (_≅_) + open _≅_ + + ≅-L-R : (X≅Y : A ≅ B) → DecoratedCospans [ L.₁ (to X≅Y) ≈ R.₁ (from X≅Y) ] + ≅-L-R X≅Y = Decorate.F-resp-≈ (Embed.≅-L-R X≅Y) + where + module Decorate = Functor Decorate + + open 𝒞 using (_+₁_) + + L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ] + L-resp-⊗ = Decorate.F-resp-≈ Embed.L-resp-⊗ ○ Decorate-resp-⊗ + where + module Decorate = Functor Decorate + open DecoratedCospans.HomReasoning diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda new file mode 100644 index 0000000..381ee06 --- /dev/null +++ b/Functor/Instance/DecoratedCospan/Stack.agda @@ -0,0 +1,430 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) + +open Lax using (SymmetricMonoidalFunctor) +open FinitelyCocompleteCategory + using () + renaming (symmetricMonoidalCategory to smc) + +module Functor.Instance.DecoratedCospan.Stack + {o o′ ℓ ℓ′ e e′} + (𝒞 : FinitelyCocompleteCategory o ℓ e) + {𝒟 : SymmetricMonoidalCategory o′ ℓ′ e′} + (F : SymmetricMonoidalFunctor (smc 𝒞) 𝒟) where + +import Categories.Diagram.Pushout as DiagramPushout +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning + +import Functor.Instance.Cospan.Stack 𝒞 as Stack + +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.BinaryProducts using (BinaryProducts) +open import Categories.Category.Monoidal.Utilities using (module Shorthands) +open import Categories.Category.Monoidal.Properties using (coherence-inv₃) +open import Categories.Category.Monoidal.Braided.Properties using (braiding-coherence-inv) +open import Categories.Functor using (Functor) +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.Functor.Properties using ([_]-resp-≅) +open import Categories.Category.Cocartesian using (module CocartesianMonoidal; module CocartesianSymmetricMonoidal) +open import Categories.Object.Initial using (Initial) +open import Categories.Object.Duality using (Coproduct⇒coProduct) +open import Category.Instance.DecoratedCospans 𝒞 F using () renaming (DecoratedCospans to Cospans; _≈_ to _≈_′) + +import Category.Diagram.Cospan 𝒞 as Cospan + +open import Cospan.Decorated 𝒞 F using (DecoratedCospan) +open import Data.Product.Base using (_,_) + +module 𝒞 = FinitelyCocompleteCategory 𝒞 +module 𝒟 = SymmetricMonoidalCategory 𝒟 +module F = SymmetricMonoidalFunctor F +module Cospans = Category Cospans + +open 𝒞 using (Obj; _+_; cocartesian) + +module mc𝒞 = CocartesianMonoidal 𝒞.U cocartesian +module smc𝒞 = CocartesianSymmetricMonoidal 𝒞.U cocartesian + +open DiagramPushout 𝒞.U using (Pushout) + +private + variable + A A′ B B′ C C′ : Obj + +together : Cospans [ A , B ] → Cospans [ A′ , B′ ] → Cospans [ A + A′ , B + B′ ] +together A⇒B A⇒B′ = record + { cospan = A⇒B.cospan Cospan.⊗ A⇒B′.cospan + ; decoration = ⊗-homo.η (A⇒B.N , A⇒B′.N) ∘ A⇒B.decoration ⊗₁ A⇒B′.decoration ∘ unitorʳ.to + } + where + module A⇒B = DecoratedCospan A⇒B + module A⇒B′ = DecoratedCospan A⇒B′ + open 𝒟 using (_∘_; _⊗₁_; module unitorʳ) + open F using (module ⊗-homo) + +id⊗id≈id : Cospans [ together (Cospans.id {A}) (Cospans.id {B}) ≈ Cospans.id ] +id⊗id≈id {A} {B} = record + { cospans-≈ = Stack.id⊗id≈id + ; same-deco = F.identity ⟩∘⟨refl + ○ identityˡ + ○ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩∘⟨refl + ○ extendʳ (extendʳ (⊗-homo.commute (! , !))) + ○ refl⟩∘⟨ pullʳ (pushˡ serialize₂₁ ○ refl⟩∘⟨ sym unitorʳ-commute-to) + ○ pushˡ (F-resp-≈ !+!≈! ○ homomorphism) + ○ refl⟩∘⟨ (refl⟩∘⟨ sym-assoc ○ pullˡ unitaryʳ ○ cancelˡ unitorʳ.isoʳ) + } + where + open 𝒞 using (_+₁_; ¡-unique) + open 𝒟 using (identityˡ; U; monoidal; module unitorʳ; unitorʳ-commute-to; assoc; sym-assoc) + open 𝒟.Equiv + open ⇒-Reasoning U + open ⇒-Reasoning 𝒞.U using () renaming (flip-iso to flip-iso′) + open ⊗-Reasoning monoidal + open F using (module ⊗-homo; F-resp-≈; homomorphism; unitaryʳ) + open 𝒞 using (initial) + open Initial initial using (!; !-unique₂) + open Morphism using (_≅_; module ≅) + open mc𝒞 using (A+⊥≅A) + module A+⊥≅A = _≅_ A+⊥≅A + !+!≈! : 𝒞.U [ (! {A} +₁ ! {B}) ≈ ! {A + B} 𝒞.∘ A+⊥≅A.from ] + !+!≈! = 𝒞.Equiv.sym (flip-iso′ (≅.sym 𝒞.U A+⊥≅A) (¡-unique ((! +₁ !) 𝒞.∘ A+⊥≅A.to))) + +homomorphism + : (A⇒B : Cospans [ A , B ]) + → (B⇒C : Cospans [ B , C ]) + → (A⇒B′ : Cospans [ A′ , B′ ]) + → (B⇒C′ : Cospans [ B′ , C′ ]) + → Cospans + [ together (Cospans [ B⇒C ∘ A⇒B ]) (Cospans [ B⇒C′ ∘ A⇒B′ ]) + ≈ Cospans [ together B⇒C B⇒C′ ∘ together A⇒B A⇒B′ ] + ] +homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record + { cospans-≈ = cospans-≈ + ; same-deco = same-deco + } + where + + module _ where + open DecoratedCospan using (cospan) + cospans-≈ : _ Cospan.⊗ _ Cospan.≈ Cospan.compose (_ Cospan.⊗ _) (_ Cospan.⊗ _) + cospans-≈ = Stack.homomorphism (f .cospan) (g .cospan) (f′ .cospan) (g′ .cospan) + open Cospan._≈_ cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public + + module DecorationNames where + open DecoratedCospan f using (N) renaming (decoration to s) public + open DecoratedCospan g using () renaming (decoration to t; N to M) public + open DecoratedCospan f′ using () renaming (decoration to s′; N to N′) public + open DecoratedCospan g′ using () renaming (decoration to t′; N to M′) public + + module PushoutNames where + open DecoratedCospan using (f₁; f₂) + open 𝒞 using (pushout) + open Pushout (pushout (f .f₂) (g .f₁)) using (i₁; i₂; Q) public + open Pushout (pushout (f′ .f₂) (g′ .f₁)) using () renaming (i₁ to i₁′; i₂ to i₂′; Q to Q′) public + open Pushout (pushout (together f f′ .f₂) (together g g′ .f₁)) + using (universal∘i₁≈h₁; universal∘i₂≈h₂) + renaming (i₁ to i₁″; i₂ to i₂″; Q to Q″) public + + module _ where + + open DecorationNames + open PushoutNames + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + + open 𝒞 using () renaming ([_,_] to [_,_]′) + + module _ where + + open 𝒞 + using (U; +-swap; inject₁; inject₂; +-η) + renaming (i₁ to ι₁; i₂ to ι₂; _+₁_ to infixr 10 _+₁_) + open Category U hiding (Obj) + open Equiv + open Shorthands mc𝒞.+-monoidal + open ⊗-Reasoning mc𝒞.+-monoidal + open ⇒-Reasoning U + open mc𝒞 using (assoc-commute-from; assoc-commute-to; module ⊗; associator) + open smc𝒞 using () renaming (module braiding to σ) + + module Codiagonal where + + open 𝒞 using (coproduct; +-unique; []-cong₂; []∘+₁; ∘-distribˡ-[]) + μ : {X : Obj} → X + X ⇒ X + μ = [ id , id ]′ + + μ∘+ : {X Y Z : Obj} {f : X ⇒ Z} {g : Y ⇒ Z} → [ f , g ]′ ≈ μ ∘ f +₁ g + μ∘+ = []-cong₂ (sym identityˡ) (sym identityˡ) ○ sym []∘+₁ + + μ∘σ : {X : Obj} → μ ∘ +-swap ≈ μ {X} + μ∘σ = sym (+-unique (pullʳ inject₁ ○ inject₂) (pullʳ inject₂ ○ inject₁) ) + + op-binaryProducts : BinaryProducts op + op-binaryProducts = record { product = Coproduct⇒coProduct U coproduct } + + module op-binaryProducts = BinaryProducts op-binaryProducts + open op-binaryProducts using () renaming (assocʳ∘⟨⟩ to []∘assocˡ) + + μ-assoc : {X : Obj} → μ {X} ∘ μ +₁ (id {X}) ≈ μ ∘ (id {X}) +₁ μ ∘ α⇒ + μ-assoc = begin + μ ∘ μ +₁ id ≈⟨ μ∘+ ⟨ + [ [ id , id ]′ , id ]′ ≈⟨ []∘assocˡ ⟨ + [ id , [ id , id ]′ ]′ ∘ α⇒ ≈⟨ pushˡ μ∘+ ⟩ + μ ∘ id +₁ μ ∘ α⇒ ∎ + + μ-natural : {X Y : Obj} {f : X ⇒ Y} → f ∘ μ ≈ μ ∘ f +₁ f + μ-natural = ∘-distribˡ-[] ○ []-cong₂ (identityʳ ○ sym identityˡ) (identityʳ ○ sym identityˡ) ○ sym []∘+₁ + + open Codiagonal + + ≅ : Q + Q′ ⇒ Q″ + ≅ = Q+Q′≅Q″.from + + ≅∘[]+[]≈μ∘μ+μ : ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′ ≈ (μ ∘ (μ +₁ μ)) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) + ≅∘[]+[]≈μ∘μ+μ = begin + ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′ ≈⟨ refl⟩∘⟨ μ∘+ ⟩⊗⟨ μ∘+ ⟩ + ≅ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ introˡ +-η ⟩ + ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ push-center μ∘+ ⟩ + ≅ ∘ μ ∘ (ι₁ +₁ ι₂) ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym ⊗-distrib-over-∘ ⟩ + ≅ ∘ μ ∘ (ι₁ ∘ μ ∘ i₁ +₁ i₂) +₁ (ι₂ ∘ μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (extendʳ μ-natural) ⟩⊗⟨ (extendʳ μ-natural) ⟩ + ≅ ∘ μ ∘ (μ ∘ ι₁ +₁ ι₁ ∘ i₁ +₁ i₂) +₁ (μ ∘ ι₂ +₁ ι₂ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩⊗⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩ + ≅ ∘ μ ∘ (μ ∘ (ι₁ ∘ i₁) +₁ (ι₁ ∘ i₂)) +₁ (μ ∘ (ι₂ ∘ i₁′) +₁ (ι₂ ∘ i₂′)) ≈⟨ extendʳ μ-natural ⟩ + μ ∘ ≅ +₁ ≅ ∘ (μ ∘ _) +₁ (μ ∘ _) ≈⟨ refl⟩∘⟨ sym ⊗-distrib-over-∘ ⟩ + μ ∘ (≅ ∘ μ ∘ _) +₁ (≅ ∘ μ ∘ _) ≈⟨ refl⟩∘⟨ extendʳ μ-natural ⟩⊗⟨ extendʳ μ-natural ⟩ + μ ∘ (μ ∘ ≅ +₁ ≅ ∘ _) +₁ (μ ∘ ≅ +₁ ≅ ∘ _) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩⊗⟨ (refl⟩∘⟨ sym ⊗-distrib-over-∘) ⟩ + μ ∘ (μ ∘ (≅ ∘ ι₁ ∘ i₁) +₁ (≅ ∘ ι₁ ∘ i₂)) +₁ (μ ∘ (≅ ∘ ι₂ ∘ i₁′) +₁ (≅ ∘ ι₂ ∘ i₂′)) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ eq₁ ⟩⊗⟨ eq₂ ) ⟩⊗⟨ (refl⟩∘⟨ eq₃ ⟩⊗⟨ eq₄ ) ⟩ + μ ∘ (μ ∘ (i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ (μ ∘ (i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩ + μ ∘ (μ +₁ μ) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ≈⟨ sym-assoc ⟩ + (μ ∘ (μ +₁ μ)) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ∎ + where + eq₁ : ≅ ∘ ι₁ ∘ i₁ ≈ i₁″ ∘ ι₁ + eq₁ = refl⟩∘⟨ sym inject₁ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₁≈h₁)) + eq₂ : ≅ ∘ ι₁ ∘ i₂ ≈ i₂″ ∘ ι₁ + eq₂ = refl⟩∘⟨ sym inject₁ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₂≈h₂)) + eq₃ : ≅ ∘ ι₂ ∘ i₁′ ≈ i₁″ ∘ ι₂ + eq₃ = refl⟩∘⟨ sym inject₂ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₁≈h₁)) + eq₄ : ≅ ∘ ι₂ ∘ i₂′ ≈ i₂″ ∘ ι₂ + eq₄ = refl⟩∘⟨ sym inject₂ ○ pullˡ (sym (switch-tofromˡ Q+Q′≅Q″ universal∘i₂≈h₂)) + + swap-inner : {W X Y Z : Obj} → (W + X) + (Y + Z) ⇒ (W + Y) + (X + Z) + swap-inner = α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ + + swap-inner-natural + : {W X Y Z W′ X′ Y′ Z′ : Obj} + {w : W ⇒ W′} {x : X ⇒ X′} {y : Y ⇒ Y′} {z : Z ⇒ Z′} + → (w +₁ x) +₁ (y +₁ z) ∘ swap-inner + ≈ swap-inner ∘ (w +₁ y) +₁ (x +₁ z) + swap-inner-natural {w = w} {x = x} {y = y} {z = z} = begin + (w +₁ x) +₁ (y +₁ z) ∘ α⇐ ∘ _ ≈⟨ extendʳ assoc-commute-to ⟨ + α⇐ ∘ w +₁ (x +₁ _) ∘ id +₁ _ ∘ α⇒ ≈⟨ pull-center merge₂ʳ ⟩ + α⇐ ∘ w +₁ (x +₁ _ ∘ α⇒ ∘ _) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ assoc-commute-from ⟩∘⟨refl ⟨ + α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y) +₁ z ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ pushˡ split₁ʳ) ⟩∘⟨refl ⟨ + α⇐ ∘ w +₁ (α⇒ ∘ (x +₁ y ∘ +-swap) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ σ.⇒.sym-commute _ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩ + α⇐ ∘ w +₁ (α⇒ ∘ (+-swap ∘ y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ push-center split₁ˡ ⟩∘⟨refl ⟩ + α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ (y +₁ x) +₁ z ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ refl⟩∘⟨ assoc-commute-to) ⟩∘⟨refl ⟨ + α⇐ ∘ w +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐ ∘ y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc²εβ ⟩∘⟨refl ⟩ + α⇐ ∘ w +₁ ((α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ w +₁ (y +₁ (x +₁ z)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟨ + α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ∘ (w +₁ y) +₁ (x +₁ z) ≈⟨ assoc²εβ ⟩ + swap-inner ∘ (w +₁ y) +₁ (x +₁ z) ∎ + + μ∘μ+μ∘swap-inner : {X : Obj} → μ {X} ∘ μ +₁ μ ∘ swap-inner ≈ μ ∘ μ +₁ μ {X} + μ∘μ+μ∘swap-inner = begin + μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ push-center serialize₁₂ ⟩ + μ ∘ μ +₁ id ∘ id +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟨ + μ ∘ μ +₁ id ∘ (id +₁ id) +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-to ⟨ + μ ∘ μ +₁ id ∘ α⇐ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ pullˡ μ-assoc ⟩ + (μ ∘ id +₁ μ ∘ α⇒) ∘ α⇐ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ extendʳ (pullʳ (cancelʳ associator.isoʳ)) ⟩ + μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ) ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ pull-center merge₂ˡ ⟩ + μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ ∘ α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ pull-center merge₂ʳ ⟩ + μ ∘ id +₁ (μ ∘ id +₁ μ ∘ α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pull-center refl ⟩∘⟨refl ⟩ + μ ∘ id +₁ (μ ∘ (id +₁ μ ∘ α⇒) ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ extendʳ μ-assoc ⟩∘⟨refl ⟨ + μ ∘ id +₁ (μ ∘ μ +₁ id ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ pull-center (sym split₁ˡ) ⟩∘⟨refl ⟩ + μ ∘ id +₁ (μ ∘ (μ ∘ +-swap) +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ μ∘σ ⟩⊗⟨refl ⟩∘⟨refl) ⟩∘⟨refl ⟩ + μ ∘ id +₁ (μ ∘ μ +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (sym-assoc ○ flip-iso associator (μ-assoc ○ sym-assoc)) ⟩∘⟨refl ⟩ + μ ∘ id +₁ (μ ∘ id +₁ μ) ∘ α⇒ ≈⟨ push-center split₂ʳ ⟩ + μ ∘ id +₁ μ ∘ id +₁ (id +₁ μ) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟨ + μ ∘ id +₁ μ ∘ α⇒ ∘ (id +₁ id) +₁ μ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩ + μ ∘ id +₁ μ ∘ α⇒ ∘ id +₁ μ ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + μ ∘ (id +₁ μ ∘ α⇒) ∘ id +₁ μ ≈⟨ extendʳ μ-assoc ⟨ + μ ∘ μ +₁ id ∘ id +₁ μ ≈⟨ refl⟩∘⟨ serialize₁₂ ⟨ + μ ∘ μ +₁ μ ∎ + + ≅∘[]+[]∘σ₄ : (Q+Q′≅Q″.from ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′) ∘ swap-inner ≈ [ i₁″ , i₂″ ]′ + ≅∘[]+[]∘σ₄ = begin + (≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′) ∘ _ ≈⟨ pushˡ ≅∘[]+[]≈μ∘μ+μ ⟩ + (μ ∘ (μ +₁ μ)) ∘ ((i₁″ ∘ ι₁) +₁ (i₂″ ∘ ι₁)) +₁ ((i₁″ ∘ ι₂) +₁ (i₂″ ∘ ι₂)) ∘ (α⇐ ∘ _) ≈⟨ refl⟩∘⟨ swap-inner-natural ⟩ + (μ ∘ (μ +₁ μ)) ∘ swap-inner ∘ _ ≈⟨ pullˡ assoc ⟩ + (μ ∘ (μ +₁ μ) ∘ swap-inner) ∘ _ ≈⟨ pushˡ μ∘μ+μ∘swap-inner ⟩ + μ ∘ (μ +₁ μ) ∘ ((i₁″ ∘ ι₁) +₁ (i₁″ ∘ ι₂)) +₁ ((i₂″ ∘ ι₁) +₁ (i₂″ ∘ ι₂)) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟩⊗⟨ ⊗-distrib-over-∘ ⟩ + μ ∘ (μ +₁ μ) ∘ (i₁″ +₁ i₁″ ∘ ι₁ +₁ ι₂) +₁ (i₂″ +₁ i₂″ ∘ ι₁ +₁ ι₂) ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + μ ∘ (μ ∘ i₁″ +₁ i₁″ ∘ ι₁ +₁ ι₂) +₁ (μ ∘ i₂″ +₁ i₂″ ∘ ι₁ +₁ ι₂) ≈⟨ refl⟩∘⟨ extendʳ μ-natural ⟩⊗⟨ extendʳ μ-natural ⟨ + μ ∘ (i₁″ ∘ μ ∘ ι₁ +₁ ι₂) +₁ (i₂″ ∘ μ ∘ ι₁ +₁ ι₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ μ∘+) ⟩⊗⟨ (refl⟩∘⟨ μ∘+) ⟨ + μ ∘ (i₁″ ∘ [ ι₁ , ι₂ ]′) +₁ (i₂″ ∘ [ ι₁ , ι₂ ]′) ≈⟨ refl⟩∘⟨ elimʳ +-η ⟩⊗⟨ elimʳ +-η ⟩ + μ ∘ i₁″ +₁ i₂″ ≈⟨ μ∘+ ⟨ + [ i₁″ , i₂″ ]′ ∎ + + module _ where + + open 𝒟 using (U; _⊗₁_; module ⊗; module unitorˡ; module unitorʳ; monoidal; assoc-commute-from; assoc-commute-to) + open Category U + open ⇒-Reasoning U + open Equiv + open ⊗-Reasoning monoidal + open smc𝒞 using () renaming (associator to α) + open 𝒟 using () renaming (associator to α′) + open Morphism._≅_ + + swap-unit : 𝒟.braiding.⇐.η (𝒟.unit , 𝒟.unit) ≈ 𝒟.id + swap-unit = cancel-toʳ 𝒟.unitorˡ + ( braiding-coherence-inv 𝒟.braided + ○ sym (coherence-inv₃ monoidal) + ○ sym 𝒟.identityˡ) + + φ-swap-inner : φ (N + M , N′ + M′) ∘ (φ (N , M) ∘ s ⊗₁ t) ⊗₁ (φ (N′ , M′) ∘ s′ ⊗₁ t′) + ≈ F.F₁ swap-inner ∘ φ (N + N′ , M + M′) ∘ (φ (N , N′) ∘ s ⊗₁ s′) ⊗₁ (φ (M , M′) ∘ t ⊗₁ t′) + φ-swap-inner = refl⟩∘⟨ ⊗-distrib-over-∘ + ○ extendʳ + ( insertˡ ([ F.F ]-resp-≅ α .isoˡ) ⟩∘⟨ serialize₁₂ + ○ center (assoc ○ F.associativity) + ○ refl⟩∘⟨ + (extendˡ + ( refl⟩∘⟨ sym ⊗.identity ⟩⊗⟨refl + ○ extendˡ assoc-commute-from + ○ ( merge₂ʳ + ○ sym F.identity ⟩⊗⟨ + ( switch-fromtoʳ α′ (assoc ○ (sym F.associativity)) + ○ ( refl⟩∘⟨ + ( refl⟩∘⟨ + ( switch-fromtoʳ 𝒟.braiding.FX≅GX (sym F.braiding-compat) ⟩⊗⟨refl + ○ assoc ⟩⊗⟨refl + ○ split₁ʳ + ○ refl⟩⊗⟨ sym F.identity ⟩∘⟨refl) + ○ extendʳ (φ-commute (_ , 𝒞.id)) + ○ refl⟩∘⟨ + ( refl⟩∘⟨ split₁ˡ + ○ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α) F.associativity)) + ○ pullˡ (sym F.homomorphism)) + ○ pullˡ (sym F.homomorphism)) ⟩∘⟨refl + ○ assoc) + ○ split₂ʳ) ⟩∘⟨refl) + ○ ( extendʳ (φ-commute (𝒞.id , _)) + ○ refl⟩∘⟨ + ( refl⟩∘⟨ split₂ʳ + ○ extendʳ + ( refl⟩∘⟨ (refl⟩⊗⟨ assoc ○ split₂ʳ) + ○ extendʳ (switch-fromtoʳ α′ (assoc ○ (sym F.associativity))) + ○ refl⟩∘⟨ + ( refl⟩∘⟨ (refl⟩⊗⟨ assoc ○ split₂ʳ) + ○ extendʳ assoc-commute-to + ○ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl) + ○ extendʳ (assoc ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym serialize₁₂)))) + ○ pullˡ (sym F.homomorphism) + ○ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ pullʳ merge₂ʳ) ) ⟩∘⟨refl ) + ○ center⁻¹ (sym F.homomorphism) assoc) + ○ refl⟩∘⟨ + ( pullʳ + ( extendˡ assoc-commute-from + ○ ( pullʳ + ( merge₂ˡ + ○ refl⟩⊗⟨ + ( extendˡ assoc-commute-to + ○ ( pullʳ (sym split₁ˡ ○ (𝒟.braiding.⇐.commute (s′ , t) ○ elimʳ swap-unit) ⟩⊗⟨refl) + ○ assoc-commute-from ) ⟩∘⟨refl + ○ cancelʳ 𝒟.associator.isoʳ)) + ○ assoc-commute-to) ⟩∘⟨refl + ○ cancelʳ 𝒟.associator.isoˡ) + ○ pullʳ (sym ⊗-distrib-over-∘)) + + open Shorthands monoidal + + same-deco + : (F.₁ Q+Q′≅Q″.from ∘ φ (Q , Q′) ∘ (F.₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ s ⊗₁ t ∘ ρ⇐) ⊗₁ (F.₁ [ i₁′ , i₂′ ]′ ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐) ∘ ρ⇐) + ≈ (F.₁ [ i₁″ , i₂″ ]′ ∘ φ (N + N′ , M + M′) ∘ (φ (N , N′) ∘ s ⊗₁ s′ ∘ ρ⇐) ⊗₁ (φ (M , M′) ∘ t ⊗₁ t′ ∘ ρ⇐) ∘ ρ⇐) + same-deco = + refl⟩∘⟨ + ( refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ + ○ extendʳ (φ-commute ([ i₁ , i₂ ]′ , [ i₁′ , i₂′ ]′)) + ○ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩⊗⟨ sym-assoc ⟩∘⟨refl + ○ refl⟩∘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ + ○ refl⟩∘⟨ sym-assoc) + ○ pullˡ (sym F.homomorphism) + ○ extendʳ (pushʳ φ-swap-inner) + ○ (sym F.homomorphism ○ F.F-resp-≈ ≅∘[]+[]∘σ₄) ⟩∘⟨refl + ○ refl⟩∘⟨ + ( assoc + ○ refl⟩∘⟨ pullˡ (sym ⊗-distrib-over-∘) + ○ refl⟩∘⟨ assoc ⟩⊗⟨ assoc ⟩∘⟨refl) + +⊗-resp-≈ + : {A A′ B B′ : Obj} + {f f′ : Cospans [ A , B ]} + {g g′ : Cospans [ A′ , B′ ]} + → Cospans [ f ≈ f′ ] + → Cospans [ g ≈ g′ ] + → Cospans [ together f g ≈ together f′ g′ ] +⊗-resp-≈ {_} {_} {_} {_} {f} {f′} {g} {g′} ≈f ≈g = record + { cospans-≈ = Stack.⊗-resp-≈ (≈f .cospans-≈) (≈g .cospans-≈) + ; same-deco = same-deco + } + where + + open _≈_′ using (cospans-≈) + + module SameNames where + open _≈_′ ≈f using () renaming (same-deco to ≅∘s≈t) public + open _≈_′ ≈g using () renaming (same-deco to ≅∘s≈t′) public + open Cospan._≈_ (≈f .cospans-≈) using (module ≅N) public + open Cospan._≈_ (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public + + open SameNames + + module DecorationNames where + open DecoratedCospan f using (N) renaming (decoration to s) public + open DecoratedCospan f′ using () renaming (decoration to t; N to M) public + open DecoratedCospan g using () renaming (decoration to s′; N to N′) public + open DecoratedCospan g′ using () renaming (decoration to t′; N to M′) public + + open DecorationNames + + module _ where + open 𝒞 using (_⇒_) + ≅ : N ⇒ M + ≅ = ≅N.from + ≅′ : N′ ⇒ M′ + ≅′ = ≅N′.from + + open 𝒞 using (_+₁_) + + module _ where + + open 𝒟 using (U; monoidal; _⊗₁_) + open Category U + open Equiv + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open F.⊗-homo using () renaming (η to φ; commute to φ-commute) + open F using (F₁) + open Shorthands monoidal + + same-deco : F₁ (≅ +₁ ≅′) ∘ φ (N , N′) ∘ s ⊗₁ s′ ∘ ρ⇐ ≈ φ (M , M′) ∘ t ⊗₁ t′ ∘ ρ⇐ + same-deco = begin + F₁ (≅ +₁ ≅′) ∘ φ (N , N′) ∘ s ⊗₁ s′ ∘ ρ⇐ ≈⟨ extendʳ (φ-commute (_ , _)) ⟨ + φ (M , M′) ∘ F₁ ≅ ⊗₁ F₁ ≅′ ∘ s ⊗₁ s′ ∘ ρ⇐ ≈⟨ pull-center (sym ⊗-distrib-over-∘) ⟩ + φ (M , M′) ∘ (F₁ ≅ ∘ s) ⊗₁ (F₁ ≅′ ∘ s′) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ ≅∘s≈t ⟩⊗⟨ ≅∘s≈t′ ⟩∘⟨refl ⟩ + φ (M , M′) ∘ t ⊗₁ t′ ∘ ρ⇐ ∎ + +⊗ : Bifunctor Cospans Cospans Cospans +⊗ = record + { F₀ = λ (A , A′) → A + A′ + ; F₁ = λ (f , g) → together f g + ; identity = λ { {x , y} → id⊗id≈id {x} {y} } + ; homomorphism = λ { {_} {_} {_} {A⇒B , A⇒B′} {B⇒C , B⇒C′} → homomorphism A⇒B B⇒C A⇒B′ B⇒C′ } + ; F-resp-≈ = λ (≈f , ≈g) → ⊗-resp-≈ ≈f ≈g + } + +module ⊗ = Functor ⊗ diff --git a/Functor/Instance/Endo/List.agda b/Functor/Instance/Endo/List.agda new file mode 100644 index 0000000..67e3d0b --- /dev/null +++ b/Functor/Instance/Endo/List.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Functor.Instance.Endo.List {ℓ : Level} where + +import Functor.Instance.List {ℓ} {ℓ} as List + +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Endofunctor) + +-- List is only an endofunctor when the carrier sets and +-- equivalence relations live at the same level +List : Endofunctor (Setoids ℓ ℓ) +List = List.List diff --git a/Functor/Instance/List.agda b/Functor/Instance/List.agda new file mode 100644 index 0000000..a280218 --- /dev/null +++ b/Functor/Instance/List.agda @@ -0,0 +1,67 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Functor.Instance.List {c ℓ : Level} where + +import Data.List.Properties as ListProps +import Data.List.Relation.Binary.Pointwise as PW + +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Setoid using (∣_∣; _⇒ₛ_) +open import Function.Base using (_∘_; id) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Relation.Binary using (Setoid) + +open Functor +open Setoid using (reflexive) +open Func + +open import Data.Opaque.List as L hiding (List) + +private + variable + A B C : Setoid c ℓ + +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) + +opaque + + unfolding L.List + + map-id + : (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ A)) + → mapₛ (Id _) ⟨$⟩ xs ≈ xs + map-id {A} = reflexive (Listₛ A) ∘ ListProps.map-id + + List-homo + : (f : A ⟶ₛ B) + (g : B ⟶ₛ C) + → (xs : ∣ Listₛ A ∣) + → (open Setoid (Listₛ C)) + → mapₛ (g ∙ f) ⟨$⟩ xs ≈ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ xs) + List-homo {C = C} f g = reflexive (Listₛ C) ∘ ListProps.map-∘ + + List-resp-≈ + : (f g : A ⟶ₛ B) + → (let open Setoid (A ⇒ₛ B) in f ≈ g) + → (let open Setoid (Listₛ A ⇒ₛ Listₛ B) in mapₛ f ≈ mapₛ g) + List-resp-≈ f g f≈g = PW.map⁺ (to f) (to g) (PW.refl f≈g) + +-- the List functor takes a carrier A to lists of A +-- and the equivalence on A to pointwise equivalence on lists of A + +-- List on morphisms is the familiar map operation +-- which applies the same function to every element of a list + +List : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) +List .F₀ = Listₛ +List .F₁ = mapₛ +List .identity {_} {xs} = map-id xs +List .homomorphism {f = f} {g} {xs} = List-homo f g xs +List .F-resp-≈ {f = f} {g} f≈g = List-resp-≈ f g f≈g + +module List = Functor List diff --git a/Functor/Instance/Monoidalize.agda b/Functor/Instance/Monoidalize.agda new file mode 100644 index 0000000..6423109 --- /dev/null +++ b/Functor/Instance/Monoidalize.agda @@ -0,0 +1,43 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (MonoidalCategory) +open import Categories.Category.Cocartesian using (Cocartesian) + +module Functor.Instance.Monoidalize + {o o′ ℓ ℓ′ e e ′ : Level} + {C : Category o ℓ e} + (cocartesian : Cocartesian C) + (D : MonoidalCategory o ℓ e) + where + +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) + +open import Categories.Functor using (Functor) +open import Categories.Functor.Monoidal using (MonoidalFunctor) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Construction.Functors using (Functors) +open import Categories.Category.Construction.MonoidalFunctors using (module Lax) +open import Functor.Monoidal.Construction.MonoidValued cocartesian {D} using () renaming (F,⊗,ε to MonoidalFunctorOf) +open import NaturalTransformation.Monoidal.Construction.MonoidValued cocartesian {D} using () renaming (β,⊗,ε to MonoidalNaturalTransformationOf) + +C-MC : MonoidalCategory o ℓ e +C-MC = record { monoidal = +-monoidal } + where + open CocartesianMonoidal C cocartesian + +module C = MonoidalCategory C-MC +module D = MonoidalCategory D + +open Lax using (MonoidalFunctors) +open Functor + +Monoidalize : Functor (Functors C.U (Monoids D.monoidal)) (MonoidalFunctors C-MC D) +Monoidalize .F₀ = MonoidalFunctorOf +Monoidalize .F₁ α = MonoidalNaturalTransformationOf α +Monoidalize .identity = D.Equiv.refl +Monoidalize .homomorphism = D.Equiv.refl +Monoidalize .F-resp-≈ x = x + +module Monoidalize = Functor Monoidalize diff --git a/Functor/Instance/Multiset.agda b/Functor/Instance/Multiset.agda new file mode 100644 index 0000000..b961c7b --- /dev/null +++ b/Functor/Instance/Multiset.agda @@ -0,0 +1,72 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Functor.Instance.Multiset {c ℓ : Level} where + +import Data.Opaque.List as L +import Data.List.Properties as ListProps +import Data.List.Relation.Binary.Pointwise as PW + +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.List.Relation.Binary.Permutation.Setoid using (↭-setoid; ↭-reflexive-≋) +open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺) +open import Data.Opaque.Multiset using (Multisetₛ; mapₛ) +open import Data.Setoid using (∣_∣; _⇒ₛ_) +open import Function.Base using (_∘_; id) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) +open import Relation.Binary using (Setoid) + +open Functor +open Setoid using (reflexive) +open Func + +private + variable + A B C : Setoid c ℓ + +-- the Multiset functor takes a carrier A to lists of A +-- and the equivalence on A to permutation equivalence on lists of A + +-- Multiset on morphisms applies the same function to every element of a multiset + +opaque + unfolding mapₛ + + map-id + : (xs : ∣ Multisetₛ A ∣) + → (open Setoid (Multisetₛ A)) + → mapₛ (Id A) ⟨$⟩ xs ≈ xs + map-id {A} = reflexive (Multisetₛ A) ∘ ListProps.map-id + +opaque + unfolding mapₛ + + Multiset-homo + : (f : A ⟶ₛ B) + (g : B ⟶ₛ C) + → (xs : ∣ Multisetₛ A ∣) + → (open Setoid (Multisetₛ C)) + → mapₛ (g ∙ f) ⟨$⟩ xs ≈ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ xs) + Multiset-homo {C = C} f g = reflexive (Multisetₛ C) ∘ ListProps.map-∘ + +opaque + unfolding mapₛ + + Multiset-resp-≈ + : (f g : A ⟶ₛ B) + → (let open Setoid (A ⇒ₛ B) in f ≈ g) + → (let open Setoid (Multisetₛ A ⇒ₛ Multisetₛ B) in mapₛ f ≈ mapₛ g) + Multiset-resp-≈ {A} {B} f g f≈g = ↭-reflexive-≋ B (PW.map⁺ (to f) (to g) (PW.refl f≈g)) + +Multiset : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ)) +Multiset .F₀ = Multisetₛ +Multiset .F₁ = mapₛ +Multiset .identity {A} {xs} = map-id {A} xs +Multiset .homomorphism {f = f} {g} {xs} = Multiset-homo f g xs +Multiset .F-resp-≈ {A} {B} {f} {g} f≈g = Multiset-resp-≈ f g f≈g + +module Multiset = Functor Multiset diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda new file mode 100644 index 0000000..88a6ec6 --- /dev/null +++ b/Functor/Instance/Nat/Circ.agda @@ -0,0 +1,56 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Functor.Instance.Nat.Circ {ℓ : Level} where + +import Data.List.Relation.Binary.Permutation.Setoid as ↭ + +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×) +open import Data.Circuit using (mk≈) +open import Data.Circuit {ℓ} using (Circuitₛ; mkCircuitₛ; edgesₛ) +open import Data.Circuit.Gate using (Gates) +open import Data.Nat using (ℕ) +open import Data.Opaque.Multiset using (Multisetₛ) +open import Data.Product using (proj₁; proj₂; Σ-syntax) +open import Functor.Free.Instance.CMonoid using (Free) +open import Functor.Instance.Nat.Edge {ℓ} Gates using (Edge) +open import Functor.Properties using (define-by-pw-iso) + +open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids) +open import Category.Construction.CMonoids.Properties Setoids-×.symmetric using (transport-by-iso) +open import Object.Monoid.Commutative Setoids-×.symmetric using (CommutativeMonoid) + +Edges : Functor Nat CMonoids +Edges = Free ∘F Edge + +module Edges = Functor Edges +module Edge = Functor Edge + +opaque + unfolding Multisetₛ + Edges≅Circₛ : (n : ℕ) → Setoids-×.U [ Multisetₛ (Edge.₀ n) ≅ Circuitₛ n ] + Edges≅Circₛ n = record + { from = mkCircuitₛ + ; to = edgesₛ + ; iso = record + { isoˡ = ↭.↭-refl (Edge.₀ n) + ; isoʳ = mk≈ (↭.↭-refl (Edge.₀ n)) + } + } + +private + Edges≅ : (n : ℕ) → Σ[ M ∈ CommutativeMonoid ] CMonoids [ Edges.₀ n ≅ M ] + Edges≅ n = transport-by-iso (Edges.₀ n) (Edges≅Circₛ n) + +Circuitₘ : ℕ → CommutativeMonoid +Circuitₘ n = proj₁ (Edges≅ n) + +Edges≅Circₘ : (n : ℕ) → CMonoids [ Edges.₀ n ≅ Circuitₘ n ] +Edges≅Circₘ n = proj₂ (Edges≅ n) + +Circ : Functor Nat CMonoids +Circ = proj₁ (define-by-pw-iso Edges Circuitₘ Edges≅Circₘ) diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda new file mode 100644 index 0000000..c69a1db --- /dev/null +++ b/Functor/Instance/Nat/Edge.agda @@ -0,0 +1,60 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) +open import Level using (Level; 0ℓ) + +module Functor.Instance.Nat.Edge {ℓ : Level} (HL : HypergraphLabel) where + +import Data.Vec as Vec +import Data.Vec.Properties as VecProps + +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Fin using (Fin) +open import Data.Fin.Properties using (cast-is-id) +open import Data.Hypergraph.Edge {ℓ} HL as Edge using (Edgeₛ; map; mapₛ; _≈_) +open import Data.Nat using (ℕ) +open import Data.Vec.Relation.Binary.Equality.Cast using (≈-reflexive) +open import Function using (id; _∘_; Func; _⟶ₛ_) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) + +module HL = HypergraphLabel HL + +open Edge.Edge +open Edge._≈_ +open Func +open Functor + +map-id : {v : ℕ} {e : Edge.Edge v} → map id e ≈ e +map-id .≡arity = ≡.refl +map-id .≡label = HL.≈-reflexive ≡.refl +map-id {_} {e} .≡ports = ≡.cong (ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl + +map-∘ + : {n m o : ℕ} + (f : Fin n → Fin m) + (g : Fin m → Fin o) + {e : Edge.Edge n} + → map (g ∘ f) e ≈ map g (map f e) +map-∘ f g .≡arity = ≡.refl +map-∘ f g .≡label = HL.≈-reflexive ≡.refl +map-∘ f g {e} .≡ports = ≡.cong (g ∘ f ∘ ports e) ∘ ≡.sym ∘ cast-is-id ≡.refl + +map-resp-≗ + : {n m : ℕ} + {f g : Fin n → Fin m} + → f ≗ g + → {e : Edge.Edge n} + → map f e ≈ map g e +map-resp-≗ f≗g .≡arity = ≡.refl +map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl +map-resp-≗ {g = g} f≗g {e} .≡ports i = ≡.trans (f≗g (ports e i)) (≡.cong (g ∘ ports e) (≡.sym (cast-is-id ≡.refl i))) + +Edge : Functor Nat (Setoids ℓ ℓ) +Edge .F₀ = Edgeₛ +Edge .F₁ = mapₛ +Edge .identity = map-id +Edge .homomorphism {f = f} {g} = map-∘ f g +Edge .F-resp-≈ = map-resp-≗ diff --git a/Functor/Instance/Nat/Preimage.agda b/Functor/Instance/Nat/Preimage.agda new file mode 100644 index 0000000..7da00f4 --- /dev/null +++ b/Functor/Instance/Nat/Preimage.agda @@ -0,0 +1,65 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Preimage where + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Fin.Base using (Fin) +open import Data.Bool.Base using (Bool) +open import Data.Nat.Base using (ℕ) +open import Data.Subset.Functional using (Subset) +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +open Functor +open Func + +_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ +_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) +infixr 4 _≈_ + +private + variable A B C : ℕ + +-- action on objects (Subset n) +Subsetₛ : ℕ → Setoid 0ℓ 0ℓ +Subsetₛ = ≋-setoid (≡.setoid Bool) + +-- action of Preimage on morphisms (contravariant) +Preimage₁ : (Fin A → Fin B) → Subsetₛ B ⟶ₛ Subsetₛ A +to (Preimage₁ f) i = i ∘ f +cong (Preimage₁ f) x≗y = x≗y ∘ f + +-- Preimage respects identity +Preimage-identity : Preimage₁ id ≈ Id (Subsetₛ A) +Preimage-identity {A} = Setoid.refl (Subsetₛ A) + +-- Preimage flips composition +Preimage-homomorphism + : {A B C : ℕ} + (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Preimage₁ (g ∘ f) ≈ Preimage₁ f ∙ Preimage₁ g +Preimage-homomorphism {A} _ _ = Setoid.refl (Subsetₛ A) + +-- Preimage respects equality +Preimage-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Preimage₁ f ≈ Preimage₁ g +Preimage-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +-- the Preimage functor +Preimage : Functor Natop (Setoids 0ℓ 0ℓ) +F₀ Preimage = Subsetₛ +F₁ Preimage = Preimage₁ +identity Preimage = Preimage-identity +homomorphism Preimage {f = f} {g} {v} = Preimage-homomorphism g f {v} +F-resp-≈ Preimage = Preimage-resp-≈ diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda new file mode 100644 index 0000000..b1764d9 --- /dev/null +++ b/Functor/Instance/Nat/Pull.agda @@ -0,0 +1,81 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Pull where + +open import Categories.Category.Instance.Nat using (Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.Circuit.Value using (Monoid) +open import Data.System.Values Monoid using (Values) +open import Data.Unit using (⊤; tt) + +open Functor +open Func + +-- Pull takes a natural number n to the setoid Values n + +private + + variable A B C : ℕ + + _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ + _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) + + infixr 4 _≈_ + + opaque + + unfolding Values + + -- action of Pull on morphisms (contravariant) + Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A + to (Pull₁ f) i = i ∘ f + cong (Pull₁ f) x≗y = x≗y ∘ f + + -- Pull respects identity + Pull-identity : Pull₁ id ≈ Id (Values A) + Pull-identity {A} = Setoid.refl (Values A) + + opaque + + unfolding Pull₁ + + -- Pull flips composition + Pull-homomorphism + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g + Pull-homomorphism {A} _ _ = Setoid.refl (Values A) + + -- Pull respects equality + Pull-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Pull₁ f ≈ Pull₁ g + Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +opaque + + unfolding Pull₁ + + Pull-defs : ⊤ + Pull-defs = tt + +-- the Pull functor +Pull : Functor Natop (Setoids 0ℓ 0ℓ) +F₀ Pull = Values +F₁ Pull = Pull₁ +identity Pull = Pull-identity +homomorphism Pull {f = f} {g} = Pull-homomorphism g f +F-resp-≈ Pull = Pull-resp-≈ + +module Pull = Functor Pull diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda new file mode 100644 index 0000000..8126006 --- /dev/null +++ b/Functor/Instance/Nat/Push.agda @@ -0,0 +1,79 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Push where + +open import Categories.Functor using (Functor) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) +open import Data.Fin.Base using (Fin) +open import Data.Fin.Preimage using (preimage; preimage-cong₁) +open import Data.Nat.Base using (ℕ) +open import Data.Subset.Functional using (⁅_⁆) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.Circuit.Value using (Monoid) +open import Data.System.Values Monoid using (Values) +open import Data.Unit using (⊤; tt) + +open Func +open Functor + +-- Push sends a natural number n to Values n + +private + + variable A B C : ℕ + + _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ + _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) + infixr 4 _≈_ + + opaque + + unfolding Values + + -- action of Push on morphisms (covariant) + Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B + to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ + cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ + + -- Push respects identity + Push-identity : Push₁ id ≈ Id (Values A) + Push-identity {_} {v} = merge-⁅⁆ v + + -- Push respects composition + Push-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f + Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ + + -- Push respects equality + Push-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Push₁ f ≈ Push₁ g + Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ + +opaque + + unfolding Push₁ + + Push-defs : ⊤ + Push-defs = tt + +-- the Push functor +Push : Functor Nat (Setoids 0ℓ 0ℓ) +F₀ Push = Values +F₁ Push = Push₁ +identity Push = Push-identity +homomorphism Push = Push-homomorphism +F-resp-≈ Push = Push-resp-≈ + +module Push = Functor Push diff --git a/Functor/Instance/Nat/System.agda b/Functor/Instance/Nat/System.agda new file mode 100644 index 0000000..05e1e7b --- /dev/null +++ b/Functor/Instance/Nat/System.agda @@ -0,0 +1,110 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.System where + + +open import Level using (suc; 0ℓ) + +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor.Core using (Functor) +open import Data.Circuit.Value using (Monoid) +open import Data.Fin.Base using (Fin) +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (_,_; _×_) +open import Data.System {suc 0ℓ} using (System; _≤_; Systemₛ) +open import Data.System.Values Monoid using (module ≋) +open import Data.Unit using (⊤; tt) +open import Function.Base using (id; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) +open import Functor.Instance.Nat.Pull using (Pull) +open import Functor.Instance.Nat.Push using (Push) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +open Func +open Functor +open _≤_ + +private + + variable A B C : ℕ + + opaque + + map : (Fin A → Fin B) → System A → System B + map f X = let open System X in record + { S = S + ; fₛ = fₛ ∙ Pull.₁ f + ; fₒ = Push.₁ f ∙ fₒ + } + + ≤-cong : (f : Fin A → Fin B) {X Y : System A} → Y ≤ X → map f Y ≤ map f X + ⇒S (≤-cong f x≤y) = ⇒S x≤y + ≗-fₛ (≤-cong f x≤y) = ≗-fₛ x≤y ∘ to (Pull.₁ f) + ≗-fₒ (≤-cong f x≤y) = cong (Push.₁ f) ∘ ≗-fₒ x≤y + + System₁ : (Fin A → Fin B) → Systemₛ A ⟶ₛ Systemₛ B + to (System₁ f) = map f + cong (System₁ f) (x≤y , y≤x) = ≤-cong f x≤y , ≤-cong f y≤x + + opaque + + unfolding System₁ + + id-x≤x : {X : System A} → System₁ id ⟨$⟩ X ≤ X + ⇒S (id-x≤x) = Id _ + ≗-fₛ (id-x≤x {_} {x}) i s = cong (System.fₛ x) Pull.identity + ≗-fₒ (id-x≤x {A} {x}) s = Push.identity + + x≤id-x : {x : System A} → x ≤ System₁ id ⟨$⟩ x + ⇒S x≤id-x = Id _ + ≗-fₛ (x≤id-x {A} {x}) i s = cong (System.fₛ x) (≋.sym Pull.identity) + ≗-fₒ (x≤id-x {A} {x}) s = ≋.sym Push.identity + + System-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + {X : System A} + → System₁ (g ∘ f) ⟨$⟩ X ≤ System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) + × System₁ g ⟨$⟩ (System₁ f ⟨$⟩ X) ≤ System₁ (g ∘ f) ⟨$⟩ X + System-homomorphism {f = f} {g} {X} = left , right + where + open System X + left : map (g ∘ f) X ≤ map g (map f X) + left .⇒S = Id S + left .≗-fₛ i s = cong fₛ Pull.homomorphism + left .≗-fₒ s = Push.homomorphism + right : map g (map f X) ≤ map (g ∘ f) X + right .⇒S = Id S + right .≗-fₛ i s = cong fₛ (≋.sym Pull.homomorphism) + right .≗-fₒ s = ≋.sym Push.homomorphism + + System-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → {X : System A} + → System₁ f ⟨$⟩ X ≤ System₁ g ⟨$⟩ X + × System₁ g ⟨$⟩ X ≤ System₁ f ⟨$⟩ X + System-resp-≈ {A} {B} {f = f} {g} f≗g {X} = both f≗g , both (≡.sym ∘ f≗g) + where + open System X + both : {f g : Fin A → Fin B} → f ≗ g → map f X ≤ map g X + both f≗g .⇒S = Id S + both f≗g .≗-fₛ i s = cong fₛ (Pull.F-resp-≈ f≗g {i}) + both {f} {g} f≗g .≗-fₒ s = Push.F-resp-≈ f≗g + +opaque + unfolding System₁ + Sys-defs : ⊤ + Sys-defs = tt + +Sys : Functor Nat (Setoids (suc 0ℓ) (suc 0ℓ)) +Sys .F₀ = Systemₛ +Sys .F₁ = System₁ +Sys .identity = id-x≤x , x≤id-x +Sys .homomorphism {x = X} = System-homomorphism {X = X} +Sys .F-resp-≈ = System-resp-≈ + +module Sys = Functor Sys diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda new file mode 100644 index 0000000..80b7b2f --- /dev/null +++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -0,0 +1,229 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --no-require-unique-meta-solutions #-} + +open import Level using (Level) +module Functor.Instance.Underlying.SymmetricMonoidal.FinitelyCocomplete {o ℓ e : Level} where + +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Object.Coproduct as Coproduct +import Categories.Object.Initial as Initial + +open import Categories.Functor using (Functor; _∘F_) +open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) +open import Categories.Functor.Monoidal using (IsMonoidalFunctor) +open import Categories.Functor.Monoidal.Braided using (module Lax) +open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory; MonoidalCategory) +open import Categories.Category.Product using (_⁂_) +open import Categories.Morphism using (_≅_) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper) renaming (refl to ≃-refl) +open import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric using (module Lax) +open import Data.Product.Base using (_,_) + +open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Category.Instance.SymMonCat {o} {ℓ} {e} using (SymMonCat) +open import Functor.Exact using (RightExactFunctor; idREF; ∘-RightExactFunctor) + +open FinitelyCocompleteCategory using () renaming (symmetricMonoidalCategory to smc) +open SymmetricMonoidalCategory using (unit) renaming (braidedMonoidalCategory to bmc) +open BraidedMonoidalCategory using () renaming (monoidalCategory to mc) + +private + variable + A B C : FinitelyCocompleteCategory o ℓ e + +F₀ : FinitelyCocompleteCategory o ℓ e → SymmetricMonoidalCategory o ℓ e +F₀ C = smc C +{-# INJECTIVE_FOR_INFERENCE F₀ #-} + +F₁ : RightExactFunctor A B → Lax.SymmetricMonoidalFunctor (F₀ A) (F₀ B) +F₁ {A} {B} F = record + { F = F.F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε-iso.from + ; ⊗-homo = ⊗-homo + ; associativity = assoc + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + ; braiding-compat = braiding-compat + } + } + where + module F = RightExactFunctor F + module A = SymmetricMonoidalCategory (F₀ A) + module B = SymmetricMonoidalCategory (F₀ B) + module A′ = FinitelyCocompleteCategory A + module B′ = FinitelyCocompleteCategory B + ε-iso : B.U [ B.unit ≅ F.₀ A.unit ] + ε-iso = Initial.up-to-iso B.U B′.initial (record { ⊥ = F.₀ A′.⊥ ; ⊥-is-initial = F.F-resp-⊥ A′.⊥-is-initial }) + module ε-iso = _≅_ ε-iso + +-iso : ∀ {X Y} → B.U [ F.₀ X B′.+ F.₀ Y ≅ F.₀ (X A′.+ Y) ] + +-iso = Coproduct.up-to-iso B.U B′.coproduct (Coproduct.IsCoproduct⇒Coproduct B.U (F.F-resp-+ (Coproduct.Coproduct⇒IsCoproduct A.U A′.coproduct))) + module +-iso {X Y} = _≅_ (+-iso {X} {Y}) + module B-proofs where + open ⇒-Reasoning B.U + open B.HomReasoning + open B.Equiv + open B using (_∘_; _≈_) + open B′ using (_+₁_; []-congˡ; []-congʳ; []-cong₂) + open A′ using (_+_; i₁; i₂) + ⊗-homo : NaturalTransformation (B.⊗ ∘F (F.F ⁂ F.F)) (F.F ∘F A.⊗) + ⊗-homo = ntHelper record + { η = λ { (X , Y) → +-iso.from {X} {Y} } + ; commute = λ { {X , Y} {X′ , Y′} (f , g) → + B′.coproduct.∘-distribˡ-[] + ○ B′.coproduct.[]-cong₂ + (pullˡ B′.coproduct.inject₁ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₁)) + (pullˡ B′.coproduct.inject₂ ○ [ F.F ]-resp-square (A.Equiv.sym A′.coproduct.inject₂)) + ○ sym B′.coproduct.∘-distribˡ-[] } + } + assoc + : {X Y Z : A.Obj} + → F.₁ A′.+-assocˡ + ∘ +-iso.from {X + Y} {Z} + ∘ (+-iso.from {X} {Y} +₁ B.id {F.₀ Z}) + ≈ +-iso.from {X} {Y + Z} + ∘ (B.id {F.₀ X} +₁ +-iso.from {Y} {Z}) + ∘ B′.+-assocˡ + assoc {X} {Y} {Z} = begin + F.₁ A′.+-assocˡ ∘ +-iso.from ∘ (+-iso.from +₁ B.id) ≈⟨ refl⟩∘⟨ B′.[]∘+₁ ⟩ + F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ +-iso.from , F.₁ i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩ + F.₁ A′.+-assocˡ ∘ B′.[ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.+-assocˡ ∘ B′.[ F.₁ i₁ ∘ F.₁ i₁ , F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ B′.[ F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩ + B′.[ B′.[ F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ _ ] , _ ] ≈⟨ []-congʳ ([]-congʳ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ A′.+-assocˡ ∘ F.₁ i₁ ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁))) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ A′.[ i₁ , i₂ A′.∘ i₁ ] ∘ F.₁ i₂ ] , _ ] ≈⟨ []-congʳ ([]-congˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ A′.+-assocˡ ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-congˡ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ (i₂ A′.∘ i₁) ] , F.₁ (i₂ A′.∘ i₂) ∘ B.id ] ≈⟨ []-cong₂ ([]-congˡ F.homomorphism) (B.identityʳ ○ F.homomorphism) ⟩ + B′.[ B′.[ F.₁ i₁ , F.₁ i₂ B′.∘ F.₁ i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congʳ ([]-congˡ B′.coproduct.inject₁) ⟨ + B′.[ B′.[ F.₁ i₁ , B′.[ F.₁ i₂ B′.∘ F.₁ i₁ , _ ] ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ ([]-cong₂ (sym B′.coproduct.inject₁) (pushˡ (sym B′.coproduct.inject₂))) ⟩ + B′.[ B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.i₁ , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₁ ] , _ ] ≈⟨ []-congʳ B′.coproduct.∘-distribˡ-[] ⟨ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ B′.i₁ , B′.i₂ ∘ B′.i₁ ] , F.₁ i₂ ∘ F.₁ i₂ ] ≈⟨ []-congˡ B′.coproduct.inject₂ ⟨ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ _ , F.₁ i₂ ∘ F.₁ i₂ ] ∘ B′.i₂ ] ≈⟨ []-congˡ (pushˡ (sym B′.coproduct.inject₂)) ⟩ + B′.[ B′.[ F.₁ i₁ , _ ] ∘ B′.[ _ , _ ] , B′.[ F.₁ i₁ , _ ] ∘ B′.i₂ ∘ B′.i₂ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨ + B′.[ F.₁ i₁ , B′.[ F.₁ i₂ ∘ F.₁ i₁ , F.₁ i₂ ∘ F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ []-cong₂ B.identityʳ (B′.coproduct.∘-distribˡ-[]) ⟩∘⟨refl ⟨ + B′.[ F.₁ i₁ B′.∘ B′.id , F.₁ i₂ ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ] ∘ B′.+-assocˡ ≈⟨ pushˡ (sym B′.[]∘+₁) ⟩ + +-iso.from ∘ (B.id +₁ +-iso.from) ∘ B′.+-assocˡ ∎ + unitaryˡ + : {X : A.Obj} + → F.₁ A′.[ A′.initial.! , A.id {X} ] + ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] + ∘ B′.[ B′.i₁ ∘ B′.initial.! , B′.i₂ ∘ B.id ] + ≈ B′.[ B′.initial.! , B.id ] + unitaryˡ {X} = begin + F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ _ , B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩ + _ ∘ B′.[ _ ∘ B′.i₁ ∘ B′.initial.! , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ ∘ B.id ] ≈⟨ refl⟩∘⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ B′.coproduct.inject₂) ⟩ + F.₁ A′.[ A′.initial.! , A.id ] ∘ B′.[ B′.initial.! , F.₁ i₂ ∘ B.id ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ _ ∘ B′.initial.! , F.₁ A′.[ A′.initial.! , A.id ] ∘ F.₁ i₂ ∘ B.id ] ≈⟨ []-cong₂ (sym (B′.¡-unique _)) (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₂)) ⟩ + B′.[ B′.initial.! , F.₁ A.id ∘ B.id ] ≈⟨ []-congˡ (elimˡ F.identity) ⟩ + B′.[ B′.initial.! , B.id ] ∎ + unitaryʳ + : {X : A.Obj} + → F.₁ A′.[ A′.id {X} , A′.initial.! ] + ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] + ∘ B′.[ B′.i₁ ∘ B.id , B′.i₂ ∘ B′.initial.! ] + ≈ B′.[ B.id , B′.initial.! ] + unitaryʳ {X} = begin + F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₁ ∘ B.id , _ ] ≈⟨ refl⟩∘⟨ B′.coproduct.∘-distribˡ-[] ⟩ + _ ∘ B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ∘ B.id , _ ∘ B′.i₂ ∘ B′.initial.! ] ≈⟨ refl⟩∘⟨ []-cong₂ (pullˡ B′.coproduct.inject₁) (sym (B′.¡-unique _)) ⟩ + F.₁ A′.[ A.id , A′.initial.! ] ∘ B′.[ F.₁ i₁ ∘ B.id , B′.initial.! ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.[ A.id , A′.initial.! ] ∘ F.₁ i₁ ∘ B.id , _ ∘ B′.initial.! ] ≈⟨ []-cong₂ (pullˡ ([ F.F ]-resp-∘ A′.coproduct.inject₁)) (sym (B′.¡-unique _)) ⟩ + B′.[ F.₁ A.id ∘ B.id , B′.initial.! ] ≈⟨ []-congʳ (elimˡ F.identity) ⟩ + B′.[ B.id , B′.initial.! ] ∎ + braiding-compat + : {X Y : A.Obj} + → F.₁ A′.[ i₂ {X} {Y} , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] + ≈ B′.[ F.F₁ i₁ , F.F₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ] + braiding-compat = begin + F.₁ A′.[ i₂ , i₁ ] ∘ B′.[ F.₁ i₁ , F.₁ i₂ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟩ + B′.[ F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₁ , F.₁ A′.[ i₂ , i₁ ] ∘ F.₁ i₂ ] ≈⟨ []-cong₂ ([ F.F ]-resp-∘ A′.coproduct.inject₁) ([ F.F ]-resp-∘ A′.coproduct.inject₂) ⟩ + B′.[ F.₁ i₂ , F.₁ i₁ ] ≈⟨ []-cong₂ B′.coproduct.inject₂ B′.coproduct.inject₁ ⟨ + B′.[ B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₂ , B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.i₁ ] ≈⟨ B′.coproduct.∘-distribˡ-[] ⟨ + B′.[ F.₁ i₁ , F.₁ i₂ ] ∘ B′.[ B′.i₂ , B′.i₁ ] ∎ + open B-proofs + +identity : Lax.SymmetricMonoidalNaturalIsomorphism (F₁ (Functor.Exact.idREF {o} {ℓ} {e} {A})) (idF-SymmetricMonoidal (F₀ A)) +identity {A} = record + { U = ≃-refl + ; F⇒G-isMonoidal = record + { ε-compat = ¡-unique₂ (id ∘ ¡) id + ; ⊗-homo-compat = refl⟩∘⟨ sym ([]-cong₂ identityʳ identityʳ) + } + } + where + open FinitelyCocompleteCategory A + open HomReasoning + open Equiv + +homomorphism + : {F : RightExactFunctor A B} + {G : RightExactFunctor B C} + → Lax.SymmetricMonoidalNaturalIsomorphism + (F₁ {A} {C} (∘-RightExactFunctor G F)) + (∘-SymmetricMonoidal (F₁ {B} {C} G) (F₁ {A} {B} F)) +homomorphism {A} {B} {C} {F} {G} = record + { U = ≃-refl + ; F⇒G-isMonoidal = record + { ε-compat = ¡-unique₂ (id ∘ ¡) (G.₁ B.¡ ∘ ¡) + ; ⊗-homo-compat = + identityˡ + ○ sym + ([]-cong₂ + ([ G.F ]-resp-∘ B.coproducts.inject₁) + ([ G.F ]-resp-∘ B.coproducts.inject₂)) + ○ sym ∘-distribˡ-[] + ○ pushʳ (introʳ C.⊗.identity) + } + } + where + module A = FinitelyCocompleteCategory A + module B = FinitelyCocompleteCategory B + open FinitelyCocompleteCategory C + module C = SymmetricMonoidalCategory (F₀ C) + open HomReasoning + open Equiv + open ⇒-Reasoning U + module F = RightExactFunctor F + module G = RightExactFunctor G + +module _ {F G : RightExactFunctor A B} where + + module F = RightExactFunctor F + module G = RightExactFunctor G + + F-resp-≈ + : NaturalIsomorphism F.F G.F + → Lax.SymmetricMonoidalNaturalIsomorphism (F₁ {A} {B} F) (F₁ {A} {B} G) + F-resp-≈ F≃G = record + { U = F≃G + ; F⇒G-isMonoidal = record + { ε-compat = sym (¡-unique (⇒.η A.⊥ ∘ ¡)) + ; ⊗-homo-compat = + ∘-distribˡ-[] + ○ []-cong₂ (⇒.commute A.i₁) (⇒.commute A.i₂) + ○ sym []∘+₁ + } + } + where + module A = FinitelyCocompleteCategory A + open NaturalIsomorphism F≃G + open FinitelyCocompleteCategory B + open HomReasoning + open Equiv + +Underlying : Functor FinitelyCocompletes SymMonCat +Underlying = record + { F₀ = F₀ + ; F₁ = F₁ + ; identity = λ { {X} → identity {X} } + ; homomorphism = λ { {X} {Y} {Z} {F} {G} → homomorphism {X} {Y} {Z} {F} {G} } + ; F-resp-≈ = λ { {X} {Y} {F} {G} → F-resp-≈ {X} {Y} {F} {G} } + } |