diff options
Diffstat (limited to 'Functor')
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 72 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 65 | ||||
| -rw-r--r-- | Functor/Instance/Nat/System.agda | 150 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Pull.agda | 290 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Push.agda | 428 | ||||
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/System.agda | 629 |
6 files changed, 744 insertions, 890 deletions
diff --git a/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda index 5b74399..b1764d9 100644 --- a/Functor/Instance/Nat/Pull.agda +++ b/Functor/Instance/Nat/Pull.agda @@ -14,50 +14,68 @@ 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 (Value) -open import Data.System.Values Value using (Values) +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 -_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ -_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) -infixr 4 _≈_ +-- 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 --- action on objects is Values n (Vector Value n) + -- Pull respects identity + Pull-identity : Pull₁ id ≈ Id (Values A) + Pull-identity {A} = Setoid.refl (Values A) --- 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 + opaque --- Pull respects identity -Pull-identity : Pull₁ id ≈ Id (Values A) -Pull-identity {A} = Setoid.refl (Values A) + unfolding Pull₁ --- Pull flips composition -Pull-homomorphism - : {A B C : ℕ} - (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 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 + -- 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} {v} = Pull-homomorphism g f {v} +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 index 53d0bef..8126006 100644 --- a/Functor/Instance/Nat/Push.agda +++ b/Functor/Instance/Nat/Push.agda @@ -17,43 +17,56 @@ 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 (Value) -open import Data.System.Values Value using (Values) +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 _≈_ + _≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ + _≈_ {X} {Y} = Setoid._≈_ (setoid X Y) + infixr 4 _≈_ + + opaque + + unfolding Values --- action of Push on objects is Values n (Vector Value n) + -- 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 ∘ ⁅_⁆ --- 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 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 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 ∘ ⁅_⁆ --- 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ℓ) @@ -62,3 +75,5 @@ 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 index 00451ad..05e1e7b 100644 --- a/Functor/Instance/Nat/System.agda +++ b/Functor/Instance/Nat/System.agda @@ -2,91 +2,103 @@ 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 (Value) +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; Systemₛ) -open import Data.System.Values Value using (module ≋) -open import Function.Bundles using (Func; _⟶ₛ_) +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₁; Pull-resp-≈) -open import Functor.Instance.Nat.Push using (Push₁; Push-identity; Push-homomorphism; Push-resp-≈) +open import Functor.Instance.Nat.Pull using (Pull) +open import Functor.Instance.Nat.Push using (Push) open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) --- import Relation.Binary.Reasoning.Setoid as ≈-Reasoning -import Function.Construct.Identity as Id - open Func -open ≤-System open Functor +open _≤_ private + variable A B C : ℕ -map : (Fin A → Fin B) → System A → System B -map f X = record - { S = S - ; fₛ = fₛ ∙ Pull₁ f - ; fₒ = Push₁ f ∙ fₒ - } - where - open System X - -≤-cong : (f : Fin A → Fin B) {X Y : System A} → ≤-System Y X → ≤-System (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 - -id-x≤x : {X : System A} → ≤-System (map id X) X -⇒S (id-x≤x) = Id.function _ -≗-fₛ (id-x≤x {_} {x}) i s = System.refl x -≗-fₒ (id-x≤x {A} {x}) s = Push-identity - -x≤id-x : {x : System A} → ≤-System x (map id x) -⇒S x≤id-x = Id.function _ -≗-fₛ (x≤id-x {A} {x}) i s = System.refl x -≗-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 (map (g ∘ f) X) (map g (map f X)) × ≤-System (map g (map f X)) (map (g ∘ f) X) -System-homomorphism {f = f} {g} {X} = left , right - where - open System X - left : ≤-System (map (g ∘ f) X) (map g (map f X)) - left .⇒S = Id.function S - left .≗-fₛ i s = refl - left .≗-fₒ s = Push-homomorphism - right : ≤-System (map g (map f X)) (map (g ∘ f) X) - right .⇒S = Id.function S - right .≗-fₛ i s = refl - right .≗-fₒ s = ≋.sym Push-homomorphism - -System-resp-≈ - : {f g : Fin A → Fin B} - → f ≗ g - → {X : System A} - → (≤-System (map f X) (map g X)) × (≤-System (map g X) (map 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 → ≤-System (map f X) (map g X) - both f≗g .⇒S = Id.function S - both f≗g .≗-fₛ i s = cong fₛ (Pull-resp-≈ f≗g {i}) - both {f} {g} f≗g .≗-fₒ s = Push-resp-≈ f≗g + 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ₛ @@ -94,3 +106,5 @@ 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/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda index c2b6958..1d3d338 100644 --- a/Functor/Monoidal/Instance/Nat/Pull.agda +++ b/Functor/Monoidal/Instance/Nat/Pull.agda @@ -2,191 +2,167 @@ 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.Instance.Nat using (Nat-Cocartesian) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) -open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper) -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.Instance.Nat using (Nat) +open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ) +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 Data.Subset.Functional using (Subset) -open import Data.Nat.Base using (ℕ; _+_) -open import Relation.Binary using (Setoid) -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.Pull using (Pull; Pull₁) -open import Level using (0ℓ; Level) - +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 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 import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_) +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.Fin.Preimage using (preimage) -open import Function.Base using (_∘_; id) +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 import Data.Bool.Base using (Bool) -open import Data.Setoid using (∣_∣) -open import Data.Circuit.Value using (Value) -open import Data.System.Values Value using (Values) - -open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) -open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong) -open Strong using (SymmetricMonoidalFunctor) -open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) module Setoids-× = SymmetricMonoidalCategory Setoids-× -import Function.Construct.Constant as Const +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 -module _ where +private - open import Categories.Morphism (Setoids-×.U) using (_≅_; module Iso) - open import Data.Unit.Polymorphic using (tt) open _≅_ open Iso - Pull-ε : SingletonSetoid ≅ Values 0 - from Pull-ε = Const.function SingletonSetoid (Values 0) [] - to Pull-ε = Const.function (Values 0) SingletonSetoid tt + Pull-ε : ⊤ₛ ≅ Values 0 + from Pull-ε = Const ⊤ₛ (Values 0) [] + to Pull-ε = Const (Values 0) ⊤ₛ tt isoˡ (iso Pull-ε) = tt - isoʳ (iso Pull-ε) () - -++ₛ : {n m : ℕ} → Values n ×ₛ Values m ⟶ₛ Values (n + m) -to ++ₛ (xs , ys) = xs ++ ys -cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys - -splitₛ : {n m : ℕ} → Values (n + m) ⟶ₛ Values n ×ₛ Values m -to (splitₛ {n} {m}) v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_) -cong (splitₛ {n} {m}) v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_) - -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 ]′ (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 : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-) -⊗-homomorphism = niHelper record - { η = λ (n , m) → ++ₛ {n} {m} - ; η⁻¹ = λ (n , m) → splitₛ {n} {m} - ; commute = λ (f , g) → Pull-++ f g - ; iso = λ (n , m) → record - { isoˡ = λ { {x , y} → (λ i → ≡.cong [ x , y ] (splitAt-↑ˡ n i m)) , (λ i → ≡.cong [ x , y ] (splitAt-↑ʳ n m i)) } - ; isoʳ = λ { {x} i → ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i)) } - } - } - where - open import Data.Sum.Base using ([_,_]) - open import Data.Product.Base using (proj₁; proj₂) - -++-↑ˡ - : {n m : ℕ} - (X : ∣ Values n ∣) - (Y : ∣ Values m ∣) - → (X ++ Y) ∘ i₁ ≗ X -++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) - -++-↑ʳ - : {n m : ℕ} - (X : ∣ Values n ∣) - (Y : ∣ Values m ∣) - → (X ++ Y) ∘ i₂ ≗ Y -++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) - --- TODO move to Data.Vector -++-assoc - : {m n o : ℕ} - (X : ∣ Values m ∣) - (Y : ∣ Values n ∣) - (Z : ∣ Values 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) ++ Z) ([ i₁ ∘ i₁ , _ ]′ (splitAt m i)) ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩ - [ ((X ++ Y) ++ Z) ∘ i₁ ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₁) (splitAt m i) ⟩ - [ (X ++ Y) ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ - [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ (_ ++ Z) ∘ i₁ ∘ i₂ {m} , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₂) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ (X ++ Y) ∘ i₂ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ Y , ((X ++ Y) ++ Z) ∘ i₂ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ - (X ++ (Y ++ Z)) i ∎ - where - open Bool - open Fin - open ≡-Reasoning - --- TODO also Data.Vector -Pull-unitaryˡ - : {n : ℕ} - (X : ∣ Values n ∣) - → (X ++ []) ∘ i₁ ≗ X -Pull-unitaryˡ {n} X i = begin - [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩ - [ X , [] ]′ (inj₁ i) ≡⟨⟩ - X i ∎ - where - open ≡-Reasoning - -open import Function.Bundles using (Inverse) -open import Categories.Category.Instance.Nat using (Nat) -open import Categories.Morphism Nat using (_≅_) -Pull-swap - : {n m : ℕ} - (X : ∣ Values n ∣) - (Y : ∣ Values m ∣) - → (X ++ Y) ∘ (+-swap {n}) ≗ 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 (++-↑ʳ 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ʳ _ }) + 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 = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i } - ; unitaryˡ = λ _ → ≡.refl - ; unitaryʳ = λ { {n} {X , _} i → Pull-unitaryˡ X i } + ; 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} i → Pull-swap X Y i } + ; 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 index 667d68e..b53282d 100644 --- a/Functor/Monoidal/Instance/Nat/Push.agda +++ b/Functor/Monoidal/Instance/Nat/Push.agda @@ -9,12 +9,14 @@ 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₁; Push-identity) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Functor.Instance.Nat.Push using (Push; Push-defs) +open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Data.Vec.Functional using (Vector; []; _++_; head; tail) -open import Data.Vec.Functional.Properties using (++-cong) +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) @@ -25,17 +27,17 @@ 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.Base using (ℕ; _+_) -open import Data.Fin.Base using (Fin) +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-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆) -open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +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; _≟_; 2↔Bool) +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) @@ -51,278 +53,144 @@ 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.System.Values Value using (Values) - -open Func -Push-ε : SingletonSetoid {0ℓ} {0ℓ} ⟶ₛ Values 0 -to Push-ε x = [] -cong Push-ε x () - -++ₛ : {n m : ℕ} → Values n ×ₛ Values m ⟶ₛ Values (n + m) -to ++ₛ (xs , ys) = xs ++ ys -cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys - -∣_∣ : {c ℓ : Level} → Setoid c ℓ → Set c -∣_∣ = Setoid.Carrier +open import Data.Setoid using (∣_∣) open ℕ -merge-++ - : {n m : ℕ} - (xs : ∣ Values n ∣) - (ys : ∣ Values m ∣) - (S₁ : Subset n) - (S₂ : Subset m) - → merge (xs ++ ys) (S₁ ++ S₂) - ≡ join (merge xs S₁) (merge ys S₂) -merge-++ {zero} {m} xs ys S₁ S₂ = begin - merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩ - merge (xs ++ ys) S₂ ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩ - merge ys S₂ ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨ - join (merge xs S₁) (merge ys S₂) ∎ - where - open ≡-Reasoning -merge-++ {suc n} {m} xs ys S₁ S₂ = begin - merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩ - merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨ - join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂))) - ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩ - join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂))) - ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩ - join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂)) ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩ - join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂)) ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨ - join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂) - ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩ - join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂) ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨ - join (merge xs S₁) (merge ys S₂) ∎ - where - open ≡-Reasoning - -open Fin -⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y) -⁅⁆-≟ zero zero = ≡.refl -⁅⁆-≟ zero (suc y) = ≡.refl -⁅⁆-≟ (suc x) zero = ≡.refl -⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y -Push-++ - : {n n′ m m′ : ℕ} - (f : Fin n → Fin n′) - (g : Fin m → Fin m′) - (xs : ∣ Values n ∣) - (ys : ∣ Values m ∣) - → merge xs ∘ preimage f ∘ ⁅_⁆ ++ merge ys ∘ preimage g ∘ ⁅_⁆ - ≗ merge (xs ++ ys) ∘ preimage (f +₁ g) ∘ ⁅_⁆ -Push-++ {n} {n′} {m} {m′} f g xs ys i = begin - ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i ≡⟨⟩ - [ merge xs ∘ preimage f ∘ ⁅_⁆ , merge ys ∘ preimage g ∘ ⁅_⁆ ]′ (splitAt n′ 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) ([ ⁅⁆++⊥ , ⊥++⁅⁆ ]′ (splitAt n′ i))) ≡⟨⟩ - merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ ++ ⊥++⁅⁆) i)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ i)) ⟩ - merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎ - where - open ≡-Reasoning - left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ ++ ⊥)) - 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 ⁆) ++ (preimage g ⊥)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩ - merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ ++ ⊥)) ∎ - right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ ++ ⁅ 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 ⊥) ++ (preimage g ⁅ x ⁆)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩ - merge (xs ++ ys) (preimage (f +₁ g) (⊥ ++ ⁅ x ⁆)) ∎ - ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′ - ⁅⁆++⊥ x = ⁅ x ⁆ ++ ⊥ - ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′ - ⊥++⁅⁆ x = ⊥ ++ ⁅ x ⁆ +open import Data.System.Values Monoid using (Values; <ε>; ++ₛ; _++_; head; tail; _≋_) - open ℕ - - open Equivalence - - ⁅⁆-++ - : (i : Fin (n′ + m′)) - → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆ - ⁅⁆-++ i x with splitAt n′ i in eq₁ - ... | inj₁ i′ with splitAt n′ x in eq₂ - ... | inj₁ x′ = begin - ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ - does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩ - does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨ - ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ - ⁅ i ⁆ x ∎ - where - ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′)) - ⇔ .to = ≡.cong (_↑ˡ m′) - ⇔ .from = ↑ˡ-injective m′ i′ x′ - ⇔ .to-cong ≡.refl = ≡.refl - ⇔ .from-cong ≡.refl = ≡.refl - ... | inj₂ x′ = begin - false ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨ - does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨ - ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ - ⁅ i ⁆ x ∎ - where - ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′ - ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () } - ⁅⁆-++ i x | inj₂ i′ with splitAt n′ x in eq₂ - ⁅⁆-++ i x | inj₂ i′ | inj₁ x′ = ≡.trans (≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂) $ begin - false ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨ - does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨ - ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ - ⁅ i ⁆ x ∎ +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 - ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′ - ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () } - ⁅⁆-++ i x | inj₂ i′ | inj₂ x′ = begin - [ ⊥ , ⁅ i′ ⁆ ] (splitAt n′ x) ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]) eq₂ ⟩ - ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ - does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩ - does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨ - ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ - ⁅ i ⁆ x ∎ + ⁅⁆++⊥ : 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 - ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′)) - ⇔ .to = ≡.cong (n′ ↑ʳ_) - ⇔ .from = ↑ʳ-injective n′ i′ x′ - ⇔ .to-cong ≡.refl = ≡.refl - ⇔ .from-cong ≡.refl = ≡.refl - -⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-) -⊗-homomorphism = ntHelper record - { η = λ (n , m) → ++ₛ {n} {m} - ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} i → Push-++ f g xs ys i } - } - -++-↑ˡ - : {n m : ℕ} - (X : ∣ Values n ∣) - (Y : ∣ Values m ∣) - → (X ++ Y) ∘ i₁ ≗ X -++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) - -++-↑ʳ - : {n m : ℕ} - (X : ∣ Values n ∣) - (Y : ∣ Values m ∣) - → (X ++ Y) ∘ i₂ ≗ Y -++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) - -++-assoc - : {m n o : ℕ} - (X : ∣ Values m ∣) - (Y : ∣ Values n ∣) - (Z : ∣ Values 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) ++ Z) ([ i₁ ∘ i₁ , _ ]′ (splitAt m i)) ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩ - [ ((X ++ Y) ++ Z) ∘ i₁ ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₁) (splitAt m i) ⟩ - [ (X ++ Y) ∘ i₁ , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ - [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ (_ ++ Z) ∘ i₁ ∘ i₂ {m} , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ i₂) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ (X ++ Y) ∘ i₂ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ Y , ((X ++ Y) ++ Z) ∘ i₂ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩ - [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ - (X ++ (Y ++ Z)) i ∎ - where - open Bool - open Fin - 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 - -Push-assoc - : {m n o : ℕ} - (X : ∣ Values m ∣) - (Y : ∣ Values n ∣) - (Z : ∣ Values o ∣) - → merge ((X ++ Y) ++ Z) ∘ preimage (+-assocˡ {m}) ∘ ⁅_⁆ - ≗ 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ʳ _ } - open ≡-Reasoning - -preimage-++′ - : {n m o : ℕ} - (f : Vector (Fin o) n) - (g : Vector (Fin o) m) - (S : Subset o) - → preimage (f ++ g) S ≗ preimage f S ++ preimage g S -preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n - -Push-unitaryʳ - : {n : ℕ} - (X : ∣ Values n ∣) - (i : Fin n) - → merge (X ++ []) (preimage (id ++ (λ ())) ⁅ i ⁆) ≡ X i -Push-unitaryʳ {n} X i = begin - merge (X ++ []) (preimage (id ++ (λ ())) ⁅ i ⁆) ≡⟨ merge-cong₂ (X ++ []) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩ - merge (X ++ []) (preimage id ⁅ i ⁆ ++ preimage (λ ()) ⁅ i ⁆) ≡⟨⟩ - merge (X ++ []) (⁅ i ⁆ ++ 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 ∎ - where - open ≡-Reasoning - t : Fin (n + 0) → Fin n - t = id ++ (λ ()) - -Push-swap - : {n m : ℕ} - (X : ∣ Values n ∣) - (Y : ∣ Values m ∣) - → merge (X ++ Y) ∘ preimage (+-swap {m}) ∘ ⁅_⁆ ≗ 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 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 @@ -331,9 +199,11 @@ Push,++,[] .isBraidedMonoidal = record { isMonoidal = record { ε = Push-ε ; ⊗-homo = ⊗-homomorphism - ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → Push-assoc X Y Z i } - ; unitaryˡ = λ { {n} {_ , X} i → merge-⁅⁆ X i } - ; unitaryʳ = λ { {n} {X , _} i → Push-unitaryʳ X i } + ; 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} i → Push-swap X Y i } + ; 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 index d86588f..2201c35 100644 --- a/Functor/Monoidal/Instance/Nat/System.agda +++ b/Functor/Monoidal/Instance/Nat/System.agda @@ -2,67 +2,79 @@ module Functor.Monoidal.Instance.Nat.System where -open import Function.Construct.Identity using () renaming (function to Id) -import Function.Construct.Constant as Const +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.Instance.Nat using (Natop) -open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) -open import Data.Circuit.Value using (Value) -open import Data.Setoid using (_⇒ₛ_; ∣_∣) -open import Data.System {suc 0ℓ} using (Systemₛ; System; ≤-System) -open import Data.System.Values Value using (Values; _≋_; module ≋) -open import Data.Unit.Polymorphic using (⊤; tt) -open import Data.Vec.Functional using ([]) -open import Relation.Binary using (Setoid) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) -open import Functor.Instance.Nat.System using (Sys; map) -open import Function.Base using (_∘_) -open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_) -open import Function.Construct.Setoid using (setoid) 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-×) -open Func - -module _ where - - open System +module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B) +module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B) - discrete : System 0 - discrete .S = SingletonSetoid - discrete .fₛ = Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id SingletonSetoid) - discrete .fₒ = Const.function SingletonSetoid (Values 0) [] +open import Functor.Monoidal.Instance.Nat.Pull using (Pull,++,[]) +open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using (module Strong) -Sys-ε : SingletonSetoid {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0 -Sys-ε = Const.function SingletonSetoid (Systemₛ 0) discrete +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 Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to ⊤ₛ) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) -open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products) -open import Categories.Category.BinaryProducts using (module BinaryProducts) -open BinaryProducts products using (-×-) -open import Categories.Functor using (_∘F_) +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 import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -open import Categories.Category.Cocartesian using (Cocartesian) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) +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 import Data.Product.Base using (_,_; dmap) renaming (map to ×-map) +open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B) -open import Categories.Functor using (Functor) -open import Categories.Category.Product using (Product) -open import Categories.Category.Instance.Nat using (Nat) -open import Categories.Category.Instance.Setoids using (Setoids) +open Func -open import Data.Fin using (_↑ˡ_; _↑ʳ_) -open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) -open import Data.Nat using (ℕ; _+_) -open import Data.Product.Base using (_×_) +Sys-ε : ⊤ₛ {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0 +Sys-ε = Const ⊤ₛ (Systemₛ 0) (discrete 0) private @@ -71,13 +83,6 @@ private c₁ c₂ c₃ c₄ c₅ c₆ : Level ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level -open import Functor.Monoidal.Instance.Nat.Push using (++ₛ; Push,++,[]; Push-++; Push-assoc) -open import Functor.Monoidal.Instance.Nat.Pull using (splitₛ; Pull,++,[]; ++-assoc; Pull-unitaryˡ; Pull-ε) -open import Functor.Instance.Nat.Pull using (Pull; Pull₁; Pull-resp-≈; Pull-identity) -open import Functor.Instance.Nat.Push using (Push₁; Push-identity) - -open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ) - _×-⇒_ : {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} @@ -91,8 +96,6 @@ _×-⇒_ _×-⇒_ f g .to (x , y) = to f x ×-function to g y _×-⇒_ f g .cong (x , y) = cong f x , cong g y -open import Function.Construct.Setoid using (_∙_) - ⊗ : System n × System m → System (n + m) ⊗ {n} {m} (S₁ , S₂) = record { S = S₁.S ×ₛ S₂.S @@ -103,16 +106,6 @@ open import Function.Construct.Setoid using (_∙_) module S₁ = System S₁ module S₂ = System S₂ -open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×) -module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B) -open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_) -open import Categories.Functor.Monoidal.Symmetric Natop,+,0 0ℓ-Setoids-× using (module Strong) -open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B) -module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B) -open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using () renaming (module Strong to StrongB) -open Strong using (SymmetricMonoidalFunctor) -open StrongB using (BraidedMonoidalFunctor) - opaque _~_ : {A B : Setoid 0ℓ 0ℓ} → Func A B → Func A B → Set @@ -128,7 +121,7 @@ opaque ⊗ₛ : {n m : ℕ} - → Func (Systemₛ n ×ₛ Systemₛ m) (Systemₛ (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 @@ -136,66 +129,57 @@ opaque module b = System b module c = System c module d = System d - open ≤-System - module a≤c = ≤-System a≤c - module b≤d = ≤-System b≤d - module c≤a = ≤-System c≤a - module d≤b = ≤-System d≤b - - open Setoid - open System - - open import Data.Product.Base using (dmap) - open import Data.Vec.Functional.Properties using (++-cong) - left : ≤-System (⊗ₛ .to (a , b)) (⊗ₛ .to (c , d)) - left = record - { ⇒S = a≤c.⇒S ×-function b≤d.⇒S - ; ≗-fₛ = λ i → dmap (a≤c.≗-fₛ (i ∘ i₁)) (b≤d.≗-fₛ (i ∘ i₂)) - ; ≗-fₒ = λ (s₁ , s₂) → ++-cong (a.fₒ′ s₁) (c.fₒ′ (a≤c.⇒S ⟨$⟩ s₁)) (a≤c.≗-fₒ s₁) (b≤d.≗-fₒ s₂) - } + 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ₒ - right : ≤-System (⊗ₛ .to (c , d)) (⊗ₛ .to (a , b)) - right = record - { ⇒S = c≤a.⇒S ×-function d≤b.⇒S - ; ≗-fₛ = λ i → dmap (c≤a.≗-fₛ (i ∘ i₁)) (d≤b.≗-fₛ (i ∘ i₂)) - ; ≗-fₒ = λ (s₁ , s₂) → ++-cong (c.fₒ′ s₁) (a.fₒ′ (c≤a.⇒S ⟨$⟩ s₁)) (c≤a.≗-fₒ s₁) (d≤b.≗-fₒ s₂) - } +opaque -open import Data.Fin using (Fin) - -System-⊗-≤ - : {n n′ m m′ : ℕ} - (X : System n) - (Y : System m) - (f : Fin n → Fin n′) - (g : Fin m → Fin m′) - → ≤-System (⊗ (map f X , map g Y)) (map (f +₁ g) (⊗ (X , Y))) -System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record - { ⇒S = Id (X.S ×ₛ Y.S) - ; ≗-fₛ = λ i _ → cong X.fₛ (≋.sym (≡.cong i ∘ +₁∘i₁)) , cong Y.fₛ (≋.sym (≡.cong i ∘ +₁∘i₂ {f = f})) - ; ≗-fₒ = λ (s₁ , s₂) → Push-++ 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′) - → ≤-System (map (f +₁ g) (⊗ (X , Y))) (⊗ (map f X , map g Y)) -System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record - { ⇒S = Id (X.S ×ₛ Y.S) - -- ; ≗-fₛ = λ i _ → cong X.fₛ (≡.cong i ∘ +₁∘i₁) , cong Y.fₛ (≡.cong i ∘ +₁∘i₂ {f = f}) - ; ≗-fₛ = λ i _ → cong (X.fₛ ×-⇒ Y.fₛ) (Pull-resp-≈ (+₁∘i₁ {n′}) {i} , Pull-resp-≈ (+₁∘i₂ {f = f}) {i}) - ; ≗-fₒ = λ (s₁ , s₂) → ≋.sym (Push-++ f g (X.fₒ′ s₁) (Y.fₒ′ s₂)) - } - where - module X = System X - module Y = System Y - import Relation.Binary.PropositionalEquality as ≡ + 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 @@ -203,220 +187,195 @@ System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record ; commute = λ { (f , g) {X , Y} → System-⊗-≤ X Y f g , System-⊗-≥ X Y f g } } -⊗-assoc-≤ - : (X : System n) - (Y : System m) - (Z : System o) - → ≤-System (map (+-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-assoc (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ˡ) - open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod) - open BinaryProducts prod using () renaming (assocˡ to ×-assocˡ) - module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] - Pull,++,[]B : BraidedMonoidalFunctor - Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } - module Pull,++,[]B = BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }) - - open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (associativity-inv) - - module X = System X - module Y = System Y - module Z = System Z - -⊗-assoc-≥ - : (X : System n) - (Y : System m) - (Z : System o) - → ≤-System (⊗ (X , ⊗ (Y , Z))) (map (+-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ʳ) - open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products) - open BinaryProducts 0ℓ-products using (×-assoc; assocˡ; assocʳ) - - open import Categories.Morphism.Reasoning 0ℓ-Setoids-×.U using (switch-tofromʳ) - open import Categories.Functor.Monoidal.Symmetric using (module Lax) - module Lax₂ = Lax Nat,+,0 0ℓ-Setoids-× - module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[] - open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv) - module Push,++,[] = Lax₂.SymmetricMonoidalFunctor Push,++,[] - - +-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 - -open import Function.Base using (id) -Sys-unitaryˡ-≤ : (X : System n) → ≤-System (map id (⊗ (discrete , X))) X -Sys-unitaryˡ-≤ X = record - { ⇒S = proj₂ₛ - ; ≗-fₛ = λ i (_ , s) → X.refl - ; ≗-fₒ = λ (_ , s) → Push-identity - } - where - module X = System X - -Sys-unitaryˡ-≥ : (X : System n) → ≤-System X (map id (⊗ (discrete , X))) -Sys-unitaryˡ-≥ {n} X = record - { ⇒S = < Const.function X.S SingletonSetoid tt , Id X.S >ₛ - ; ≗-fₛ = λ i s → tt , X.refl - ; ≗-fₒ = λ s → Equiv.sym {x = Push₁ id} {Id (Values n)} Push-identity - } - where - module X = System X - open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv) - -open import Data.Vec.Functional using (_++_) +opaque -Sys-unitaryʳ-≤ : (X : System n) → ≤-System (map (id ++ (λ ())) (⊗ {n} {0} (X , discrete))) X -Sys-unitaryʳ-≤ {n} X = record - { ⇒S = proj₁ₛ - ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = SingletonSetoid {0ℓ}}) (unitaryʳ-inv {n} {i}) - ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt} - } - where - module X = System X - module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[] - open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; module Shorthands) - open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) - module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] - -Sys-unitaryʳ-≥ : (X : System n) → ≤-System X (map (id ++ (λ ())) (⊗ {n} {0} (X , discrete))) -Sys-unitaryʳ-≥ {n} X = record - { ⇒S = < Id X.S , Const.function X.S SingletonSetoid tt >ₛ - ; ≗-fₛ = λ i s → - cong - (X.fₛ ×-⇒ Const.function (Values 0) (SingletonSetoid ⇒ₛ SingletonSetoid) (Id (SingletonSetoid {suc 0ℓ} {0ℓ})) ∙ Id (Values n) ×-function ε⇒) - sym-split-unitaryʳ - {s , tt} - ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt} - } - where - module X = System X - module Pull,++,[] = Strong.SymmetricMonoidalFunctor Pull,++,[] - open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; module Shorthands) - open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) - module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] - import Categories.Category.Monoidal.Utilities 0ℓ-Setoids-×.monoidal as ⊗-Util - - open ⊗-Util.Shorthands using (ρ⇐) - open Shorthands using (ε⇐; ε⇒) - - sym-split-unitaryʳ - : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull₁ (id ++ (λ ())) - sym-split-unitaryʳ = - 0ℓ-Setoids-×.Equiv.sym - {Values n} - {Values n ×ₛ SingletonSetoid} - {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull₁ (id ++ (λ ()))} - {ρ⇐} - (unitaryʳ-inv {n}) - - sym-++-unitaryʳ : proj₁ₛ {B = SingletonSetoid {0ℓ} {0ℓ}} ≈ Push₁ (id ++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function ε⇒ - sym-++-unitaryʳ = - 0ℓ-Setoids-×.Equiv.sym - {Values n ×ₛ SingletonSetoid} - {Values n} - {Push₁ (id ++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function ε⇒} - {proj₁ₛ} - (Push,++,[].unitaryʳ {n}) - -Sys-braiding-compat-≤ - : (X : System n) - (Y : System m) - → ≤-System (map (+-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 - module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] - Pull,++,[]B : BraidedMonoidalFunctor - Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } - open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv) - open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) - module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] - -Sys-braiding-compat-≥ - : (X : System n) - (Y : System m) - → ≤-System (⊗ (Y , X)) (map (+-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 - module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[] - Pull,++,[]B : BraidedMonoidalFunctor - Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal } - open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv) - open import Categories.Functor.Monoidal.Symmetric Nat,+,0 0ℓ-Setoids-× using (module Lax) - module Push,++,[] = Lax.SymmetricMonoidalFunctor Push,++,[] - - 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}) + 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 import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax) open Lax.SymmetricMonoidalFunctor Sys,⊗,ε : Lax.SymmetricMonoidalFunctor @@ -431,3 +390,5 @@ Sys,⊗,ε .isBraidedMonoidal = record } ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y } } + +module Sys,⊗,ε = Lax.SymmetricMonoidalFunctor Sys,⊗,ε |