diff options
Diffstat (limited to 'Functor/Instance')
| -rw-r--r-- | Functor/Instance/Cospan/Embed.agda | 103 | ||||
| -rw-r--r-- | Functor/Instance/Cospan/Stack.agda | 96 | ||||
| -rw-r--r-- | Functor/Instance/Decorate.agda | 31 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Embed.agda | 10 | ||||
| -rw-r--r-- | Functor/Instance/DecoratedCospan/Stack.agda | 41 | ||||
| -rw-r--r-- | Functor/Instance/Endo/List.agda | 15 | ||||
| -rw-r--r-- | Functor/Instance/List.agda | 67 | ||||
| -rw-r--r-- | Functor/Instance/Monoidalize.agda | 43 | ||||
| -rw-r--r-- | Functor/Instance/Multiset.agda | 72 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 56 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 60 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Preimage.agda | 65 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 81 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 79 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 110 |
15 files changed, 786 insertions, 143 deletions
diff --git a/Functor/Instance/Cospan/Embed.agda b/Functor/Instance/Cospan/Embed.agda index 77f0361..6dbc04a 100644 --- a/Functor/Instance/Cospan/Embed.agda +++ b/Functor/Instance/Cospan/Embed.agda @@ -1,4 +1,5 @@ {-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) @@ -14,9 +15,10 @@ open import Categories.Category using (_[_,_]; _[_∘_]; _[_≈_]) open import Categories.Category.Core using (Category) open import Categories.Functor.Core using (Functor) open import Category.Instance.Cospans 𝒞 using (Cospans) +open import Category.Diagram.Cospan 𝒞 using (cospan) open import Data.Product.Base using (_,_) open import Function.Base using (id) -open import Functor.Instance.Cospan.Stack using (⊗) +open import Functor.Instance.Cospan.Stack 𝒞 using (⊗) module 𝒞 = FinitelyCocompleteCategory 𝒞 module Cospans = Category Cospans @@ -28,24 +30,26 @@ open Morphism U using (module ≅; _≅_) open PushoutProperties U using (up-to-iso) open Pushout′ U using (pushout-id-g; pushout-f-id) -L₁ : {A B : 𝒞.Obj} → U [ A , B ] → Cospans [ A , B ] -L₁ f = record - { f₁ = f - ; f₂ = 𝒞.id - } +private + variable + A B C : 𝒞.Obj + W X Y Z : 𝒞.Obj + +L₁ : U [ A , B ] → Cospans [ A , B ] +L₁ f = cospan f 𝒞.id -L-identity : {A : 𝒞.Obj} → L₁ 𝒞.id ≈ Cospans.id {A} +L-identity : L₁ 𝒞.id ≈ Cospans.id {A} L-identity = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identity² } -L-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] +L-homomorphism : {f : U [ X , Y ]} {g : U [ Y , Z ]} → L₁ (U [ g ∘ f ]) ≈ Cospans [ L₁ g ∘ L₁ f ] L-homomorphism {X} {Y} {Z} {f} {g} = record { ≅N = up-to-iso P′ P - ; from∘f₁≈f₁′ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) - ; from∘f₂≈f₂′ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₁≈f₁ = pullˡ (P′.universal∘i₁≈h₁ {eq = P.commute}) + ; from∘f₂≈f₂ = P′.universal∘i₂≈h₂ {eq = P.commute} ○ sym 𝒞.identityʳ } where open ⇒-Reasoning U @@ -57,11 +61,11 @@ L-homomorphism {X} {Y} {Z} {f} {g} = record module P = Pushout P module P′ = Pushout P′ -L-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] +L-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ L₁ f ≈ L₁ g ] L-resp-≈ {A} {B} {f} {g} f≈g = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ ○ f≈g - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identityˡ ○ f≈g + ; from∘f₂≈f₂ = 𝒞.identity² } where open 𝒞.HomReasoning @@ -75,24 +79,21 @@ L = record ; F-resp-≈ = L-resp-≈ } -R₁ : {A B : 𝒞.Obj} → U [ B , A ] → Cospans [ A , B ] -R₁ g = record - { f₁ = 𝒞.id - ; f₂ = g - } +R₁ : U [ B , A ] → Cospans [ A , B ] +R₁ g = cospan 𝒞.id g -R-identity : {A : 𝒞.Obj} → R₁ 𝒞.id ≈ Cospans.id {A} +R-identity : R₁ 𝒞.id ≈ Cospans.id {A} R-identity = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identity² + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identity² } -R-homomorphism : {X Y Z : 𝒞.Obj} {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] -R-homomorphism {X} {Y} {Z} {f} {g} = record +R-homomorphism : {f : U [ Y , X ]} {g : U [ Z , Y ]} → R₁ (U [ f ∘ g ]) ≈ Cospans [ R₁ g ∘ R₁ f ] +R-homomorphism {f} {g} = record { ≅N = up-to-iso P′ P - ; from∘f₁≈f₁′ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ - ; from∘f₂≈f₂′ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) + ; from∘f₁≈f₁ = P′.universal∘i₁≈h₁ {eq = P.commute} ○ sym 𝒞.identityʳ + ; from∘f₂≈f₂ = pullˡ (P′.universal∘i₂≈h₂ {eq = P.commute}) } where open ⇒-Reasoning U @@ -104,11 +105,11 @@ R-homomorphism {X} {Y} {Z} {f} {g} = record module P = Pushout P module P′ = Pushout P′ -R-resp-≈ : {A B : 𝒞.Obj} {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] -R-resp-≈ {A} {B} {f} {g} f≈g = record +R-resp-≈ : {f g : U [ A , B ]} → U [ f ≈ g ] → Cospans [ R₁ f ≈ R₁ g ] +R-resp-≈ {f} {g} f≈g = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identity² - ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ f≈g + ; from∘f₁≈f₁ = 𝒞.identity² + ; from∘f₂≈f₂ = 𝒞.identityˡ ○ f≈g } where open 𝒞.HomReasoning @@ -122,17 +123,11 @@ R = record ; F-resp-≈ = R-resp-≈ } -B₁ : {A B C : 𝒞.Obj} → U [ A , C ] → U [ B , C ] → Cospans [ A , B ] -B₁ f g = record - { f₁ = f - ; f₂ = g - } - -B∘L : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ B₁ g h ∘ L₁ f ] ≈ B₁ (U [ g ∘ f ]) h -B∘L {W} {X} {Y} {Z} {f} {g} {h} = record +B∘L : {f : U [ W , X ]} {g : U [ X , Y ]} {h : U [ Z , Y ]} → Cospans [ cospan g h ∘ L₁ f ] ≈ cospan (U [ g ∘ f ]) h +B∘L {f} {g} {h} = record { ≅N = up-to-iso P P′ - ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) - ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) + ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) ○ 𝒞.identityˡ } where open ⇒-Reasoning U @@ -144,11 +139,11 @@ B∘L {W} {X} {Y} {Z} {f} {g} {h} = record module P = Pushout P module P′ = Pushout P′ -R∘B : {W X Y Z : 𝒞.Obj} {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ B₁ f g ] ≈ B₁ f (U [ g ∘ h ]) -R∘B {W} {X} {Y} {Z} {f} {g} {h} = record +R∘B : {f : U [ W , X ]} {g : U [ Y , X ]} {h : U [ Z , Y ]} → Cospans [ R₁ h ∘ cospan f g ] ≈ cospan f (U [ g ∘ h ]) +R∘B {f} {g} {h} = record { ≅N = up-to-iso P P′ - ; from∘f₁≈f₁′ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ - ; from∘f₂≈f₂′ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) + ; from∘f₁≈f₁ = pullˡ (P.universal∘i₁≈h₁ {eq = P′.commute}) ○ 𝒞.identityˡ + ; from∘f₂≈f₂ = pullˡ (P.universal∘i₂≈h₂ {eq = P′.commute}) } where open ⇒-Reasoning U @@ -164,20 +159,18 @@ module _ where open _≅_ - ≅-L-R : ∀ {X Y : 𝒞.Obj} (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) - ≅-L-R {X} {Y} X≅Y = record + ≅-L-R : (X≅Y : X ≅ Y) → L₁ (to X≅Y) ≈ R₁ (from X≅Y) + ≅-L-R X≅Y = record { ≅N = X≅Y - ; from∘f₁≈f₁′ = isoʳ X≅Y - ; from∘f₂≈f₂′ = 𝒞.identityʳ + ; from∘f₁≈f₁ = isoʳ X≅Y + ; from∘f₂≈f₂ = 𝒞.identityʳ } -module ⊗ = Functor (⊗ 𝒞) - -L-resp-⊗ : {X Y X′ Y′ : 𝒞.Obj} {a : U [ X , X′ ]} {b : U [ Y , Y′ ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) -L-resp-⊗ {X} {Y} {X′} {Y′} {a} {b} = record +L-resp-⊗ : {a : U [ W , X ]} {b : U [ Y , Z ]} → L₁ (a +₁ b) ≈ ⊗.₁ (L₁ a , L₁ b) +L-resp-⊗ {a} {b} = record { ≅N = ≅.refl - ; from∘f₁≈f₁′ = 𝒞.identityˡ - ; from∘f₂≈f₂′ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) + ; from∘f₁≈f₁ = 𝒞.identityˡ + ; from∘f₂≈f₂ = 𝒞.identityˡ ○ sym +-η ○ sym ([]-cong₂ identityʳ identityʳ) } where open 𝒞.HomReasoning diff --git a/Functor/Instance/Cospan/Stack.agda b/Functor/Instance/Cospan/Stack.agda index 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 |