diff options
Diffstat (limited to 'Functor')
29 files changed, 2646 insertions, 143 deletions
diff --git a/Functor/Forgetful/Instance/CMonoid.agda b/Functor/Forgetful/Instance/CMonoid.agda new file mode 100644 index 0000000..fd8ecc1 --- /dev/null +++ b/Functor/Forgetful/Instance/CMonoid.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Level using (Level) + +module Functor.Forgetful.Instance.CMonoid + {o ℓ e : Level} + {S : Category o ℓ e} + {monoidal : Monoidal S} + (symmetric : Symmetric monoidal) + where + +open import Categories.Category.Construction.Monoids monoidal using (Monoids) +open import Categories.Functor using (Functor) +open import Category.Construction.CMonoids symmetric using (CMonoids) +open import Function using (id) +open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒) + +private + module S = Category S + +open CommutativeMonoid +open CommutativeMonoid⇒ +open Functor +open S.Equiv using (refl) + +Forget : Functor CMonoids Monoids +Forget .F₀ = monoid +Forget .F₁ = monoid⇒ +Forget .identity = refl +Forget .homomorphism = refl +Forget .F-resp-≈ = id + +module Forget = Functor Forget diff --git a/Functor/Forgetful/Instance/Monoid.agda b/Functor/Forgetful/Instance/Monoid.agda new file mode 100644 index 0000000..2f9e4d8 --- /dev/null +++ b/Functor/Forgetful/Instance/Monoid.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Level using (Level) + +module Functor.Forgetful.Instance.Monoid {o ℓ e : Level} {S : Category o ℓ e} (monoidal : Monoidal S) where + +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Functor using (Functor) +open import Categories.Object.Monoid using (Monoid; Monoid⇒) +open import Function using (id) + +private + module S = Category S + +open Monoid +open Monoid⇒ +open S.Equiv using (refl) +open Functor + +Forget : Functor (Monoids monoidal) S +Forget .F₀ = Carrier +Forget .F₁ = arr +Forget .identity = refl +Forget .homomorphism = refl +Forget .F-resp-≈ = id + +module Forget = Functor Forget diff --git a/Functor/Free/Instance/CMonoid.agda b/Functor/Free/Instance/CMonoid.agda new file mode 100644 index 0000000..be9cb94 --- /dev/null +++ b/Functor/Free/Instance/CMonoid.agda @@ -0,0 +1,116 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Functor.Free.Instance.CMonoid {c ℓ : Level} where + +import Categories.Object.Monoid as MonoidObject +import Object.Monoid.Commutative as CMonoidObject + +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation using (NaturalTransformation) +open import Category.Construction.CMonoids using (CMonoids) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-symmetric′) +open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (++-assoc; ++-identityˡ; ++-identityʳ; ++-comm) +open import Data.Product using (_,_) +open import Data.Setoid using (∣_∣) +open import Data.Opaque.Multiset using ([]ₛ; Multisetₛ; ++ₛ; mapₛ) +open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Functor.Instance.Multiset {c} {ℓ} using (Multiset) +open import NaturalTransformation.Instance.EmptyMultiset {c} {ℓ} using (⊤⇒[]) +open import NaturalTransformation.Instance.MultisetAppend {c} {ℓ} using (++) +open import Relation.Binary using (Setoid) + +module ++ = NaturalTransformation ++ +module ⊤⇒[] = NaturalTransformation ⊤⇒[] + +open Functor +open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) +open CMonoidObject Setoids-×.symmetric using (CommutativeMonoid; IsCommutativeMonoid; CommutativeMonoid⇒) +open IsCommutativeMonoid +open CommutativeMonoid using () renaming (μ to μ′; η to η′) +open IsMonoid +open CommutativeMonoid⇒ +open Monoid⇒ + +module _ (X : Setoid c ℓ) where + + open Setoid (Multiset.₀ X) + + opaque + + unfolding Multisetₛ + + ++ₛ-assoc + : (x y z : ∣ Multisetₛ X ∣) + → ++ₛ ⟨$⟩ (++ₛ ⟨$⟩ (x , y) , z) + ≈ ++ₛ ⟨$⟩ (x , ++ₛ ⟨$⟩ (y , z)) + ++ₛ-assoc x y z = ++-assoc X x y z + + ++ₛ-identityˡ + : (x : ∣ Multisetₛ X ∣) + → x ≈ ++ₛ ⟨$⟩ ([]ₛ ⟨$⟩ _ , x) + ++ₛ-identityˡ x = ++-identityˡ X x + + ++ₛ-identityʳ + : (x : ∣ Multisetₛ X ∣) + → x ≈ ++ₛ ⟨$⟩ (x , []ₛ ⟨$⟩ _) + ++ₛ-identityʳ x = sym (++-identityʳ X x) + + ++ₛ-comm + : (x y : ∣ Multisetₛ X ∣) + → ++ₛ ⟨$⟩ (x , y) ≈ ++ₛ ⟨$⟩ (y , x) + ++ₛ-comm x y = ++-comm X x y + + opaque + unfolding ×-symmetric′ + MultisetCMonoid : IsCommutativeMonoid (Multiset.₀ X) + MultisetCMonoid .isMonoid .μ = ++.η X + MultisetCMonoid .isMonoid .η = ⊤⇒[].η X + MultisetCMonoid .isMonoid .assoc {(x , y) , z} = ++ₛ-assoc x y z + MultisetCMonoid .isMonoid .identityˡ {_ , x} = ++ₛ-identityˡ x + MultisetCMonoid .isMonoid .identityʳ {x , _} = ++ₛ-identityʳ x + MultisetCMonoid .commutative {x , y} = ++ₛ-comm x y + +Multisetₘ : (X : Setoid c ℓ) → CommutativeMonoid +Multisetₘ X = record { isCommutativeMonoid = MultisetCMonoid X } + +open Setoids-× using (_⊗₀_; _⊗₁_) +opaque + unfolding MultisetCMonoid + mapₛ-++ₛ + : {A B : Setoid c ℓ} + → (f : A ⟶ₛ B) + → {xy : ∣ Multisetₛ A ⊗₀ Multisetₛ A ∣} + → (open Setoid (Multisetₛ B)) + → mapₛ f ⟨$⟩ (μ′ (Multisetₘ A) ⟨$⟩ xy) + ≈ μ′ (Multisetₘ B) ⟨$⟩ (mapₛ f ⊗₁ mapₛ f ⟨$⟩ xy) + mapₛ-++ₛ = ++.sym-commute + +opaque + unfolding MultisetCMonoid mapₛ + mapₛ-[]ₛ + : {A B : Setoid c ℓ} + → (f : A ⟶ₛ B) + → {x : ∣ Setoids-×.unit ∣} + → (open Setoid (Multisetₛ B)) + → mapₛ f ⟨$⟩ (η′ (Multisetₘ A) ⟨$⟩ x) + ≈ η′ (Multisetₘ B) ⟨$⟩ x + mapₛ-[]ₛ = ⊤⇒[].commute + +mapₘ + : {A B : Setoid c ℓ} + (f : A ⟶ₛ B) + → CommutativeMonoid⇒ (Multisetₘ A) (Multisetₘ B) +mapₘ f .monoid⇒ .arr = Multiset.₁ f +mapₘ f .monoid⇒ .preserves-μ = mapₛ-++ₛ f +mapₘ f .monoid⇒ .preserves-η = mapₛ-[]ₛ f + +Free : Functor (Setoids c ℓ) (CMonoids Setoids-×.symmetric) +Free .F₀ = Multisetₘ +Free .F₁ = mapₘ +Free .identity {X} = Multiset.identity {X} +Free .homomorphism {X} {Y} {Z} {f} {g} = Multiset.homomorphism {X} {Y} {Z} {f} {g} +Free .F-resp-≈ {A} {B} {f} {g} = Multiset.F-resp-≈ {A} {B} {f} {g} diff --git a/Functor/Free/Instance/Monoid.agda b/Functor/Free/Instance/Monoid.agda new file mode 100644 index 0000000..c8450b9 --- /dev/null +++ b/Functor/Free/Instance/Monoid.agda @@ -0,0 +1,116 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; suc) + +module Functor.Free.Instance.Monoid {c ℓ : Level} where + +import Categories.Object.Monoid as MonoidObject + +open import Categories.Category using (Category) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation using (NaturalTransformation) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-monoidal′) +open import Data.List.Properties using (++-assoc; ++-identityˡ; ++-identityʳ) +open import Data.Opaque.List using ([]ₛ; Listₛ; ++ₛ; mapₛ) +open import Data.Product using (_,_) +open import Data.Setoid using (∣_∣) +open import Function using (_⟶ₛ_; _⟨$⟩_) +open import Functor.Instance.List {c} {ℓ} using (List) +open import NaturalTransformation.Instance.EmptyList {c} {ℓ} using (⊤⇒[]) +open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +module ++ = NaturalTransformation ++ +module ⊤⇒[] = NaturalTransformation ⊤⇒[] + +open Functor +open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒) + +open IsMonoid + +-- the functor sending a setoid A to the monoid List A + +module _ (X : Setoid c ℓ) where + + open Setoid (List.₀ X) + + opaque + + unfolding []ₛ + + ++ₛ-assoc + : (x y z : ∣ Listₛ X ∣) + → ++ₛ ⟨$⟩ (++ₛ ⟨$⟩ (x , y) , z) + ≈ ++ₛ ⟨$⟩ (x , ++ₛ ⟨$⟩ (y , z)) + ++ₛ-assoc x y z = reflexive (++-assoc x y z) + + ++ₛ-identityˡ + : (x : ∣ Listₛ X ∣) + → x ≈ ++ₛ ⟨$⟩ ([]ₛ ⟨$⟩ _ , x) + ++ₛ-identityˡ x = reflexive (++-identityˡ x) + + ++ₛ-identityʳ + : (x : ∣ Listₛ X ∣) + → x ≈ ++ₛ ⟨$⟩ (x , []ₛ ⟨$⟩ _) + ++ₛ-identityʳ x = sym (reflexive (++-identityʳ x)) + + opaque + + unfolding ×-monoidal′ + + ListMonoid : IsMonoid (List.₀ X) + ListMonoid = record + { μ = ++.η X + ; η = ⊤⇒[].η X + ; assoc = λ { {(x , y) , z} → ++ₛ-assoc x y z } + ; identityˡ = λ { {_ , x} → ++ₛ-identityˡ x } + ; identityʳ = λ { {x , _} → ++ₛ-identityʳ x } + } + +Listₘ : Setoid c ℓ → Monoid +Listₘ X = record { isMonoid = ListMonoid X } + +opaque + + unfolding ListMonoid + + mapₘ + : {Aₛ Bₛ : Setoid c ℓ} + (f : Aₛ ⟶ₛ Bₛ) + → Monoid⇒ (Listₘ Aₛ) (Listₘ Bₛ) + mapₘ f = record + { arr = List.₁ f + ; preserves-μ = λ {x,y} → ++.sym-commute f {x,y} + ; preserves-η = ⊤⇒[].sym-commute f + } + +module U = Category Setoids-×.U +open Monoid⇒ using (arr) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Composition using () renaming (function to compose) +opaque + unfolding mapₘ + Free-identity : {X : Setoid c ℓ} → arr (mapₘ (Id X)) U.≈ U.id + Free-identity = List.identity + + Free-homomorphism : {X Y Z : Setoid c ℓ} {f : X ⟶ₛ Y} {g : Y ⟶ₛ Z} → arr (mapₘ (compose f g)) U.≈ arr (mapₘ g) U.∘ arr (mapₘ f) + Free-homomorphism = List.homomorphism + + Free-resp-≈ + : {X Y : Setoid c ℓ} + {f g : X ⟶ₛ Y} + (let module Y = Setoid Y) + → (∀ {x} → f ⟨$⟩ x Y.≈ g ⟨$⟩ x) + → arr (mapₘ f) U.≈ arr (mapₘ g) + Free-resp-≈ = List.F-resp-≈ + +Free : Functor (Setoids c ℓ) (Monoids Setoids-×.monoidal) +Free .F₀ = Listₘ +Free .F₁ = mapₘ +Free .identity = Free-identity +Free .homomorphism = Free-homomorphism +Free .F-resp-≈ = Free-resp-≈ 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 03cca1f..b72219b 100644 --- a/Functor/Instance/Cospan/Stack.agda +++ b/Functor/Instance/Cospan/Stack.agda @@ -9,9 +9,11 @@ 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.Cartesian.Instance.FinitelyCocompletes {o} {ℓ} {e} using (-+-; FinitelyCocompletes-CC) open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) @@ -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 index e87f20c..fedddba 100644 --- a/Functor/Instance/Decorate.agda +++ b/Functor/Instance/Decorate.agda @@ -1,4 +1,5 @@ {-# 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) @@ -19,6 +20,7 @@ module Functor.Instance.Decorate 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) @@ -27,10 +29,10 @@ 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 (Cospan; Cospans; Same) +open import Category.Instance.Cospans 𝒞 using (Cospans) open import Category.Instance.DecoratedCospans 𝒞 F using (DecoratedCospans) -open import Functor.Instance.Cospan.Stack using (⊗) -open import Functor.Instance.DecoratedCospan.Stack using () renaming (⊗ to ⊗′) +open import Functor.Instance.Cospan.Stack 𝒞 using (module ⊗) +open import Functor.Instance.DecoratedCospan.Stack 𝒞 F using () renaming (module ⊗ to ⊗′) module 𝒞 = FinitelyCocompleteCategory 𝒞 module 𝒟 = SymmetricMonoidalCategory 𝒟 @@ -40,7 +42,7 @@ 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 empty decoration +-- i.e. the original cospan with the discrete decoration private variable @@ -67,14 +69,14 @@ identity = record open ⇒-Reasoning 𝒟.U homomorphism : DecoratedCospans [ decorate (Cospans [ g ∘ f ]) ≈ DecoratedCospans [ decorate g ∘ decorate f ] ] -homomorphism {B} {C} {g} {A} {f} = record +homomorphism {g} {f} = record { cospans-≈ = Cospans.Equiv.refl ; same-deco = same-deco } where - open Cospan f using (N; f₂) - open Cospan g using () renaming (N to M; f₁ to g₁) + 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 _+₁_ ) @@ -99,7 +101,7 @@ homomorphism {B} {C} {g} {A} {f} = record 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 (sym 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 (¡ , ¡)) ⟨ @@ -126,19 +128,15 @@ Decorate = record ; F-resp-≈ = F-resp-≈ } -module ⊗ = Functor (⊗ 𝒞) -module ⊗′ = Functor (⊗′ 𝒞 F) -open 𝒞 using (_+₁_) - Decorate-resp-⊗ : DecoratedCospans [ decorate (⊗.₁ (f , g)) ≈ ⊗′.₁ (decorate f , decorate g) ] -Decorate-resp-⊗ {f = f} {g = g} = record - { cospans-≈ = Cospans.Equiv.refl +Decorate-resp-⊗ {f} {g} = record + { cospans-≈ = Cospan.≈-refl ; same-deco = same-deco } where - open Cospan f using (N) - open Cospan g using () renaming (N to M) + 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 _+₁_ ) @@ -165,4 +163,3 @@ Decorate-resp-⊗ {f = f} {g = g} = record 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 index 4595a8f..77b16fa 100644 --- a/Functor/Instance/DecoratedCospan/Embed.agda +++ b/Functor/Instance/DecoratedCospan/Embed.agda @@ -19,6 +19,7 @@ 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; _[_,_]; _[_≈_]; _[_∘_]) @@ -34,9 +35,9 @@ 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.Base using (_,_) -open import Function.Base using () renaming (id to idf) -open import Functor.Instance.DecoratedCospan.Stack using (⊗) +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 𝒟 @@ -62,7 +63,7 @@ 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 = Embed.B₁ f g + { cospan = Cospan.cospan f g ; decoration = s } @@ -265,7 +266,6 @@ module _ where where module Decorate = Functor Decorate - module ⊗ = Functor (⊗ 𝒞 F) open 𝒞 using (_+₁_) L-resp-⊗ : DecoratedCospans [ L.₁ (f +₁ g) ≈ ⊗.₁ (L.₁ f , L.₁ g) ] diff --git a/Functor/Instance/DecoratedCospan/Stack.agda b/Functor/Instance/DecoratedCospan/Stack.agda index 5c3c232..381ee06 100644 --- a/Functor/Instance/DecoratedCospan/Stack.agda +++ b/Functor/Instance/DecoratedCospan/Stack.agda @@ -19,6 +19,7 @@ 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; _[_,_]; _[_≈_]; _[_∘_]) @@ -26,13 +27,16 @@ 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; Same to Same′) -open import Category.Instance.Cospans 𝒞 using (Same; compose) +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 (_,_) @@ -52,10 +56,9 @@ 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 = Stack.together A⇒B.cospan A⇒B′.cospan + { 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 @@ -108,9 +111,9 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record module _ where open DecoratedCospan using (cospan) - cospans-≈ : Same (Stack.together _ _) (compose (Stack.together _ _) (Stack.together _ _)) + cospans-≈ : _ Cospan.⊗ _ Cospan.≈ Cospan.compose (_ Cospan.⊗ _) (_ Cospan.⊗ _) cospans-≈ = Stack.homomorphism (f .cospan) (g .cospan) (f′ .cospan) (g′ .cospan) - open Same cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public + open Cospan._≈_ cospans-≈ using () renaming (≅N to Q+Q′≅Q″) public module DecorationNames where open DecoratedCospan f using (N) renaming (decoration to s) public @@ -185,7 +188,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record ≅∘[]+[]≈μ∘μ+μ = begin ≅ ∘ [ i₁ , i₂ ]′ +₁ [ i₁′ , i₂′ ]′ ≈⟨ refl⟩∘⟨ μ∘+ ⟩⊗⟨ μ∘+ ⟩ ≅ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ refl⟩∘⟨ introˡ +-η ⟩ - ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ i₁ +₁ i₂) +₁ (μ ∘ i₁′ +₁ i₂′) ≈⟨ push-center (sym μ∘+) ⟩ + ≅ ∘ [ ι₁ , ι₂ ]′ ∘ (μ ∘ 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-∘) ⟩ @@ -221,7 +224,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record α⇐ ∘ 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 (sym split₁ˡ) ⟩∘⟨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₂ˡ ⟩ @@ -231,7 +234,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record μ∘μ+μ∘swap-inner : {X : Obj} → μ {X} ∘ μ +₁ μ ∘ swap-inner ≈ μ ∘ μ +₁ μ {X} μ∘μ+μ∘swap-inner = begin - μ ∘ μ +₁ μ ∘ α⇐ ∘ id +₁ (α⇒ ∘ +-swap +₁ id ∘ α⇐) ∘ α⇒ ≈⟨ push-center (sym serialize₁₂) ⟩ + μ ∘ μ +₁ μ ∘ α⇐ ∘ 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 ⟩ @@ -243,7 +246,7 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record μ ∘ 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 (sym split₂ʳ) ⟩ + μ ∘ 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 ⟩ @@ -370,13 +373,13 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record } where - open Same′ using (cospans-≈) + open _≈_′ using (cospans-≈) module SameNames where - open Same′ ≈f using () renaming (same-deco to ≅∘s≈t) public - open Same′ ≈g using () renaming (same-deco to ≅∘s≈t′) public - open Same (≈f .cospans-≈) using (module ≅N) public - open Same (≈g .cospans-≈) using () renaming (module ≅N to ≅N′) public + 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 @@ -417,9 +420,11 @@ homomorphism {A} {B} {C} {A′} {B′} {C′} f g f′ g′ = record ⊗ : Bifunctor Cospans Cospans Cospans ⊗ = record - { F₀ = λ { (A , A′) → A + A′ } - ; F₁ = λ { (f , g) → together f g } + { 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 } + ; 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/Monoidal/Braided/Strong/Properties.agda b/Functor/Monoidal/Braided/Strong/Properties.agda new file mode 100644 index 0000000..66dc4c0 --- /dev/null +++ b/Functor/Monoidal/Braided/Strong/Properties.agda @@ -0,0 +1,59 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Categories.Category.Monoidal using (BraidedMonoidalCategory) +open import Categories.Functor.Monoidal.Braided using (module Strong) +open Strong using (BraidedMonoidalFunctor) + +module Functor.Monoidal.Braided.Strong.Properties + {o o′ ℓ ℓ′ e e′ : Level} + {C : BraidedMonoidalCategory o ℓ e} + {D : BraidedMonoidalCategory o′ ℓ′ e′} + (F,φ,ε : BraidedMonoidalFunctor C D) where + +import Categories.Category.Construction.Core as Core +import Categories.Category.Monoidal.Utilities as ⊗-Utilities +import Functor.Monoidal.Strong.Properties as MonoidalProp + +open import Categories.Functor.Properties using ([_]-resp-≅) + +private + + module C = BraidedMonoidalCategory C + module D = BraidedMonoidalCategory D + +open D +open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) +open ⊗-Utilities monoidal using (_⊗ᵢ_) +open BraidedMonoidalFunctor F,φ,ε +open MonoidalProp monoidalFunctor public + +private + + variable + A B : Obj + X Y : C.Obj + + σ : A ⊗₀ B ≅ B ⊗₀ A + σ = braiding.FX≅GX + + σ⇐ : B ⊗₀ A ⇒ A ⊗₀ B + σ⇐ = braiding.⇐.η _ + + Fσ : F₀ (X C.⊗₀ Y) ≅ F₀ (Y C.⊗₀ X) + Fσ = [ F ]-resp-≅ C.braiding.FX≅GX + + Fσ⇐ : F₀ (Y C.⊗₀ X) ⇒ F₀ (X C.⊗₀ Y) + Fσ⇐ = F₁ (C.braiding.⇐.η _) + + φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y) + φ = ⊗-homo.FX≅GX + +open HomReasoning +open Shorthands using (φ⇐) + +braiding-compatᵢ : Fσ {X} {Y} ∘ᵢ φ ≈ᵢ φ ∘ᵢ σ +braiding-compatᵢ = ⌞ braiding-compat ⌟ + +braiding-compat-inv : φ⇐ ∘ Fσ⇐ {X} {Y} ≈ σ⇐ ∘ φ⇐ +braiding-compat-inv = to-≈ braiding-compatᵢ diff --git a/Functor/Monoidal/Construction/MonoidValued.agda b/Functor/Monoidal/Construction/MonoidValued.agda new file mode 100644 index 0000000..937714d --- /dev/null +++ b/Functor/Monoidal/Construction/MonoidValued.agda @@ -0,0 +1,214 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Monoidal.Bundle using (MonoidalCategory) +open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_) +open import Level using (Level; _⊔_) + +-- A functor from a cocartesian category 𝒞 to Monoids[S] +-- can be turned into a monoidal functor from 𝒞 to S + +module Functor.Monoidal.Construction.MonoidValued + {o o′ ℓ ℓ′ e e′ : Level} + {𝒞 : Category o ℓ e} + (𝒞-+ : Cocartesian 𝒞) + {S : MonoidalCategory o′ ℓ′ e′} + (let module S = MonoidalCategory S) + (M : Functor 𝒞 (Monoids S.monoidal)) + where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Category.Monoidal.Utilities as ⊗-Util +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Categories.Object.Monoid as MonoidObject + +open import Categories.Category using (module Definitions) +open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor.Monoidal using (MonoidalFunctor; IsMonoidalFunctor) +open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) +open import Categories.Morphism using (_≅_) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Product using (_,_) +open import Functor.Forgetful.Instance.Monoid S.monoidal using (Forget) + +private + + G : Functor 𝒞 S.U + G = Forget ∙ M + + module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ }) + module 𝒞-M = CocartesianMonoidal 𝒞 𝒞-+ + + 𝒞-MC : MonoidalCategory o ℓ e + 𝒞-MC = record { monoidal = 𝒞-M.+-monoidal } + + module +-assoc {n} {m} {o} = _≅_ (𝒞.+-assoc {n} {m} {o}) + module +-λ {n} = _≅_ (𝒞-M.⊥+A≅A {n}) + module +-ρ {n} = _≅_ (𝒞-M.A+⊥≅A {n}) + + module G = Functor G + module M = Functor M + + open MonoidObject S.monoidal using (Monoid; Monoid⇒) + open Monoid renaming (assoc to μ-assoc; identityˡ to μ-identityˡ; identityʳ to μ-identityʳ) + open Monoid⇒ + + open 𝒞 using (-+-; _+_; _+₁_; i₁; i₂; inject₁; inject₂) + + module _ where + + open Category 𝒞 + open ⇒-Reasoning 𝒞 + open ⊗-Reasoning 𝒞-M.+-monoidal + + module _ {n m o : Obj} where + + private + + +-α : (n + m) + o 𝒞.⇒ n + (m + o) + +-α = +-assoc.to {n} {m} {o} + + +-α∘i₂ : +-α ∘ i₂ ≈ i₂ ∘ i₂ + +-α∘i₂ = inject₂ + + +-α∘i₁∘i₁ : (+-α ∘ i₁) ∘ i₁ ≈ i₁ + +-α∘i₁∘i₁ = inject₁ ⟩∘⟨refl ○ inject₁ + + +-α∘i₁∘i₂ : (+-α ∘ i₁) ∘ i₂ ≈ i₂ ∘ i₁ + +-α∘i₁∘i₂ = inject₁ ⟩∘⟨refl ○ inject₂ + + module _ {n : Obj} where + + +-ρ∘i₁ : +-ρ.from {n} ∘ i₁ ≈ id + +-ρ∘i₁ = inject₁ + + +-λ∘i₂ : +-λ.from {n} ∘ i₂ ≈ id + +-λ∘i₂ = inject₂ + + open S + open ⇒-Reasoning U + open ⊗-Reasoning monoidal + open ⊗-Util.Shorthands monoidal + + ⊲ : {A : 𝒞.Obj} → G.₀ A ⊗₀ G.₀ A ⇒ G.₀ A + ⊲ {A} = μ (M.₀ A) + + ⇒⊲ : {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) → G.₁ f ∘ ⊲ ≈ ⊲ ∘ G.₁ f ⊗₁ G.₁ f + ⇒⊲ f = preserves-μ (M.₁ f) + + ε : {A : 𝒞.Obj} → unit ⇒ G.₀ A + ε {A} = η (M.₀ A) + + ⇒ε : {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) → G.₁ f ∘ ε ≈ ε + ⇒ε f = preserves-η (M.₁ f) + + ⊲-⊗ : {n m : 𝒞.Obj} → G.₀ n ⊗₀ G.₀ m ⇒ G.₀ (n + m) + ⊲-⊗ = ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂ + + module _ {n n′ m m′ : 𝒞.Obj} (f : n 𝒞.⇒ n′) (g : m 𝒞.⇒ m′) where + + open Definitions S.U using (CommutativeSquare) + + left₁ : CommutativeSquare (G.₁ i₁) (G.₁ f) (G.₁ (f +₁ g)) (G.₁ i₁) + left₁ = [ G ]-resp-square inject₁ + + left₂ : CommutativeSquare (G.₁ i₂) (G.₁ g) (G.₁ (f +₁ g)) (G.₁ i₂) + left₂ = [ G ]-resp-square inject₂ + + right : CommutativeSquare ⊲ (G.₁ (f +₁ g) ⊗₁ G.₁ (f +₁ g)) (G.₁ (f +₁ g)) ⊲ + right = ⇒⊲ (f +₁ g) + + ⊲-⊗-commute : + CommutativeSquare + (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + (G.₁ f ⊗₁ G.₁ g) + (G.₁ (f +₁ g)) + (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ⊲-⊗-commute = glue′ right (parallel left₁ left₂) + + ⊲-⊗-homo : NaturalTransformation (⊗ ∙ (G ⁂ G)) (G ∙ -+-) + ⊲-⊗-homo = ntHelper record + { η = λ (n , m) → ⊲-⊗ {n} {m} + ; commute = λ (f , g) → Equiv.sym (⊲-⊗-commute f g) + } + + ⊲-⊗-α + : {n m o : 𝒞.Obj} + → G.₁ (+-assoc.to {n} {m} {o}) + ∘ (μ (M.₀ ((n + m) + o)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ∘ (μ (M.₀ (n + m)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ id + ≈ (μ (M.₀ (n + m + o)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ∘ id ⊗₁ (μ (M.₀ (m + o)) ∘ G.₁ i₁ ⊗₁ G.₁ i₂) + ∘ α⇒ + ⊲-⊗-α {n} {m} {o} = begin + G.₁ +-α ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ id ≈⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ + G.₁ +-α ∘ ⊲ ∘ (G.₁ i₁ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ G.₁ i₂ ≈⟨ extendʳ (⇒⊲ +-α) ⟩ + ⊲ ∘ G.₁ +-α ⊗₁ G.₁ +-α ∘ (G.₁ i₁ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ G.₁ i₂ ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + ⊲ ∘ (G.₁ +-α ∘ G.₁ i₁ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ (G.₁ +-α ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ pullˡ (Equiv.sym G.homomorphism) ⟩⊗⟨ [ G ]-resp-square +-α∘i₂ ⟩ + ⊲ ∘ (G.₁ (+-α 𝒞.∘ i₁) ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ extendʳ (⇒⊲ (+-α 𝒞.∘ i₁)) ⟩⊗⟨refl ⟩ + ⊲ ∘ (⊲ ∘ G.₁ (+-α 𝒞.∘ i₁) ⊗₁ G.₁ (+-α 𝒞.∘ i₁) ∘ _) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩⊗⟨refl ⟨ + ⊲ ∘ (⊲ ∘ _ ⊗₁ (G.₁ (+-α 𝒞.∘ i₁) ∘ G.₁ i₂)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ [ G ]-resp-∘ +-α∘i₁∘i₁ ⟩⊗⟨ [ G ]-resp-square +-α∘i₁∘i₂) ⟩⊗⟨refl ⟩ + ⊲ ∘ (⊲ ∘ G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ split₁ˡ ⟩ + ⊲ ∘ ⊲ ⊗₁ id ∘ (G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ extendʳ (μ-assoc (M.₀ (n + (m + o)))) ⟩ + ⊲ ∘ (id ⊗₁ ⊲ ∘ α⇒) ∘ (G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ assoc ⟩ + ⊲ ∘ id ⊗₁ ⊲ ∘ α⇒ ∘ (G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ G.₁ i₁)) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-commute-from ⟩ + ⊲ ∘ id ⊗₁ ⊲ ∘ G.₁ i₁ ⊗₁ ((G.₁ i₂ ∘ G.₁ i₁) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂)) ∘ α⇒ ≈⟨ refl⟩∘⟨ pullˡ merge₂ˡ ⟩ + ⊲ ∘ G.₁ i₁ ⊗₁ (⊲ ∘ (G.₁ i₂ ∘ G.₁ i₁) ⊗₁ (G.₁ i₂ ∘ G.₁ i₂)) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (refl⟩∘⟨ ⊗-distrib-over-∘) ⟩∘⟨refl ⟩ + ⊲ ∘ G.₁ i₁ ⊗₁ (⊲ ∘ G.₁ i₂ ⊗₁ G.₁ i₂ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ (extendʳ (⇒⊲ i₂)) ⟩∘⟨refl ⟨ + ⊲ ∘ G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ ⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ α⇒ ≈⟨ pushʳ (pushˡ split₂ʳ) ⟩ + (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ id ⊗₁ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ α⇒ ∎ + where + +-α : (n + m) + o 𝒞.⇒ n + (m + o) + +-α = +-assoc.to {n} {m} {o} + + module _ {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) where + + ⊲-εʳ : ⊲ ∘ G.₁ f ⊗₁ ε ≈ G.₁ f ∘ ρ⇒ + ⊲-εʳ = begin + ⊲ ∘ G.₁ f ⊗₁ ε ≈⟨ refl⟩∘⟨ serialize₂₁ ⟩ + ⊲ ∘ id ⊗₁ ε ∘ G.₁ f ⊗₁ id ≈⟨ pullˡ (Equiv.sym (μ-identityʳ (M.₀ B))) ⟩ + ρ⇒ ∘ G.₁ f ⊗₁ id ≈⟨ unitorʳ-commute-from ⟩ + G.₁ f ∘ ρ⇒ ∎ + + ⊲-εˡ : ⊲ ∘ ε ⊗₁ G.₁ f ≈ G.₁ f ∘ λ⇒ + ⊲-εˡ = begin + ⊲ ∘ ε ⊗₁ G.₁ f ≈⟨ refl⟩∘⟨ serialize₁₂ ⟩ + ⊲ ∘ ε ⊗₁ id ∘ id ⊗₁ G.₁ f ≈⟨ pullˡ (Equiv.sym (μ-identityˡ (M.₀ B))) ⟩ + λ⇒ ∘ id ⊗₁ G.₁ f ≈⟨ unitorˡ-commute-from ⟩ + G.₁ f ∘ λ⇒ ∎ + + module _ {n : 𝒞.Obj} where + + ⊲-⊗-λ : G.₁ (+-λ.from {n}) ∘ ⊲-⊗ ∘ ε ⊗₁ id ≈ λ⇒ + ⊲-⊗-λ = begin + G.₁ +-λ.from ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ ε ⊗₁ id ≈⟨ refl⟩∘⟨ pullʳ merge₁ʳ ⟩ + G.₁ +-λ.from ∘ ⊲ ∘ (G.₁ i₁ ∘ ε) ⊗₁ G.₁ i₂ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⇒ε i₁ ⟩⊗⟨refl ⟩ + G.₁ +-λ.from ∘ ⊲ ∘ ε ⊗₁ G.₁ i₂ ≈⟨ refl⟩∘⟨ ⊲-εˡ i₂ ⟩ + G.₁ +-λ.from ∘ G.₁ i₂ ∘ λ⇒ ≈⟨ cancelˡ ([ G ]-resp-∘ +-λ∘i₂ ○ G.identity) ⟩ + λ⇒ ∎ + + ⊲-⊗-ρ : G.₁ (+-ρ.from {n}) ∘ ⊲-⊗ ∘ id ⊗₁ ε ≈ ρ⇒ + ⊲-⊗-ρ = begin + G.₁ +-ρ.from ∘ (⊲ ∘ G.₁ i₁ ⊗₁ G.₁ i₂) ∘ id ⊗₁ ε ≈⟨ refl⟩∘⟨ pullʳ merge₂ʳ ⟩ + G.₁ +-ρ.from ∘ ⊲ ∘ G.₁ i₁ ⊗₁ (G.₁ i₂ ∘ ε) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⇒ε i₂ ⟩ + G.₁ +-ρ.from ∘ ⊲ ∘ G.₁ i₁ ⊗₁ ε ≈⟨ refl⟩∘⟨ ⊲-εʳ i₁ ⟩ + G.₁ +-ρ.from ∘ G.₁ i₁ ∘ ρ⇒ ≈⟨ cancelˡ ([ G ]-resp-∘ +-ρ∘i₁ ○ G.identity) ⟩ + ρ⇒ ∎ + +F,⊗,ε : MonoidalFunctor 𝒞-MC S +F,⊗,ε = record + { F = G + ; isMonoidal = record + { ε = ε + ; ⊗-homo = ⊲-⊗-homo + ; associativity = ⊲-⊗-α + ; unitaryˡ = ⊲-⊗-λ + ; unitaryʳ = ⊲-⊗-ρ + } + } + +module F,⊗,ε = MonoidalFunctor F,⊗,ε diff --git a/Functor/Monoidal/Construction/MultisetOf.agda b/Functor/Monoidal/Construction/MultisetOf.agda new file mode 100644 index 0000000..83bdf52 --- /dev/null +++ b/Functor/Monoidal/Construction/MultisetOf.agda @@ -0,0 +1,89 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_) +open import Category.Construction.CMonoids using (CMonoids) + +open import Level using (Level) + +module Functor.Monoidal.Construction.MultisetOf + {o o′ ℓ ℓ′ e e′ : Level} + {𝒞 : CocartesianCategory o ℓ e} + {S : SymmetricMonoidalCategory o′ ℓ′ e′} + (let module 𝒞 = CocartesianCategory 𝒞) + (let module S = SymmetricMonoidalCategory S) + (G : Functor 𝒞.U S.U) + (M : Functor S.U (CMonoids S.symmetric)) + where + +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +import Categories.Category.Monoidal.Utilities as ⊗-Util +import Categories.Morphism.Reasoning as ⇒-Reasoning +import Object.Monoid.Commutative as CMonoidObject + +open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal) +open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands) +open import Categories.Functor.Monoidal using (MonoidalFunctor) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.Functor.Properties using ([_]-resp-∘) +open import Data.Product using (_,_) + +module G = Functor G +module M = Functor M +module 𝒞-SM = CocartesianSymmetricMonoidal 𝒞.U 𝒞.cocartesian + +open 𝒞 using (⊥; -+-; _+_; _+₁_; i₁; i₂; inject₁; inject₂; +-swap) +open Lax using (SymmetricMonoidalFunctor) + +open S +open Functor +open CMonoidObject symmetric using (CommutativeMonoid; CommutativeMonoid⇒) +open CommutativeMonoid renaming (assoc to μ-assoc; identityˡ to μ-identityˡ; identityʳ to μ-identityʳ; commutative to μ-commutative) +open CommutativeMonoid⇒ + +Forget : Functor (CMonoids symmetric) (Monoids monoidal) +Forget .F₀ = monoid +Forget .F₁ = monoid⇒ +Forget .identity = Equiv.refl +Forget .homomorphism = Equiv.refl +Forget .F-resp-≈ x = x + +𝒞-SMC : SymmetricMonoidalCategory o ℓ e +𝒞-SMC = record { symmetric = 𝒞-SM.+-symmetric } + +open import Functor.Monoidal.Construction.ListOf {𝒞 = 𝒞} G (Forget ∙ M) + using (List∘G; ListOf,++,[]; module LG; ++; module List; ++⇒) + +open Shorthands symmetric + +++-swap : {A : Obj} → ++ {A} ≈ ++ ∘ σ⇒ +++-swap {A} = μ-commutative (M.₀ A) + +open ⇒-Reasoning U +open ⊗-Reasoning monoidal + +++-⊗-σ + : {X Y : 𝒞.Obj} + → LG.₁ (+-swap {X} {Y}) ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ + ≈ (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ σ⇒ +++-⊗-σ {X} {Y} = begin + LG.₁ +-swap ∘ ++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ ≈⟨ extendʳ (++⇒ (G.₁ +-swap)) ⟩ + ++ ∘ LG.₁ +-swap ⊗₁ LG.₁ +-swap ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂ ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨ + ++ ∘ (LG.₁ +-swap ∘ LG.₁ i₁) ⊗₁ (LG.₁ +-swap ∘ LG.₁ i₂) ≈⟨ refl⟩∘⟨ [ List∘G ]-resp-∘ inject₁ ⟩⊗⟨ [ List∘G ]-resp-∘ inject₂ ⟩ + ++ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₁ ≈⟨ pushˡ ++-swap ⟩ + ++ ∘ σ⇒ ∘ LG.₁ i₂ ⊗₁ LG.₁ i₁ ≈⟨ pushʳ (braiding.⇒.commute (LG.₁ i₂ , LG.₁ i₁ )) ⟩ + (++ ∘ LG.₁ i₁ ⊗₁ LG.₁ i₂) ∘ σ⇒ ∎ + +open SymmetricMonoidalFunctor + +module ListOf,++,[] = MonoidalFunctor ListOf,++,[] + +MultisetOf,++,[] : SymmetricMonoidalFunctor 𝒞-SMC S +MultisetOf,++,[] .F = List∘G +MultisetOf,++,[] .isBraidedMonoidal = record + { isMonoidal = ListOf,++,[].isMonoidal + ; braiding-compat = ++-⊗-σ + } diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda new file mode 100644 index 0000000..1b45a75 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Circ.agda @@ -0,0 +1,87 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_; 0ℓ; suc) + +module Functor.Monoidal.Instance.Nat.Circ where + +import Categories.Object.Monoid as MonoidObject +import Data.Permutation.Sort as ↭-Sort +import Function.Reasoning as →-Reasoning + +open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×) +import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning +open import Category.Monoidal.Instance.Nat using (Nat,+,0) +open import Categories.Category.Construction.Monoids using (Monoids) +open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Data.Setoid.Unit using (⊤ₛ) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.Cartesian using (Cartesian) +open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Functor using (_∘F_) +open BinaryProducts products using (-×-) +open import Categories.Category.Product using (_⁂_) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Categories.Functor.Monoidal.Symmetric using (module Lax) +open import Categories.Functor using (Functor) +open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Circuit using (Circuit; Circuitₛ; mkCircuit; mkCircuitₛ; _≈_; mk≈; map) +open import Data.Circuit.Gate using (Gates) +open import Data.Nat using (ℕ; _+_) +open import Data.Product using (_,_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; _∘_; id) +open import Functor.Instance.Nat.Circ {suc 0ℓ} using (Circ; module Multiset∘Edge) +open import Functor.Instance.Nat.Edge {suc 0ℓ} using (Edge) +open import Function.Construct.Setoid using (_∙_) + +module Setoids-× = SymmetricMonoidalCategory Setoids-× + +open import Functor.Instance.FreeCMonoid {suc 0ℓ} {suc 0ℓ} using (FreeCMonoid) + +Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ +Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian } + +open import Functor.Monoidal.Construction.MultisetOf + {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (MultisetOf,++,[]) + +open Lax using (SymmetricMonoidalFunctor) + +module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[] + +open SymmetricMonoidalFunctor + +ε⇒ : ⊤ₛ ⟶ₛ Circuitₛ 0 +ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε + +open Cocartesian Nat-Cocartesian using (-+-) + +open Func + +η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m) +η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (MultisetOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y)) +η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (MultisetOf,++,[].⊗-homo.η (n , m)) (x , y)) + +⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → η {n} {m} + ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (MultisetOf,++,[].⊗-homo.commute (f , g) {X , Y}) } + } + +Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-× +Circ,⊗,ε .F = Circ +Circ,⊗,ε .isBraidedMonoidal = record + { isMonoidal = record + { ε = ε⇒ + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} → + mk≈ (MultisetOf,++,[].associativity {n} {m} {o} {(x , y) , z}) } + ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (MultisetOf,++,[].unitaryˡ {n} {_ , x}) } + ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (MultisetOf,++,[].unitaryʳ {n} {x , _}) } + } + ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} → + mk≈ (MultisetOf,++,[].braiding-compat {n} {m} {x , y}) } + } diff --git a/Functor/Monoidal/Instance/Nat/Preimage.agda b/Functor/Monoidal/Instance/Nat/Preimage.agda new file mode 100644 index 0000000..844df79 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Preimage.agda @@ -0,0 +1,164 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.Preimage where + +open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Data.Setoid.Unit using (⊤ₛ) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using (_∘F_) +open import Data.Subset.Functional using (Subset) +open import Data.Nat.Base using (ℕ; _+_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Product.Base using (_,_; _×_; Σ) +open import Data.Vec.Functional using ([]; _++_) +open import Data.Vec.Functional.Properties using (++-cong) +open import Data.Vec.Functional using (Vector; []) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Functor.Instance.Nat.Preimage using (Preimage; Subsetₛ) +open import Level using (0ℓ) + +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) +open BinaryProducts products using (-×-) +open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-swap; +₁∘+-swap) +open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) + +open import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_) +open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ) +open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂) +open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘) +open import Data.Fin.Preimage using (preimage) +open import Function.Base using (_∘_; id) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) +open import Data.Bool.Base using (Bool) + +open Func +Preimage-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0 +to Preimage-ε x = [] +cong Preimage-ε x () + +++ₛ : {n m : ℕ} → Subsetₛ n ×ₛ Subsetₛ m ⟶ₛ Subsetₛ (n + m) +to ++ₛ (xs , ys) = xs ++ ys +cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys + +preimage-++ + : {n n′ m m′ : ℕ} + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + {xs : Subset n′} + {ys : Subset m′} + → preimage f xs ++ preimage g ys ≗ preimage (f +₁ g) (xs ++ ys) +preimage-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin + (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨ + [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨ + [ xs , ys ]′ (splitAt n′ (join n′ m′ (map f g (splitAt n e)))) ≡⟨ ≡.cong ([ xs , ys ]′ ∘ splitAt n′) ([,]-map (splitAt n e)) ⟩ + [ xs , ys ]′ (splitAt n′ ((f +₁ g) e)) ∎ + where + open ≡-Reasoning + +⊗-homomorphism : NaturalTransformation (-×- ∘F (Preimage ⁂ Preimage)) (Preimage ∘F -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → ++ₛ {n} {m} + ; commute = λ { {n′ , m′} {n , m} (f , g) {xs , ys} e → preimage-++ f g e } + } + +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Lax) +open Lax using (SymmetricMonoidalFunctor) + +++-assoc + : {m n o : ℕ} + (X : Subset m) + (Y : Subset n) + (Z : Subset o) + → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z) +++-assoc {m} {n} {o} X Y Z i = begin + ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩ + [ [ X , Y ]′ ∘ splitAt m , Z ]′ (splitAt (m + n) (+-assocʳ {m} i)) ≡⟨ [,]-cong ([,]-cong (inv ∘ X) (inv ∘ Y) ∘ splitAt m) (inv ∘ Z) (splitAt (m + n) (+-assocʳ {m} i)) ⟨ + [ [ b ∘ X′ , b ∘ Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [-,]-cong ([,]-∘ b ∘ splitAt m) (splitAt (m + n) (+-assocʳ {m} i)) ⟨ + [ b ∘ [ X′ , Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [,]-∘ b (splitAt (m + n) (+-assocʳ {m} i)) ⟨ + b ([ [ X′ , Y′ ]′ ∘ splitAt m , Z′ ]′ (splitAt _ (+-assocʳ {m} i))) ≡⟨ ≡.cong b ([]∘assocʳ {2} {m} i) ⟩ + b ([ X′ , [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩ + [ b ∘ X′ , b ∘ [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ b ∘ splitAt n) (splitAt m i) ⟩ + [ b ∘ X′ , [ b ∘ Y′ , b ∘ Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ X) ([,]-cong (inv ∘ Y) (inv ∘ Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ + (X ++ (Y ++ Z)) i ∎ + where + open Bool + open Fin + f : Bool → Fin 2 + f false = zero + f true = suc zero + b : Fin 2 → Bool + b zero = false + b (suc zero) = true + inv : b ∘ f ≗ id + inv false = ≡.refl + inv true = ≡.refl + X′ : Fin m → Fin 2 + X′ = f ∘ X + Y′ : Fin n → Fin 2 + Y′ = f ∘ Y + Z′ : Fin o → Fin 2 + Z′ = f ∘ Z + open ≡-Reasoning + +Preimage-unitaryˡ + : {n : ℕ} + (X : Subset n) + → (X ++ []) ∘ (_↑ˡ 0) ≗ X +Preimage-unitaryˡ {n} X i = begin + [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩ + [ X , [] ]′ (inj₁ i) ≡⟨⟩ + X i ∎ + where + open ≡-Reasoning + +++-swap + : {n m : ℕ} + (X : Subset n) + (Y : Subset m) + → (X ++ Y) ∘ +-swap {n} ≗ Y ++ X +++-swap {n} {m} X Y i = begin + [ X , Y ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-cong (inv ∘ X) (inv ∘ Y) (splitAt n (+-swap {n} i)) ⟨ + [ b ∘ X′ , b ∘ Y′ ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-∘ b (splitAt n (+-swap {n} i)) ⟨ + b ([ X′ , Y′ ]′ (splitAt n (+-swap {n} i))) ≡⟨ ≡.cong b ([]∘swap {2} {n} i) ⟩ + b ([ Y′ , X′ ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩ + [ b ∘ Y′ , b ∘ X′ ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ Y) (inv ∘ X) (splitAt m i) ⟩ + [ Y , X ]′ (splitAt m i) ∎ + where + open Bool + open Fin + f : Bool → Fin 2 + f false = zero + f true = suc zero + b : Fin 2 → Bool + b zero = false + b (suc zero) = true + inv : b ∘ f ≗ id + inv false = ≡.refl + inv true = ≡.refl + X′ : Fin n → Fin 2 + X′ = f ∘ X + Y′ : Fin m → Fin 2 + Y′ = f ∘ Y + open ≡-Reasoning + +open SymmetricMonoidalFunctor +Preimage,++,[] : SymmetricMonoidalFunctor +Preimage,++,[] .F = Preimage +Preimage,++,[] .isBraidedMonoidal = record + { isMonoidal = record + { ε = Preimage-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i } + ; unitaryˡ = λ _ → ≡.refl + ; unitaryʳ = λ { {n} {X , _} i → Preimage-unitaryˡ X i } + } + ; braiding-compat = λ { {n} {m} {X , Y} i → ++-swap X Y i } + } diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda new file mode 100644 index 0000000..b267f97 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Pull.agda @@ -0,0 +1,166 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.Pull where + +import Categories.Morphism as Morphism + +open import Level using (0ℓ; Level) + +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian) + +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Data.Setoid.Unit using (⊤ₛ) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using (_∘F_) +open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper) +open import Data.Circuit.Value using (Monoid) +open import Data.Vector using (++-assoc) +open import Data.Fin.Base using (Fin; splitAt; join) +open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_) +open import Data.Fin.Preimage using (preimage) +open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ; splitAt-↑ʳ; join-splitAt) +open import Data.Nat.Base using (ℕ; _+_) +open import Data.Product.Base using (_,_; _×_; Σ; proj₁; proj₂) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) +open import Data.Subset.Functional using (Subset) +open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂) +open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘) +open import Data.System.Values Monoid using (Values; <ε>; []-unique; _++_; ++ₛ; splitₛ; _≋_; []) +open import Data.Unit.Polymorphic using (tt) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_) +open import Function.Construct.Constant using () renaming (function to Const) +open import Functor.Instance.Nat.Pull using (Pull; Pull-defs) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) + +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) + +open BinaryProducts products using (-×-) +open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-comm; +-swap; +₁∘+-swap; i₁; i₂) +open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) +open Func +open Morphism (Setoids-×.U) using (_≅_; module Iso) +open Strong using (SymmetricMonoidalFunctor) +open ≡-Reasoning + +private + + open _≅_ + open Iso + + Pull-ε : ⊤ₛ ≅ Values 0 + from Pull-ε = Const ⊤ₛ (Values 0) [] + to Pull-ε = Const (Values 0) ⊤ₛ tt + isoˡ (iso Pull-ε) = tt + isoʳ (iso Pull-ε) {x} = []-unique [] x + + opaque + unfolding _++_ + unfolding Pull-defs + Pull-++ + : {n n′ m m′ : ℕ} + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + {xs : ∣ Values n′ ∣} + {ys : ∣ Values m′ ∣} + → (Pull.₁ f ⟨$⟩ xs) ++ (Pull.₁ g ⟨$⟩ ys) ≋ Pull.₁ (f +₁ g) ⟨$⟩ (xs ++ ys) + Pull-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin + (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨ + [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨ + (xs ++ ys) (join n′ m′ (map f g (splitAt n e))) ≡⟨ ≡.cong (xs ++ ys) ([,]-map (splitAt n e)) ⟩ + (xs ++ ys) ((f +₁ g) e) ∎ + + module _ {n m : ℕ} where + + opaque + unfolding splitₛ + + open import Function.Construct.Setoid using (setoid) + open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_) + open import Function.Construct.Setoid using (_∙_) + open import Function.Construct.Identity using () renaming (function to Id) + + split∘++ : splitₛ ∙ ++ₛ ≈ Id (Values n ×ₛ Values m) + split∘++ {xs , ys} .proj₁ i = ≡.cong [ xs , ys ]′ (splitAt-↑ˡ n i m) + split∘++ {xs , ys} .proj₂ i = ≡.cong [ xs , ys ]′ (splitAt-↑ʳ n m i) + + ++∘split : ++ₛ {n} ∙ splitₛ ≈ Id (Values (n + m)) + ++∘split {x} i = ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i)) + + ⊗-homomorphism : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-) + ⊗-homomorphism = niHelper record + { η = λ (n , m) → ++ₛ {n} {m} + ; η⁻¹ = λ (n , m) → splitₛ {n} {m} + ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} → Pull-++ f g } + ; iso = λ (n , m) → record + { isoˡ = split∘++ + ; isoʳ = ++∘split + } + } + + module _ {n m : ℕ} where + + opaque + unfolding Pull-++ + + Pull-i₁ + : (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → Pull.₁ i₁ ⟨$⟩ (X ++ Y) ≋ X + Pull-i₁ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) + + Pull-i₂ + : (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → Pull.₁ i₂ ⟨$⟩ (X ++ Y) ≋ Y + Pull-i₂ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) + + opaque + unfolding Pull-++ + + Push-assoc + : {m n o : ℕ} + (X : ∣ Values m ∣) + (Y : ∣ Values n ∣) + (Z : ∣ Values o ∣) + → Pull.₁ (+-assocʳ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z) ≋ X ++ (Y ++ Z) + Push-assoc {m} {n} {o} X Y Z i = ++-assoc X Y Z i + + Pull-swap + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → Pull.₁ (+-swap {n}) ⟨$⟩ (X ++ Y) ≋ Y ++ X + Pull-swap {n} {m} X Y i = begin + ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩ + [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (Pull-i₂ X Y) (splitAt m i) ⟩ + [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (Pull-i₁ X Y) (splitAt m i) ⟩ + [ Y , X ]′ (splitAt m i) ≡⟨⟩ + (Y ++ X) i ∎ + +open SymmetricMonoidalFunctor + +Pull,++,[] : SymmetricMonoidalFunctor +Pull,++,[] .F = Pull +Pull,++,[] .isBraidedMonoidal = record + { isStrongMonoidal = record + { ε = Pull-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {_} {_} {_} {(X , Y) , Z} → Push-assoc X Y Z } + ; unitaryˡ = λ { {n} {_ , X} → Pull-i₂ {0} {n} [] X } + ; unitaryʳ = λ { {n} {X , _} → Pull-i₁ {n} {0} X [] } + } + ; braiding-compat = λ { {n} {m} {X , Y} → Pull-swap X Y } + } + +module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda new file mode 100644 index 0000000..2e8c0cf --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/Push.agda @@ -0,0 +1,209 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.Push where + +open import Categories.Category.Instance.Nat using (Nat) +open import Data.Bool.Base using (Bool; false) +open import Data.Subset.Functional using (Subset; ⁅_⁆; ⊥) +open import Function.Base using (_∘_; case_of_; _$_; id) +open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) +open import Level using (0ℓ; Level) +open import Relation.Binary using (Rel; Setoid) +open import Functor.Instance.Nat.Push using (Push; Push-defs) +open import Data.Setoid.Unit using (⊤ₛ) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) +open import Data.Vec.Functional as Vec using (Vector) +open import Data.Vector using (++-assoc; ++-↑ˡ; ++-↑ʳ) +-- open import Data.Vec.Functional.Properties using (++-cong) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Function.Construct.Constant using () renaming (function to Const) +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) +open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using () renaming (_∘F_ to _∘′_) +open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assoc; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Nat using (ℕ; _+_) +open import Data.Fin using (Fin) +open import Data.Product.Base using (_,_; _×_; Σ) +open import Data.Fin.Preimage using (preimage; preimage-⊥; preimage-cong₂) +open import Functor.Monoidal.Instance.Nat.Preimage using (preimage-++) +open import Data.Sum.Base using ([_,_]; [_,_]′; inj₁; inj₂) +open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map) +open import Data.Circuit.Merge using (merge-with; merge; merge-⊥; merge-[]; ⁅⁆-++; merge-++; merge-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆) +open import Data.Circuit.Value using (Value; join; join-comm; join-assoc; Monoid) +open import Data.Fin.Base using (splitAt; _↑ˡ_; _↑ʳ_) renaming (join to joinAt) +open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning) +open BinaryProducts products using (-×-) +open Value using (U) +open Bool using (false) + +open import Function.Bundles using (Equivalence) +open import Category.Monoidal.Instance.Nat using (Nat,+,0) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) +open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax) +open Lax using (SymmetricMonoidalFunctor) +open import Categories.Morphism Nat using (_≅_) +open import Function.Bundles using (Inverse) +open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_) +open Dual.op-binaryProducts using () renaming (assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap) +open import Relation.Nullary.Decidable using (does; does-⇔; dec-false) +open import Data.Setoid using (∣_∣) + +open ℕ + +open import Data.System.Values Monoid using (Values; <ε>; ++ₛ; _++_; head; tail; _≋_) + +open Func +open ≡-Reasoning + +private + + Push-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Values 0 + Push-ε = Const ⊤ₛ (Values 0) <ε> + + opaque + + unfolding _++_ + + unfolding Push-defs + Push-++ + : {n n′ m m′ : ℕ } + → (f : Fin n → Fin n′) + → (g : Fin m → Fin m′) + → (xs : ∣ Values n ∣) + → (ys : ∣ Values m ∣) + → (Push.₁ f ⟨$⟩ xs) ++ (Push.₁ g ⟨$⟩ ys) + ≋ Push.₁ (f +₁ g) ⟨$⟩ (xs ++ ys) + Push-++ {n} {n′} {m} {m′} f g xs ys i = begin + ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i + ≡⟨ [,]-cong left right (splitAt n′ i) ⟩ + [ (λ x → merge (xs ++ ys) _) , (λ x → merge (xs ++ ys) _) ]′ (splitAt n′ i) + ≡⟨ [,]-∘ (merge (xs ++ ys) ∘ (preimage (f +₁ g))) (splitAt n′ i) ⟨ + merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ Vec.++ ⊥++⁅⁆) i)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ {n′} i)) ⟩ + merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎ + where + ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′ + ⁅⁆++⊥ x = ⁅ x ⁆ Vec.++ ⊥ + ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′ + ⊥++⁅⁆ x = ⊥ Vec.++ ⁅ x ⁆ + left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥)) + left x = begin + merge xs (preimage f ⁅ x ⁆) ≡⟨ join-comm U (merge xs (preimage f ⁅ x ⁆)) ⟩ + join (merge xs (preimage f ⁅ x ⁆)) U ≡⟨ ≡.cong (join (merge _ _)) (merge-⊥ ys) ⟨ + join (merge xs (preimage f ⁅ x ⁆)) (merge ys ⊥) ≡⟨ ≡.cong (join (merge _ _)) (merge-cong₂ ys (preimage-⊥ g)) ⟨ + join (merge xs (preimage f ⁅ x ⁆)) (merge ys (preimage g ⊥)) ≡⟨ merge-++ xs ys (preimage f ⁅ x ⁆) (preimage g ⊥) ⟨ + merge (xs ++ ys) ((preimage f ⁅ x ⁆) Vec.++ (preimage g ⊥)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩ + merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥)) ∎ + right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆)) + right x = begin + merge ys (preimage g ⁅ x ⁆) ≡⟨⟩ + join U (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-⊥ xs) ⟨ + join (merge xs ⊥) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-cong₂ xs (preimage-⊥ f)) ⟨ + join (merge xs (preimage f ⊥)) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ merge-++ xs ys (preimage f ⊥) (preimage g ⁅ x ⁆) ⟨ + merge (xs ++ ys) ((preimage f ⊥) Vec.++ (preimage g ⁅ x ⁆)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩ + merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆)) ∎ + + ⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-) + ⊗-homomorphism = ntHelper record + { η = λ (n , m) → ++ₛ {n} {m} + ; commute = λ { (f , g) {xs , ys} → Push-++ f g xs ys } + } + + opaque + + unfolding Push-defs + unfolding _++_ + + Push-assoc + : {m n o : ℕ} + (X : ∣ Values m ∣) + (Y : ∣ Values n ∣) + (Z : ∣ Values o ∣) + → (Push.₁ (+-assocˡ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z)) ≋ X ++ Y ++ Z + Push-assoc {m} {n} {o} X Y Z i = begin + merge ((X ++ Y) ++ Z) (preimage (+-assocˡ {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ ↔-mno ((X ++ Y) ++ Z) ⁅ i ⁆ ⟩ + merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (⁅ i ⁆) ≡⟨⟩ + merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (preimage id ⁅ i ⁆) ≡⟨ merge-cong₁ (++-assoc X Y Z) (preimage id ⁅ i ⁆) ⟩ + merge (X ++ (Y ++ Z)) (preimage id ⁅ i ⁆) ≡⟨ Push.identity i ⟩ + (X ++ (Y ++ Z)) i ∎ + where + open Inverse + module +-assoc = _≅_ (+-assoc {m} {n} {o}) + ↔-mno : Permutation ((m + n) + o) (m + (n + o)) + ↔-mno .to = +-assocˡ {m} + ↔-mno .from = +-assocʳ {m} + ↔-mno .to-cong ≡.refl = ≡.refl + ↔-mno .from-cong ≡.refl = ≡.refl + ↔-mno .inverse = (λ { ≡.refl → +-assoc.isoˡ _ }) , λ { ≡.refl → +-assoc.isoʳ _ } + + Push-unitaryˡ + : {n : ℕ} + (X : ∣ Values n ∣) + → Push.₁ id ⟨$⟩ (<ε> ++ X) ≋ X + Push-unitaryˡ = merge-⁅⁆ + + preimage-++′ + : {n m o : ℕ} + (f : Vector (Fin o) n) + (g : Vector (Fin o) m) + (S : Subset o) + → preimage (f Vec.++ g) S ≗ preimage f S Vec.++ preimage g S + preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n + + Push-unitaryʳ + : {n : ℕ} + (X : ∣ Values n ∣) + → Push.₁ (id Vec.++ (λ())) ⟨$⟩ (X ++ (<ε> {0})) ≋ X + Push-unitaryʳ {n} X i = begin + merge (X ++ <ε>) (preimage (id Vec.++ (λ ())) ⁅ i ⁆) ≡⟨ merge-cong₂ (X Vec.++ <ε>) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩ + merge (X ++ <ε>) (⁅ i ⁆ Vec.++ preimage (λ ()) ⁅ i ⁆) ≡⟨ merge-++ X <ε> ⁅ i ⁆ (preimage (λ ()) ⁅ i ⁆) ⟩ + join (merge X ⁅ i ⁆) (merge <ε> (preimage (λ ()) ⁅ i ⁆)) ≡⟨ ≡.cong (join (merge X ⁅ i ⁆)) (merge-[] <ε> (preimage (λ ()) ⁅ i ⁆)) ⟩ + join (merge X ⁅ i ⁆) U ≡⟨ join-comm (merge X ⁅ i ⁆) U ⟩ + merge X ⁅ i ⁆ ≡⟨ merge-⁅⁆ X i ⟩ + X i ∎ + + Push-swap + : {n m : ℕ} + (X : ∣ Values n ∣) + (Y : ∣ Values m ∣) + → Push.₁ (+-swap {m}) ⟨$⟩ (X ++ Y) ≋ (Y ++ X) + Push-swap {n} {m} X Y i = begin + merge (X ++ Y) (preimage (+-swap {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ n+m↔m+n (X ++ Y) ⁅ i ⁆ ⟩ + merge ((X ++ Y) ∘ +-swap {n}) ⁅ i ⁆ ≡⟨ merge-⁅⁆ ((X ++ Y) ∘ (+-swap {n})) i ⟩ + ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩ + [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩ + [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ Y , X ]′ (splitAt m i) ≡⟨⟩ + (Y ++ X) i ∎ + where + open ≡-Reasoning + open Inverse + module +-swap = _≅_ (+-comm {m} {n}) + n+m↔m+n : Permutation (n + m) (m + n) + n+m↔m+n .to = +-swap.to + n+m↔m+n .from = +-swap.from + n+m↔m+n .to-cong ≡.refl = ≡.refl + n+m↔m+n .from-cong ≡.refl = ≡.refl + n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ }) + +open SymmetricMonoidalFunctor +Push,++,[] : SymmetricMonoidalFunctor +Push,++,[] .F = Push +Push,++,[] .isBraidedMonoidal = record + { isMonoidal = record + { ε = Push-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {n} {m} {o} {(X , Y) , Z} → Push-assoc X Y Z } + ; unitaryˡ = λ { {n} {_ , X} → Push-unitaryˡ X } + ; unitaryʳ = λ { {n} {X , _} → Push-unitaryʳ X } + } + ; braiding-compat = λ { {n} {m} {X , Y} → Push-swap X Y } + } + +module Push,++,[] = SymmetricMonoidalFunctor Push,++,[] diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda new file mode 100644 index 0000000..6659fb3 --- /dev/null +++ b/Functor/Monoidal/Instance/Nat/System.agda @@ -0,0 +1,394 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Monoidal.Instance.Nat.System where + +import Categories.Category.Monoidal.Utilities as ⊗-Util +import Data.Circuit.Value as Value +import Data.Vec.Functional as Vec +import Relation.Binary.PropositionalEquality as ≡ + +open import Level using (0ℓ; suc; Level) + +open import Category.Monoidal.Instance.Nat using (Nat,+,0; Natop,+,0) +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×) +open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×) + +module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B) +module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B) + +open import Functor.Monoidal.Instance.Nat.Pull using (Pull,++,[]) +open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using (module Strong) + +Pull,++,[]B : Strong.BraidedMonoidalFunctor +Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } +module Pull,++,[]B = Strong.BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }) + +open import Categories.Category.BinaryProducts using (module BinaryProducts) +open import Categories.Category.Cartesian using (Cartesian) +open import Categories.Category.Cocartesian using (Cocartesian) +open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian; Natop) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Data.Setoid.Unit using (⊤ₛ) +open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) +open import Categories.Category.Product using (Product) +open import Categories.Category.Product using (_⁂_) +open import Categories.Functor using (Functor) +open import Categories.Functor using (_∘F_) +open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax) +open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper) +open import Data.Circuit.Value using (Monoid) +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ; _+_) +open import Data.Product using (_,_; dmap; _×_) renaming (map to ×-map) +open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (_⇒ₛ_; ∣_∣) +open import Data.System {suc 0ℓ} using (Systemₛ; System; discrete; _≤_) +open import Data.System.Values Monoid using (++ₛ; splitₛ; Values; ++-cong; _++_; []) +open import Data.System.Values Value.Monoid using (_≋_; module ≋) +open import Data.Unit.Polymorphic using (⊤; tt) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id; case_of_) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_; setoid) +open import Functor.Instance.Nat.Pull using (Pull) +open import Functor.Instance.Nat.Push using (Push) +open import Functor.Instance.Nat.System using (Sys; Sys-defs) +open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv) +open import Functor.Monoidal.Instance.Nat.Push using (Push,++,[]) +open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv) +open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; unitaryˡ-inv; module Shorthands) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) + +open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_) + +open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products) + +open BinaryProducts products using (-×-) +open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap; +₁∘i₁; +₁∘i₂) +open Dual.op-binaryProducts using () renaming (×-assoc to +-assoc) +open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B) + +open Func + +Sys-ε : ⊤ₛ {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0 +Sys-ε = Const ⊤ₛ (Systemₛ 0) (discrete 0) + +private + + variable + n m o : ℕ + c₁ c₂ c₃ c₄ c₅ c₆ : Level + ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level + +_×-⇒_ + : {A : Setoid c₁ ℓ₁} + {B : Setoid c₂ ℓ₂} + {C : Setoid c₃ ℓ₃} + {D : Setoid c₄ ℓ₄} + {E : Setoid c₅ ℓ₅} + {F : Setoid c₆ ℓ₆} + → A ⟶ₛ B ⇒ₛ C + → D ⟶ₛ E ⇒ₛ F + → A ×ₛ D ⟶ₛ B ×ₛ E ⇒ₛ C ×ₛ F +_×-⇒_ f g .to (x , y) = to f x ×-function to g y +_×-⇒_ f g .cong (x , y) = cong f x , cong g y + +⊗ : System n × System m → System (n + m) +⊗ {n} {m} (S₁ , S₂) = record + { S = S₁.S ×ₛ S₂.S + ; fₛ = S₁.fₛ ×-⇒ S₂.fₛ ∙ splitₛ + ; fₒ = ++ₛ ∙ S₁.fₒ ×-function S₂.fₒ + } + where + module S₁ = System S₁ + module S₂ = System S₂ + +opaque + + _~_ : {A B : Setoid 0ℓ 0ℓ} → Func A B → Func A B → Set + _~_ = _≈_ + infix 4 _~_ + + sym-~ + : {A B : Setoid 0ℓ 0ℓ} + {x y : Func A B} + → x ~ y + → y ~ x + sym-~ {A} {B} {x} {y} = 0ℓ-Setoids-×.Equiv.sym {A} {B} {x} {y} + +⊗ₛ + : {n m : ℕ} + → Systemₛ n ×ₛ Systemₛ m ⟶ₛ Systemₛ (n + m) +⊗ₛ .to = ⊗ +⊗ₛ {n} {m} .cong {a , b} {c , d} ((a≤c , c≤a) , (b≤d , d≤b)) = left , right + where + module a = System a + module b = System b + module c = System c + module d = System d + module a≤c = _≤_ a≤c + module b≤d = _≤_ b≤d + module c≤a = _≤_ c≤a + module d≤b = _≤_ d≤b + + open _≤_ + left : ⊗ₛ ⟨$⟩ (a , b) ≤ ⊗ₛ ⟨$⟩ (c , d) + left .⇒S = a≤c.⇒S ×-function b≤d.⇒S + left .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (a≤c.≗-fₛ i₁) (b≤d.≗-fₛ i₂) + left .≗-fₒ = cong ++ₛ ∘ dmap a≤c.≗-fₒ b≤d.≗-fₒ + + right : ⊗ₛ ⟨$⟩ (c , d) ≤ ⊗ₛ ⟨$⟩ (a , b) + right .⇒S = c≤a.⇒S ×-function d≤b.⇒S + right .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (c≤a.≗-fₛ i₁) (d≤b.≗-fₛ i₂) + right .≗-fₒ = cong ++ₛ ∘ dmap c≤a.≗-fₒ d≤b.≗-fₒ + +opaque + + unfolding Sys-defs + + System-⊗-≤ + : {n n′ m m′ : ℕ} + (X : System n) + (Y : System m) + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + → ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y) ≤ Sys.₁ (f +₁ g) ⟨$⟩ ⊗ (X , Y) + System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record + { ⇒S = Id (X.S ×ₛ Y.S) + ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.sym-commute (f , g) {i}) {s} + ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂} + } + where + module X = System X + module Y = System Y + + System-⊗-≥ + : {n n′ m m′ : ℕ} + (X : System n) + (Y : System m) + (f : Fin n → Fin n′) + (g : Fin m → Fin m′) + → Sys.₁ (f +₁ g) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y) + System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record + { ⇒S = Id (X.S ×ₛ Y.S) + ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.commute (f , g) {i}) {s} + ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.sym-commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂} + } + where + module X = System X + module Y = System Y + +⊗-homomorphism : NaturalTransformation (-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → ⊗ₛ {n} {m} + ; commute = λ { (f , g) {X , Y} → System-⊗-≤ X Y f g , System-⊗-≥ X Y f g } + } + +opaque + + unfolding Sys-defs + + ⊗-assoc-≤ + : (X : System n) + (Y : System m) + (Z : System o) + → Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z)) ≤ ⊗ (X , ⊗ (Y , Z)) + ⊗-assoc-≤ {n} {m} {o} X Y Z = record + { ⇒S = assocˡ + ; ≗-fₛ = λ i ((s₁ , s₂) , s₃) → cong (X.fₛ ×-⇒ (Y.fₛ ×-⇒ Z.fₛ) ∙ assocˡ) (associativity-inv {x = i}) {s₁ , s₂ , s₃} + ; ≗-fₒ = λ ((s₁ , s₂) , s₃) → Push,++,[].associativity {x = (X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃} + } + where + open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products) + open BinaryProducts 0ℓ-products using (assocˡ) + + module X = System X + module Y = System Y + module Z = System Z + + ⊗-assoc-≥ + : (X : System n) + (Y : System m) + (Z : System o) + → ⊗ (X , ⊗ (Y , Z)) ≤ Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z)) + ⊗-assoc-≥ {n} {m} {o} X Y Z = record + { ⇒S = ×-assocʳ + ; ≗-fₛ = λ i (s₁ , s₂ , s₃) → cong ((X.fₛ ×-⇒ Y.fₛ) ×-⇒ Z.fₛ) (sym-split-assoc {i}) {(s₁ , s₂) , s₃} + ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃} + } + where + open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod) + open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ; assocˡ to ×-assocˡ) + + +-assocℓ : Fin ((n + m) + o) → Fin (n + (m + o)) + +-assocℓ = +-assocˡ {n} {m} {o} + + opaque + + unfolding _~_ + + associativity-inv-~ : splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ ~ ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ + associativity-inv-~ {i} = associativity-inv {n} {m} {o} {i} + + associativity-~ : Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) ~ ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ + associativity-~ {i} = Push,++,[].associativity {n} {m} {o} {i} + + sym-split-assoc-~ : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ~ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ + sym-split-assoc-~ = sym-~ associativity-inv-~ + + sym-++-assoc-~ : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ~ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) + sym-++-assoc-~ = sym-~ associativity-~ + + opaque + + unfolding _~_ + + sym-split-assoc : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ≈ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ + sym-split-assoc {i} = sym-split-assoc-~ {i} + + sym-++-assoc : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ≈ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) + sym-++-assoc {i} = sym-++-assoc-~ + + module X = System X + module Y = System Y + module Z = System Z + + Sys-unitaryˡ-≤ : (X : System n) → Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X)) ≤ X + Sys-unitaryˡ-≤ {n} X = record + { ⇒S = proj₂ₛ + ; ≗-fₛ = λ i (_ , s) → cong (X.fₛ ∙ proj₂ₛ {A = ⊤ₛ {0ℓ}}) (unitaryˡ-inv {n} {i}) + ; ≗-fₒ = λ (_ , s) → Push,++,[].unitaryˡ {n} {tt , X.fₒ′ s} + } + where + module X = System X + + Sys-unitaryˡ-≥ : (X : System n) → X ≤ Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X)) + Sys-unitaryˡ-≥ {n} X = record + { ⇒S = < Const X.S ⊤ₛ tt , Id X.S >ₛ + ; ≗-fₛ = λ i s → cong (disc.fₛ ×-⇒ X.fₛ ∙ ε⇒ ×-function Id (Values n)) (sym-split-unitaryˡ {i}) + ; ≗-fₒ = λ s → sym-++-unitaryˡ {_ , X.fₒ′ s} + } + where + module X = System X + open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv) + open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (λ⇐) + open Shorthands using (ε⇐; ε⇒) + module disc = System (discrete 0) + sym-split-unitaryˡ + : λ⇐ ≈ ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id) + sym-split-unitaryˡ = + 0ℓ-Setoids-×.Equiv.sym + {Values n} + {⊤ₛ ×ₛ Values n} + {ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)} + {λ⇐} + (unitaryˡ-inv {n}) + sym-++-unitaryˡ : proj₂ₛ {A = ⊤ₛ {0ℓ} {0ℓ}} ≈ Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n) + sym-++-unitaryˡ = + 0ℓ-Setoids-×.Equiv.sym + {⊤ₛ ×ₛ Values n} + {Values n} + {Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)} + {proj₂ₛ} + (Push,++,[].unitaryˡ {n}) + + + Sys-unitaryʳ-≤ : (X : System n) → Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0)) ≤ X + Sys-unitaryʳ-≤ {n} X = record + { ⇒S = proj₁ₛ + ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = ⊤ₛ {0ℓ}}) (unitaryʳ-inv {n} {i}) + ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt} + } + where + module X = System X + + Sys-unitaryʳ-≥ : (X : System n) → X ≤ Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0)) + Sys-unitaryʳ-≥ {n} X = record + { ⇒S = < Id X.S , Const X.S ⊤ₛ tt >ₛ + ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ disc.fₛ ∙ Id (Values n) ×-function ε⇒) sym-split-unitaryʳ {s , tt} + ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt} + } + where + module X = System X + module disc = System (discrete 0) + open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (ρ⇐) + open Shorthands using (ε⇐; ε⇒) + sym-split-unitaryʳ + : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ())) + sym-split-unitaryʳ = + 0ℓ-Setoids-×.Equiv.sym + {Values n} + {Values n ×ₛ ⊤ₛ} + {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))} + {ρ⇐} + (unitaryʳ-inv {n}) + sym-++-unitaryʳ : proj₁ₛ {B = ⊤ₛ {0ℓ}} ≈ Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε + sym-++-unitaryʳ = + 0ℓ-Setoids-×.Equiv.sym + {Values n ×ₛ ⊤ₛ} + {Values n} + {Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε} + {proj₁ₛ} + (Push,++,[].unitaryʳ {n}) + + Sys-braiding-compat-≤ + : (X : System n) + (Y : System m) + → Sys.₁ (+-swap {m} {n}) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Y , X) + Sys-braiding-compat-≤ {n} {m} X Y = record + { ⇒S = swapₛ + ; ≗-fₛ = λ i (s₁ , s₂) → cong (Y.fₛ ×-⇒ X.fₛ ∙ swapₛ) (braiding-compat-inv {m} {n} {i}) {s₂ , s₁} + ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].braiding-compat {n} {m} {X.fₒ′ s₁ , Y.fₒ′ s₂} + } + where + module X = System X + module Y = System Y + + Sys-braiding-compat-≥ + : (X : System n) + (Y : System m) + → ⊗ (Y , X) ≤ Sys.₁ (+-swap {m} {n}) ⟨$⟩ ⊗ (X , Y) + Sys-braiding-compat-≥ {n} {m} X Y = record + { ⇒S = swapₛ + ; ≗-fₛ = λ i (s₂ , s₁) → cong (X.fₛ ×-⇒ Y.fₛ) (sym-braiding-compat-inv {i}) + ; ≗-fₒ = λ (s₂ , s₁) → sym-braiding-compat-++ {X.fₒ′ s₁ , Y.fₒ′ s₂} + } + where + module X = System X + module Y = System Y + sym-braiding-compat-inv : swapₛ ∙ splitₛ {m} ≈ splitₛ ∙ Pull.₁ (+-swap {m} {n}) + sym-braiding-compat-inv {i} = + 0ℓ-Setoids-×.Equiv.sym + {Values (m + n)} + {Values n ×ₛ Values m} + {splitₛ ∙ Pull.₁ (+-swap {m} {n})} + {swapₛ ∙ splitₛ {m}} + (λ {j} → braiding-compat-inv {m} {n} {j}) {i} + sym-braiding-compat-++ : ++ₛ {m} ∙ swapₛ ≈ Push.₁ (+-swap {m} {n}) ∙ ++ₛ + sym-braiding-compat-++ {i} = + 0ℓ-Setoids-×.Equiv.sym + {Values n ×ₛ Values m} + {Values (m + n)} + {Push.₁ (+-swap {m} {n}) ∙ ++ₛ} + {++ₛ {m} ∙ swapₛ} + (Push,++,[].braiding-compat {n} {m}) + +open Lax.SymmetricMonoidalFunctor + +Sys,⊗,ε : Lax.SymmetricMonoidalFunctor +Sys,⊗,ε .F = Sys +Sys,⊗,ε .isBraidedMonoidal = record + { isMonoidal = record + { ε = Sys-ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {n} {m} {o} {(X , Y), Z} → ⊗-assoc-≤ X Y Z , ⊗-assoc-≥ X Y Z } + ; unitaryˡ = λ { {n} {_ , X} → Sys-unitaryˡ-≤ X , Sys-unitaryˡ-≥ X } + ; unitaryʳ = λ { {n} {X , _} → Sys-unitaryʳ-≤ X , Sys-unitaryʳ-≥ X } + } + ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y } + } + +module Sys,⊗,ε = Lax.SymmetricMonoidalFunctor Sys,⊗,ε diff --git a/Functor/Monoidal/Strong/Properties.agda b/Functor/Monoidal/Strong/Properties.agda new file mode 100644 index 0000000..9eb7579 --- /dev/null +++ b/Functor/Monoidal/Strong/Properties.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +open import Categories.Category.Monoidal using (MonoidalCategory) +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor) + +module Functor.Monoidal.Strong.Properties + {o o′ ℓ ℓ′ e e′ : Level} + {C : MonoidalCategory o ℓ e} + {D : MonoidalCategory o′ ℓ′ e′} + (F,φ,ε : StrongMonoidalFunctor C D) where + +import Categories.Category.Monoidal.Utilities as ⊗-Utilities +import Categories.Category.Construction.Core as Core + +open import Categories.Functor.Monoidal using (StrongMonoidalFunctor) +open import Categories.Functor.Properties using ([_]-resp-≅) + +private + + module C where + open MonoidalCategory C public + open ⊗-Utilities.Shorthands monoidal public using (α⇐; λ⇐; ρ⇐) + + module D where + open MonoidalCategory D public + open ⊗-Utilities.Shorthands monoidal using (α⇐; λ⇐; ρ⇐) public + open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) public + open ⊗-Utilities monoidal using (_⊗ᵢ_) public + +open D + +open StrongMonoidalFunctor F,φ,ε + +private + + variable + X Y Z : C.Obj + + α : {A B C : Obj} → (A ⊗₀ B) ⊗₀ C ≅ A ⊗₀ (B ⊗₀ C) + α = associator + + Fα : F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z)) + Fα = [ F ]-resp-≅ C.associator + + λ- : {A : Obj} → unit ⊗₀ A ≅ A + λ- = unitorˡ + + Fλ : F₀ (C.unit C.⊗₀ X) ≅ F₀ X + Fλ = [ F ]-resp-≅ C.unitorˡ + + ρ : {A : Obj} → A ⊗₀ unit ≅ A + ρ = unitorʳ + + Fρ : F₀ (X C.⊗₀ C.unit) ≅ F₀ X + Fρ = [ F ]-resp-≅ C.unitorʳ + + φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y) + φ = ⊗-homo.FX≅GX + +module Shorthands where + + φ⇒ : F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y) + φ⇒ = ⊗-homo.⇒.η _ + + φ⇐ : F₀ (X C.⊗₀ Y) ⇒ F₀ X ⊗₀ F₀ Y + φ⇐ = ⊗-homo.⇐.η _ + + ε⇒ : unit ⇒ F₀ C.unit + ε⇒ = ε.from + + ε⇐ : F₀ C.unit ⇒ unit + ε⇐ = ε.to + +open Shorthands +open HomReasoning + +associativityᵢ : Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α +associativityᵢ = ⌞ associativity ⌟ + +associativity-inv : φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.α⇐ {X} {Y} {Z}) ≈ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ +associativity-inv = begin + φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.α⇐ ≈⟨ sym-assoc ⟩ + (φ⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.α⇐ ≈⟨ to-≈ associativityᵢ ⟩ + (α⇐ ∘ id ⊗₁ φ⇐) ∘ φ⇐ ≈⟨ assoc ⟩ + α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ ∎ + +unitaryˡᵢ : Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ- +unitaryˡᵢ = ⌞ unitaryˡ ⌟ + +unitaryˡ-inv : ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.λ⇐ {X}) ≈ λ⇐ +unitaryˡ-inv = begin + ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.λ⇐ ≈⟨ sym-assoc ⟩ + (ε⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.λ⇐ ≈⟨ to-≈ unitaryˡᵢ ⟩ + λ⇐ ∎ + +unitaryʳᵢ : Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ +unitaryʳᵢ = ⌞ unitaryʳ ⌟ + +unitaryʳ-inv : id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ (C.ρ⇐ {X}) ≈ ρ⇐ +unitaryʳ-inv = begin + id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ C.ρ⇐ ≈⟨ sym-assoc ⟩ + (id ⊗₁ ε⇐ ∘ φ⇐) ∘ F₁ C.ρ⇐ ≈⟨ to-≈ unitaryʳᵢ ⟩ + ρ⇐ ∎ diff --git a/Functor/Properties.agda b/Functor/Properties.agda new file mode 100644 index 0000000..1bd3ba6 --- /dev/null +++ b/Functor/Properties.agda @@ -0,0 +1,77 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Properties where + +import Categories.Morphism.Reasoning as ⇒-Reasoning + +open import Categories.Category using (Category; _[_,_]) +open import Level using (Level) +open import Categories.Morphism.Notation using (_[_≅_]) +open import Categories.Morphism using (_≅_) +open import Categories.Functor using (Functor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) +open import Data.Product using (Σ-syntax; _,_) + +module _ + {o o′ ℓ ℓ′ e e′ : Level} + {𝒞 : Category o ℓ e} + {𝒟 : Category o′ ℓ′ e′} + where + + module 𝒞 = Category 𝒞 + module 𝒟 = Category 𝒟 + + define-by-pw-iso + : (F : Functor 𝒞 𝒟) + (G₀ : 𝒞.Obj → 𝒟.Obj) + → (let module F = Functor F) + → ((X : 𝒞.Obj) → 𝒟 [ F.₀ X ≅ G₀ X ]) + → Σ[ G ∈ Functor 𝒞 𝒟 ] F ≃ G + define-by-pw-iso F G₀ α = G , F≃G + where + open Functor + module F = Functor F + open 𝒟 + open _≅_ + open HomReasoning + open ⇒-Reasoning 𝒟 + + G-homo + : {X Y Z : 𝒞.Obj} + → (f : 𝒞 [ X , Y ]) + → (g : 𝒞 [ Y , Z ]) + → from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X) + ≈ (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X) + G-homo {X} {Y} {Z} f g = begin + from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X) ≈⟨ extendʳ (pushʳ F.homomorphism) ⟩ + (from (α Z) ∘ F.₁ g) ∘ F.₁ f ∘ to (α X) ≈⟨ extendˡ (pushˡ (insertʳ (isoˡ (α Y)))) ⟩ + (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X) ∎ + + G-resp-≈ + : {X Y : 𝒞.Obj} + → {f g : 𝒞 [ X , Y ]} + → f 𝒞.≈ g + → from (α Y) ∘ F.₁ f ∘ to (α X) + ≈ from (α Y) ∘ F.₁ g ∘ to (α X) + G-resp-≈ f≈g = refl⟩∘⟨ F.F-resp-≈ f≈g ⟩∘⟨refl + + G-identity : {X : 𝒞.Obj} → from (α X) ∘ F.₁ 𝒞.id ∘ to (α X) ≈ id + G-identity {X} = refl⟩∘⟨ (F.identity ⟩∘⟨refl ○ identityˡ) ○ isoʳ (α X) + + G : Functor 𝒞 𝒟 + G .F₀ = G₀ + G .F₁ {X} {Y} f = from (α Y) ∘ F.₁ f ∘ to (α X) + G .identity {X} = G-identity + G .homomorphism {f = f} {g} = G-homo f g + G .F-resp-≈ = G-resp-≈ + + commute : {X Y : 𝒞.Obj} (f : 𝒞 [ X , Y ]) → from (α Y) ∘ F.F₁ f ≈ (from (α Y) ∘ F.₁ f ∘ to (α X)) ∘ from (α X) + commute {X} {Y} f = pushʳ (insertʳ (isoˡ (α X))) + + F≃G : F ≃ G + F≃G = niHelper record + { η = λ X → from (α X) + ; η⁻¹ = λ X → to (α X) + ; commute = commute + ; iso = λ X → iso (α X) + } |