aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Functor/Monoidal/Instance/Nat/Circ.agda87
-rw-r--r--Functor/Monoidal/Instance/Nat/Preimage.agda164
-rw-r--r--Functor/Monoidal/Instance/Nat/Pull.agda166
-rw-r--r--Functor/Monoidal/Instance/Nat/Push.agda209
-rw-r--r--Functor/Monoidal/Instance/Nat/System.agda394
5 files changed, 0 insertions, 1020 deletions
diff --git a/Functor/Monoidal/Instance/Nat/Circ.agda b/Functor/Monoidal/Instance/Nat/Circ.agda
deleted file mode 100644
index 1b45a75..0000000
--- a/Functor/Monoidal/Instance/Nat/Circ.agda
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level; _⊔_; 0ℓ; suc)
-
-module Functor.Monoidal.Instance.Nat.Circ where
-
-import Categories.Object.Monoid as MonoidObject
-import Data.Permutation.Sort as ↭-Sort
-import Function.Reasoning as →-Reasoning
-
-open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
-import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
-open import Category.Monoidal.Instance.Nat using (Nat,+,0)
-open import Categories.Category.Construction.Monoids using (Monoids)
-open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian)
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Data.Setoid.Unit using (⊤ₛ)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open import Categories.Category.Cartesian using (Cartesian)
-open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
-open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open import Categories.Functor using (_∘F_)
-open BinaryProducts products using (-×-)
-open import Categories.Category.Product using (_⁂_)
-open import Categories.Category.Cocartesian using (Cocartesian)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Categories.Functor.Monoidal.Symmetric using (module Lax)
-open import Categories.Functor using (Functor)
-open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Data.Circuit using (Circuit; Circuitₛ; mkCircuit; mkCircuitₛ; _≈_; mk≈; map)
-open import Data.Circuit.Gate using (Gates)
-open import Data.Nat using (ℕ; _+_)
-open import Data.Product using (_,_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Function using (_⟶ₛ_; Func; _⟨$⟩_; _∘_; id)
-open import Functor.Instance.Nat.Circ {suc 0ℓ} using (Circ; module Multiset∘Edge)
-open import Functor.Instance.Nat.Edge {suc 0ℓ} using (Edge)
-open import Function.Construct.Setoid using (_∙_)
-
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-
-open import Functor.Instance.FreeCMonoid {suc 0ℓ} {suc 0ℓ} using (FreeCMonoid)
-
-Nat-Cocartesian-Category : CocartesianCategory 0ℓ 0ℓ 0ℓ
-Nat-Cocartesian-Category = record { cocartesian = Nat-Cocartesian }
-
-open import Functor.Monoidal.Construction.MultisetOf
- {𝒞 = Nat-Cocartesian-Category} (Edge Gates) FreeCMonoid using (MultisetOf,++,[])
-
-open Lax using (SymmetricMonoidalFunctor)
-
-module MultisetOf,++,[] = SymmetricMonoidalFunctor MultisetOf,++,[]
-
-open SymmetricMonoidalFunctor
-
-ε⇒ : ⊤ₛ ⟶ₛ Circuitₛ 0
-ε⇒ = mkCircuitₛ ∙ MultisetOf,++,[].ε
-
-open Cocartesian Nat-Cocartesian using (-+-)
-
-open Func
-
-η : {n m : ℕ} → Circuitₛ n ×ₛ Circuitₛ m ⟶ₛ Circuitₛ (n + m)
-η {n} {m} .to (mkCircuit X , mkCircuit Y) = mkCircuit (MultisetOf,++,[].⊗-homo.η (n , m) ⟨$⟩ (X , Y))
-η {n} {m} .cong (mk≈ x , mk≈ y) = mk≈ (cong (MultisetOf,++,[].⊗-homo.η (n , m)) (x , y))
-
-⊗-homomorphism : NaturalTransformation (-×- ∘F (Circ ⁂ Circ)) (Circ ∘F -+-)
-⊗-homomorphism = ntHelper record
- { η = λ (n , m) → η {n} {m}
- ; commute = λ { (f , g) {mkCircuit X , mkCircuit Y} → mk≈ (MultisetOf,++,[].⊗-homo.commute (f , g) {X , Y}) }
- }
-
-Circ,⊗,ε : SymmetricMonoidalFunctor Nat,+,0 Setoids-×
-Circ,⊗,ε .F = Circ
-Circ,⊗,ε .isBraidedMonoidal = record
- { isMonoidal = record
- { ε = ε⇒
- ; ⊗-homo = ⊗-homomorphism
- ; associativity = λ { {n} {m} {o} {(mkCircuit x , mkCircuit y) , mkCircuit z} →
- mk≈ (MultisetOf,++,[].associativity {n} {m} {o} {(x , y) , z}) }
- ; unitaryˡ = λ { {n} {_ , mkCircuit x} → mk≈ (MultisetOf,++,[].unitaryˡ {n} {_ , x}) }
- ; unitaryʳ = λ { {n} {mkCircuit x , _} → mk≈ (MultisetOf,++,[].unitaryʳ {n} {x , _}) }
- }
- ; braiding-compat = λ { {n} {m} {mkCircuit x , mkCircuit y} →
- mk≈ (MultisetOf,++,[].braiding-compat {n} {m} {x , y}) }
- }
diff --git a/Functor/Monoidal/Instance/Nat/Preimage.agda b/Functor/Monoidal/Instance/Nat/Preimage.agda
deleted file mode 100644
index 844df79..0000000
--- a/Functor/Monoidal/Instance/Nat/Preimage.agda
+++ /dev/null
@@ -1,164 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Functor.Monoidal.Instance.Nat.Preimage where
-
-open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Data.Setoid.Unit using (⊤ₛ)
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
-open import Categories.Category.Product using (_⁂_)
-open import Categories.Functor using (_∘F_)
-open import Data.Subset.Functional using (Subset)
-open import Data.Nat.Base using (ℕ; _+_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Product.Base using (_,_; _×_; Σ)
-open import Data.Vec.Functional using ([]; _++_)
-open import Data.Vec.Functional.Properties using (++-cong)
-open import Data.Vec.Functional using (Vector; [])
-open import Function.Bundles using (Func; _⟶ₛ_)
-open import Functor.Instance.Nat.Preimage using (Preimage; Subsetₛ)
-open import Level using (0ℓ)
-
-open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-open BinaryProducts products using (-×-)
-open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-swap; +₁∘+-swap)
-open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
-
-open import Data.Fin.Base using (Fin; splitAt; join; _↑ˡ_; _↑ʳ_)
-open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ)
-open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂)
-open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘)
-open import Data.Fin.Preimage using (preimage)
-open import Function.Base using (_∘_; id)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
-open import Data.Bool.Base using (Bool)
-
-open Func
-Preimage-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Subsetₛ 0
-to Preimage-ε x = []
-cong Preimage-ε x ()
-
-++ₛ : {n m : ℕ} → Subsetₛ n ×ₛ Subsetₛ m ⟶ₛ Subsetₛ (n + m)
-to ++ₛ (xs , ys) = xs ++ ys
-cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys
-
-preimage-++
- : {n n′ m m′ : ℕ}
- (f : Fin n → Fin n′)
- (g : Fin m → Fin m′)
- {xs : Subset n′}
- {ys : Subset m′}
- → preimage f xs ++ preimage g ys ≗ preimage (f +₁ g) (xs ++ ys)
-preimage-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin
- (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨
- [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨
- [ xs , ys ]′ (splitAt n′ (join n′ m′ (map f g (splitAt n e)))) ≡⟨ ≡.cong ([ xs , ys ]′ ∘ splitAt n′) ([,]-map (splitAt n e)) ⟩
- [ xs , ys ]′ (splitAt n′ ((f +₁ g) e)) ∎
- where
- open ≡-Reasoning
-
-⊗-homomorphism : NaturalTransformation (-×- ∘F (Preimage ⁂ Preimage)) (Preimage ∘F -+-)
-⊗-homomorphism = ntHelper record
- { η = λ (n , m) → ++ₛ {n} {m}
- ; commute = λ { {n′ , m′} {n , m} (f , g) {xs , ys} e → preimage-++ f g e }
- }
-
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
-open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Lax)
-open Lax using (SymmetricMonoidalFunctor)
-
-++-assoc
- : {m n o : ℕ}
- (X : Subset m)
- (Y : Subset n)
- (Z : Subset o)
- → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z)
-++-assoc {m} {n} {o} X Y Z i = begin
- ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩
- [ [ X , Y ]′ ∘ splitAt m , Z ]′ (splitAt (m + n) (+-assocʳ {m} i)) ≡⟨ [,]-cong ([,]-cong (inv ∘ X) (inv ∘ Y) ∘ splitAt m) (inv ∘ Z) (splitAt (m + n) (+-assocʳ {m} i)) ⟨
- [ [ b ∘ X′ , b ∘ Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [-,]-cong ([,]-∘ b ∘ splitAt m) (splitAt (m + n) (+-assocʳ {m} i)) ⟨
- [ b ∘ [ X′ , Y′ ]′ ∘ splitAt m , b ∘ Z′ ]′ (splitAt _ (+-assocʳ {m} i)) ≡⟨ [,]-∘ b (splitAt (m + n) (+-assocʳ {m} i)) ⟨
- b ([ [ X′ , Y′ ]′ ∘ splitAt m , Z′ ]′ (splitAt _ (+-assocʳ {m} i))) ≡⟨ ≡.cong b ([]∘assocʳ {2} {m} i) ⟩
- b ([ X′ , [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩
- [ b ∘ X′ , b ∘ [ Y′ , Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ b ∘ splitAt n) (splitAt m i) ⟩
- [ b ∘ X′ , [ b ∘ Y′ , b ∘ Z′ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ X) ([,]-cong (inv ∘ Y) (inv ∘ Z) ∘ splitAt n) (splitAt m i) ⟩
- [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩
- (X ++ (Y ++ Z)) i ∎
- where
- open Bool
- open Fin
- f : Bool → Fin 2
- f false = zero
- f true = suc zero
- b : Fin 2 → Bool
- b zero = false
- b (suc zero) = true
- inv : b ∘ f ≗ id
- inv false = ≡.refl
- inv true = ≡.refl
- X′ : Fin m → Fin 2
- X′ = f ∘ X
- Y′ : Fin n → Fin 2
- Y′ = f ∘ Y
- Z′ : Fin o → Fin 2
- Z′ = f ∘ Z
- open ≡-Reasoning
-
-Preimage-unitaryˡ
- : {n : ℕ}
- (X : Subset n)
- → (X ++ []) ∘ (_↑ˡ 0) ≗ X
-Preimage-unitaryˡ {n} X i = begin
- [ X , [] ]′ (splitAt _ (i ↑ˡ 0)) ≡⟨ ≡.cong ([ X , [] ]′) (splitAt-↑ˡ n i 0) ⟩
- [ X , [] ]′ (inj₁ i) ≡⟨⟩
- X i ∎
- where
- open ≡-Reasoning
-
-++-swap
- : {n m : ℕ}
- (X : Subset n)
- (Y : Subset m)
- → (X ++ Y) ∘ +-swap {n} ≗ Y ++ X
-++-swap {n} {m} X Y i = begin
- [ X , Y ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-cong (inv ∘ X) (inv ∘ Y) (splitAt n (+-swap {n} i)) ⟨
- [ b ∘ X′ , b ∘ Y′ ]′ (splitAt n (+-swap {n} i)) ≡⟨ [,]-∘ b (splitAt n (+-swap {n} i)) ⟨
- b ([ X′ , Y′ ]′ (splitAt n (+-swap {n} i))) ≡⟨ ≡.cong b ([]∘swap {2} {n} i) ⟩
- b ([ Y′ , X′ ]′ (splitAt m i)) ≡⟨ [,]-∘ b (splitAt m i) ⟩
- [ b ∘ Y′ , b ∘ X′ ]′ (splitAt m i) ≡⟨ [,]-cong (inv ∘ Y) (inv ∘ X) (splitAt m i) ⟩
- [ Y , X ]′ (splitAt m i) ∎
- where
- open Bool
- open Fin
- f : Bool → Fin 2
- f false = zero
- f true = suc zero
- b : Fin 2 → Bool
- b zero = false
- b (suc zero) = true
- inv : b ∘ f ≗ id
- inv false = ≡.refl
- inv true = ≡.refl
- X′ : Fin n → Fin 2
- X′ = f ∘ X
- Y′ : Fin m → Fin 2
- Y′ = f ∘ Y
- open ≡-Reasoning
-
-open SymmetricMonoidalFunctor
-Preimage,++,[] : SymmetricMonoidalFunctor
-Preimage,++,[] .F = Preimage
-Preimage,++,[] .isBraidedMonoidal = record
- { isMonoidal = record
- { ε = Preimage-ε
- ; ⊗-homo = ⊗-homomorphism
- ; associativity = λ { {m} {n} {o} {(X , Y) , Z} i → ++-assoc X Y Z i }
- ; unitaryˡ = λ _ → ≡.refl
- ; unitaryʳ = λ { {n} {X , _} i → Preimage-unitaryˡ X i }
- }
- ; braiding-compat = λ { {n} {m} {X , Y} i → ++-swap X Y i }
- }
diff --git a/Functor/Monoidal/Instance/Nat/Pull.agda b/Functor/Monoidal/Instance/Nat/Pull.agda
deleted file mode 100644
index b267f97..0000000
--- a/Functor/Monoidal/Instance/Nat/Pull.agda
+++ /dev/null
@@ -1,166 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Functor.Monoidal.Instance.Nat.Pull where
-
-import Categories.Morphism as Morphism
-
-open import Level using (0ℓ; Level)
-
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
-open import Category.Monoidal.Instance.Nat using (Natop,+,0; Natop-Cartesian)
-
-open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian; BinaryCoproducts)
-open import Categories.Category.Instance.Nat using (Nat)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Data.Setoid.Unit using (⊤ₛ)
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open import Categories.Category.Product using (_⁂_)
-open import Categories.Functor using (_∘F_)
-open import Categories.Functor.Monoidal.Symmetric Natop,+,0 Setoids-× using (module Strong)
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; niHelper)
-open import Data.Circuit.Value using (Monoid)
-open import Data.Vector using (++-assoc)
-open import Data.Fin.Base using (Fin; splitAt; join)
-open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
-open import Data.Fin.Preimage using (preimage)
-open import Data.Fin.Properties using (splitAt-join; splitAt-↑ˡ; splitAt-↑ʳ; join-splitAt)
-open import Data.Nat.Base using (ℕ; _+_)
-open import Data.Product.Base using (_,_; _×_; Σ; proj₁; proj₂)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Setoid using (∣_∣)
-open import Data.Subset.Functional using (Subset)
-open import Data.Sum.Base using ([_,_]′; map; map₁; map₂; inj₁; inj₂)
-open import Data.Sum.Properties using ([,]-map; [,]-cong; [-,]-cong; [,-]-cong; [,]-∘)
-open import Data.System.Values Monoid using (Values; <ε>; []-unique; _++_; ++ₛ; splitₛ; _≋_; [])
-open import Data.Unit.Polymorphic using (tt)
-open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Functor.Instance.Nat.Pull using (Pull; Pull-defs)
-open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning)
-
-open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-
-open BinaryProducts products using (-×-)
-open Cocartesian Nat-Cocartesian using (module Dual; _+₁_; +-assocʳ; +-comm; +-swap; +₁∘+-swap; i₁; i₂)
-open Dual.op-binaryProducts using () renaming (-×- to -+-; assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
-open Func
-open Morphism (Setoids-×.U) using (_≅_; module Iso)
-open Strong using (SymmetricMonoidalFunctor)
-open ≡-Reasoning
-
-private
-
- open _≅_
- open Iso
-
- Pull-ε : ⊤ₛ ≅ Values 0
- from Pull-ε = Const ⊤ₛ (Values 0) []
- to Pull-ε = Const (Values 0) ⊤ₛ tt
- isoˡ (iso Pull-ε) = tt
- isoʳ (iso Pull-ε) {x} = []-unique [] x
-
- opaque
- unfolding _++_
- unfolding Pull-defs
- Pull-++
- : {n n′ m m′ : ℕ}
- (f : Fin n → Fin n′)
- (g : Fin m → Fin m′)
- {xs : ∣ Values n′ ∣}
- {ys : ∣ Values m′ ∣}
- → (Pull.₁ f ⟨$⟩ xs) ++ (Pull.₁ g ⟨$⟩ ys) ≋ Pull.₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
- Pull-++ {n} {n′} {m} {m′} f g {xs} {ys} e = begin
- (xs ∘ f ++ ys ∘ g) e ≡⟨ [,]-map (splitAt n e) ⟨
- [ xs , ys ]′ (map f g (splitAt n e)) ≡⟨ ≡.cong [ xs , ys ]′ (splitAt-join n′ m′ (map f g (splitAt n e))) ⟨
- (xs ++ ys) (join n′ m′ (map f g (splitAt n e))) ≡⟨ ≡.cong (xs ++ ys) ([,]-map (splitAt n e)) ⟩
- (xs ++ ys) ((f +₁ g) e) ∎
-
- module _ {n m : ℕ} where
-
- opaque
- unfolding splitₛ
-
- open import Function.Construct.Setoid using (setoid)
- open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
- open import Function.Construct.Setoid using (_∙_)
- open import Function.Construct.Identity using () renaming (function to Id)
-
- split∘++ : splitₛ ∙ ++ₛ ≈ Id (Values n ×ₛ Values m)
- split∘++ {xs , ys} .proj₁ i = ≡.cong [ xs , ys ]′ (splitAt-↑ˡ n i m)
- split∘++ {xs , ys} .proj₂ i = ≡.cong [ xs , ys ]′ (splitAt-↑ʳ n m i)
-
- ++∘split : ++ₛ {n} ∙ splitₛ ≈ Id (Values (n + m))
- ++∘split {x} i = ≡.trans (≡.sym ([,]-∘ x (splitAt n i))) (≡.cong x (join-splitAt n m i))
-
- ⊗-homomorphism : NaturalIsomorphism (-×- ∘F (Pull ⁂ Pull)) (Pull ∘F -+-)
- ⊗-homomorphism = niHelper record
- { η = λ (n , m) → ++ₛ {n} {m}
- ; η⁻¹ = λ (n , m) → splitₛ {n} {m}
- ; commute = λ { {n , m} {n′ , m′} (f , g) {xs , ys} → Pull-++ f g }
- ; iso = λ (n , m) → record
- { isoˡ = split∘++
- ; isoʳ = ++∘split
- }
- }
-
- module _ {n m : ℕ} where
-
- opaque
- unfolding Pull-++
-
- Pull-i₁
- : (X : ∣ Values n ∣)
- (Y : ∣ Values m ∣)
- → Pull.₁ i₁ ⟨$⟩ (X ++ Y) ≋ X
- Pull-i₁ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m)
-
- Pull-i₂
- : (X : ∣ Values n ∣)
- (Y : ∣ Values m ∣)
- → Pull.₁ i₂ ⟨$⟩ (X ++ Y) ≋ Y
- Pull-i₂ X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i)
-
- opaque
- unfolding Pull-++
-
- Push-assoc
- : {m n o : ℕ}
- (X : ∣ Values m ∣)
- (Y : ∣ Values n ∣)
- (Z : ∣ Values o ∣)
- → Pull.₁ (+-assocʳ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z) ≋ X ++ (Y ++ Z)
- Push-assoc {m} {n} {o} X Y Z i = ++-assoc X Y Z i
-
- Pull-swap
- : {n m : ℕ}
- (X : ∣ Values n ∣)
- (Y : ∣ Values m ∣)
- → Pull.₁ (+-swap {n}) ⟨$⟩ (X ++ Y) ≋ Y ++ X
- Pull-swap {n} {m} X Y i = begin
- ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
- [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (Pull-i₂ X Y) (splitAt m i) ⟩
- [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (Pull-i₁ X Y) (splitAt m i) ⟩
- [ Y , X ]′ (splitAt m i) ≡⟨⟩
- (Y ++ X) i ∎
-
-open SymmetricMonoidalFunctor
-
-Pull,++,[] : SymmetricMonoidalFunctor
-Pull,++,[] .F = Pull
-Pull,++,[] .isBraidedMonoidal = record
- { isStrongMonoidal = record
- { ε = Pull-ε
- ; ⊗-homo = ⊗-homomorphism
- ; associativity = λ { {_} {_} {_} {(X , Y) , Z} → Push-assoc X Y Z }
- ; unitaryˡ = λ { {n} {_ , X} → Pull-i₂ {0} {n} [] X }
- ; unitaryʳ = λ { {n} {X , _} → Pull-i₁ {n} {0} X [] }
- }
- ; braiding-compat = λ { {n} {m} {X , Y} → Pull-swap X Y }
- }
-
-module Pull,++,[] = SymmetricMonoidalFunctor Pull,++,[]
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda
deleted file mode 100644
index 2e8c0cf..0000000
--- a/Functor/Monoidal/Instance/Nat/Push.agda
+++ /dev/null
@@ -1,209 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Functor.Monoidal.Instance.Nat.Push where
-
-open import Categories.Category.Instance.Nat using (Nat)
-open import Data.Bool.Base using (Bool; false)
-open import Data.Subset.Functional using (Subset; ⁅_⁆; ⊥)
-open import Function.Base using (_∘_; case_of_; _$_; id)
-open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
-open import Level using (0ℓ; Level)
-open import Relation.Binary using (Rel; Setoid)
-open import Functor.Instance.Nat.Push using (Push; Push-defs)
-open import Data.Setoid.Unit using (⊤ₛ)
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Data.Vec.Functional as Vec using (Vector)
-open import Data.Vector using (++-assoc; ++-↑ˡ; ++-↑ʳ)
--- open import Data.Vec.Functional.Properties using (++-cong)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open import Categories.Category.Cartesian using (Cartesian)
-open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products)
-open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
-open import Categories.Category.Instance.Nat using (Nat-Cocartesian)
-open import Categories.Category.Cocartesian using (Cocartesian)
-open import Categories.Category.Product using (_⁂_)
-open import Categories.Functor using () renaming (_∘F_ to _∘′_)
-open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assoc; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Nat using (ℕ; _+_)
-open import Data.Fin using (Fin)
-open import Data.Product.Base using (_,_; _×_; Σ)
-open import Data.Fin.Preimage using (preimage; preimage-⊥; preimage-cong₂)
-open import Functor.Monoidal.Instance.Nat.Preimage using (preimage-++)
-open import Data.Sum.Base using ([_,_]; [_,_]′; inj₁; inj₂)
-open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map)
-open import Data.Circuit.Merge using (merge-with; merge; merge-⊥; merge-[]; ⁅⁆-++; merge-++; merge-cong₁; merge-cong₂; merge-suc; _when_; join-merge; merge-preimage-ρ; merge-⁅⁆)
-open import Data.Circuit.Value using (Value; join; join-comm; join-assoc; Monoid)
-open import Data.Fin.Base using (splitAt; _↑ˡ_; _↑ʳ_) renaming (join to joinAt)
-open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; splitAt⁻¹-↑ʳ; ↑ˡ-injective; ↑ʳ-injective; _≟_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning)
-open BinaryProducts products using (-×-)
-open Value using (U)
-open Bool using (false)
-
-open import Function.Bundles using (Equivalence)
-open import Category.Monoidal.Instance.Nat using (Nat,+,0)
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×)
-open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
-open Lax using (SymmetricMonoidalFunctor)
-open import Categories.Morphism Nat using (_≅_)
-open import Function.Bundles using (Inverse)
-open import Data.Fin.Permutation using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
-open Dual.op-binaryProducts using () renaming (assocˡ∘⟨⟩ to []∘assocʳ; swap∘⟨⟩ to []∘swap)
-open import Relation.Nullary.Decidable using (does; does-⇔; dec-false)
-open import Data.Setoid using (∣_∣)
-
-open ℕ
-
-open import Data.System.Values Monoid using (Values; <ε>; ++ₛ; _++_; head; tail; _≋_)
-
-open Func
-open ≡-Reasoning
-
-private
-
- Push-ε : ⊤ₛ {0ℓ} {0ℓ} ⟶ₛ Values 0
- Push-ε = Const ⊤ₛ (Values 0) <ε>
-
- opaque
-
- unfolding _++_
-
- unfolding Push-defs
- Push-++
- : {n n′ m m′ : ℕ }
- → (f : Fin n → Fin n′)
- → (g : Fin m → Fin m′)
- → (xs : ∣ Values n ∣)
- → (ys : ∣ Values m ∣)
- → (Push.₁ f ⟨$⟩ xs) ++ (Push.₁ g ⟨$⟩ ys)
- ≋ Push.₁ (f +₁ g) ⟨$⟩ (xs ++ ys)
- Push-++ {n} {n′} {m} {m′} f g xs ys i = begin
- ((merge xs ∘ preimage f ∘ ⁅_⁆) ++ (merge ys ∘ preimage g ∘ ⁅_⁆)) i
- ≡⟨ [,]-cong left right (splitAt n′ i) ⟩
- [ (λ x → merge (xs ++ ys) _) , (λ x → merge (xs ++ ys) _) ]′ (splitAt n′ i)
- ≡⟨ [,]-∘ (merge (xs ++ ys) ∘ (preimage (f +₁ g))) (splitAt n′ i) ⟨
- merge (xs ++ ys) (preimage (f +₁ g) ((⁅⁆++⊥ Vec.++ ⊥++⁅⁆) i)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-cong₂ (f +₁ g) (⁅⁆-++ {n′} i)) ⟩
- merge (xs ++ ys) (preimage (f +₁ g) ⁅ i ⁆) ∎
- where
- ⁅⁆++⊥ : Vector (Subset (n′ + m′)) n′
- ⁅⁆++⊥ x = ⁅ x ⁆ Vec.++ ⊥
- ⊥++⁅⁆ : Vector (Subset (n′ + m′)) m′
- ⊥++⁅⁆ x = ⊥ Vec.++ ⁅ x ⁆
- left : (x : Fin n′) → merge xs (preimage f ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥))
- left x = begin
- merge xs (preimage f ⁅ x ⁆) ≡⟨ join-comm U (merge xs (preimage f ⁅ x ⁆)) ⟩
- join (merge xs (preimage f ⁅ x ⁆)) U ≡⟨ ≡.cong (join (merge _ _)) (merge-⊥ ys) ⟨
- join (merge xs (preimage f ⁅ x ⁆)) (merge ys ⊥) ≡⟨ ≡.cong (join (merge _ _)) (merge-cong₂ ys (preimage-⊥ g)) ⟨
- join (merge xs (preimage f ⁅ x ⁆)) (merge ys (preimage g ⊥)) ≡⟨ merge-++ xs ys (preimage f ⁅ x ⁆) (preimage g ⊥) ⟨
- merge (xs ++ ys) ((preimage f ⁅ x ⁆) Vec.++ (preimage g ⊥)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
- merge (xs ++ ys) (preimage (f +₁ g) (⁅ x ⁆ Vec.++ ⊥)) ∎
- right : (x : Fin m′) → merge ys (preimage g ⁅ x ⁆) ≡ merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆))
- right x = begin
- merge ys (preimage g ⁅ x ⁆) ≡⟨⟩
- join U (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-⊥ xs) ⟨
- join (merge xs ⊥) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ ≡.cong (λ h → join h (merge _ _)) (merge-cong₂ xs (preimage-⊥ f)) ⟨
- join (merge xs (preimage f ⊥)) (merge ys (preimage g ⁅ x ⁆)) ≡⟨ merge-++ xs ys (preimage f ⊥) (preimage g ⁅ x ⁆) ⟨
- merge (xs ++ ys) ((preimage f ⊥) Vec.++ (preimage g ⁅ x ⁆)) ≡⟨ merge-cong₂ (xs ++ ys) (preimage-++ f g) ⟩
- merge (xs ++ ys) (preimage (f +₁ g) (⊥ Vec.++ ⁅ x ⁆)) ∎
-
- ⊗-homomorphism : NaturalTransformation (-×- ∘′ (Push ⁂ Push)) (Push ∘′ -+-)
- ⊗-homomorphism = ntHelper record
- { η = λ (n , m) → ++ₛ {n} {m}
- ; commute = λ { (f , g) {xs , ys} → Push-++ f g xs ys }
- }
-
- opaque
-
- unfolding Push-defs
- unfolding _++_
-
- Push-assoc
- : {m n o : ℕ}
- (X : ∣ Values m ∣)
- (Y : ∣ Values n ∣)
- (Z : ∣ Values o ∣)
- → (Push.₁ (+-assocˡ {m} {n} {o}) ⟨$⟩ ((X ++ Y) ++ Z)) ≋ X ++ Y ++ Z
- Push-assoc {m} {n} {o} X Y Z i = begin
- merge ((X ++ Y) ++ Z) (preimage (+-assocˡ {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ ↔-mno ((X ++ Y) ++ Z) ⁅ i ⁆ ⟩
- merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (⁅ i ⁆) ≡⟨⟩
- merge (((X ++ Y) ++ Z) ∘ (+-assocʳ {m})) (preimage id ⁅ i ⁆) ≡⟨ merge-cong₁ (++-assoc X Y Z) (preimage id ⁅ i ⁆) ⟩
- merge (X ++ (Y ++ Z)) (preimage id ⁅ i ⁆) ≡⟨ Push.identity i ⟩
- (X ++ (Y ++ Z)) i ∎
- where
- open Inverse
- module +-assoc = _≅_ (+-assoc {m} {n} {o})
- ↔-mno : Permutation ((m + n) + o) (m + (n + o))
- ↔-mno .to = +-assocˡ {m}
- ↔-mno .from = +-assocʳ {m}
- ↔-mno .to-cong ≡.refl = ≡.refl
- ↔-mno .from-cong ≡.refl = ≡.refl
- ↔-mno .inverse = (λ { ≡.refl → +-assoc.isoˡ _ }) , λ { ≡.refl → +-assoc.isoʳ _ }
-
- Push-unitaryˡ
- : {n : ℕ}
- (X : ∣ Values n ∣)
- → Push.₁ id ⟨$⟩ (<ε> ++ X) ≋ X
- Push-unitaryˡ = merge-⁅⁆
-
- preimage-++′
- : {n m o : ℕ}
- (f : Vector (Fin o) n)
- (g : Vector (Fin o) m)
- (S : Subset o)
- → preimage (f Vec.++ g) S ≗ preimage f S Vec.++ preimage g S
- preimage-++′ {n} f g S = [,]-∘ S ∘ splitAt n
-
- Push-unitaryʳ
- : {n : ℕ}
- (X : ∣ Values n ∣)
- → Push.₁ (id Vec.++ (λ())) ⟨$⟩ (X ++ (<ε> {0})) ≋ X
- Push-unitaryʳ {n} X i = begin
- merge (X ++ <ε>) (preimage (id Vec.++ (λ ())) ⁅ i ⁆) ≡⟨ merge-cong₂ (X Vec.++ <ε>) (preimage-++′ id (λ ()) ⁅ i ⁆) ⟩
- merge (X ++ <ε>) (⁅ i ⁆ Vec.++ preimage (λ ()) ⁅ i ⁆) ≡⟨ merge-++ X <ε> ⁅ i ⁆ (preimage (λ ()) ⁅ i ⁆) ⟩
- join (merge X ⁅ i ⁆) (merge <ε> (preimage (λ ()) ⁅ i ⁆)) ≡⟨ ≡.cong (join (merge X ⁅ i ⁆)) (merge-[] <ε> (preimage (λ ()) ⁅ i ⁆)) ⟩
- join (merge X ⁅ i ⁆) U ≡⟨ join-comm (merge X ⁅ i ⁆) U ⟩
- merge X ⁅ i ⁆ ≡⟨ merge-⁅⁆ X i ⟩
- X i ∎
-
- Push-swap
- : {n m : ℕ}
- (X : ∣ Values n ∣)
- (Y : ∣ Values m ∣)
- → Push.₁ (+-swap {m}) ⟨$⟩ (X ++ Y) ≋ (Y ++ X)
- Push-swap {n} {m} X Y i = begin
- merge (X ++ Y) (preimage (+-swap {m}) ⁅ i ⁆) ≡⟨ merge-preimage-ρ n+m↔m+n (X ++ Y) ⁅ i ⁆ ⟩
- merge ((X ++ Y) ∘ +-swap {n}) ⁅ i ⁆ ≡⟨ merge-⁅⁆ ((X ++ Y) ∘ (+-swap {n})) i ⟩
- ((X ++ Y) ∘ +-swap {n}) i ≡⟨ [,]-∘ (X ++ Y) (splitAt m i) ⟩
- [ (X ++ Y) ∘ i₂ , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ʳ X Y) (splitAt m i) ⟩
- [ Y , (X ++ Y) ∘ i₁ ]′ (splitAt m i) ≡⟨ [,-]-cong (++-↑ˡ X Y) (splitAt m i) ⟩
- [ Y , X ]′ (splitAt m i) ≡⟨⟩
- (Y ++ X) i ∎
- where
- open ≡-Reasoning
- open Inverse
- module +-swap = _≅_ (+-comm {m} {n})
- n+m↔m+n : Permutation (n + m) (m + n)
- n+m↔m+n .to = +-swap.to
- n+m↔m+n .from = +-swap.from
- n+m↔m+n .to-cong ≡.refl = ≡.refl
- n+m↔m+n .from-cong ≡.refl = ≡.refl
- n+m↔m+n .inverse = (λ { ≡.refl → +-swap.isoˡ _ }) , (λ { ≡.refl → +-swap.isoʳ _ })
-
-open SymmetricMonoidalFunctor
-Push,++,[] : SymmetricMonoidalFunctor
-Push,++,[] .F = Push
-Push,++,[] .isBraidedMonoidal = record
- { isMonoidal = record
- { ε = Push-ε
- ; ⊗-homo = ⊗-homomorphism
- ; associativity = λ { {n} {m} {o} {(X , Y) , Z} → Push-assoc X Y Z }
- ; unitaryˡ = λ { {n} {_ , X} → Push-unitaryˡ X }
- ; unitaryʳ = λ { {n} {X , _} → Push-unitaryʳ X }
- }
- ; braiding-compat = λ { {n} {m} {X , Y} → Push-swap X Y }
- }
-
-module Push,++,[] = SymmetricMonoidalFunctor Push,++,[]
diff --git a/Functor/Monoidal/Instance/Nat/System.agda b/Functor/Monoidal/Instance/Nat/System.agda
deleted file mode 100644
index 6659fb3..0000000
--- a/Functor/Monoidal/Instance/Nat/System.agda
+++ /dev/null
@@ -1,394 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Functor.Monoidal.Instance.Nat.System where
-
-import Categories.Category.Monoidal.Utilities as ⊗-Util
-import Data.Circuit.Value as Value
-import Data.Vec.Functional as Vec
-import Relation.Binary.PropositionalEquality as ≡
-
-open import Level using (0ℓ; suc; Level)
-
-open import Category.Monoidal.Instance.Nat using (Nat,+,0; Natop,+,0)
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory)
-open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using () renaming (Setoids-× to 0ℓ-Setoids-×)
-open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
-
-module Natop,+,0 = SymmetricMonoidalCategory Natop,+,0 renaming (braidedMonoidalCategory to B)
-module 0ℓ-Setoids-× = SymmetricMonoidalCategory 0ℓ-Setoids-× renaming (braidedMonoidalCategory to B)
-
-open import Functor.Monoidal.Instance.Nat.Pull using (Pull,++,[])
-open import Categories.Functor.Monoidal.Braided Natop,+,0.B 0ℓ-Setoids-×.B using (module Strong)
-
-Pull,++,[]B : Strong.BraidedMonoidalFunctor
-Pull,++,[]B = record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal }
-module Pull,++,[]B = Strong.BraidedMonoidalFunctor (record { isBraidedMonoidal = Pull,++,[].isBraidedMonoidal })
-
-open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Cocartesian using (Cocartesian)
-open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian; Natop)
-open import Categories.Category.Instance.Setoids using (Setoids)
-open import Data.Setoid.Unit using (⊤ₛ)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
-open import Categories.Category.Product using (Product)
-open import Categories.Category.Product using (_⁂_)
-open import Categories.Functor using (Functor)
-open import Categories.Functor using (_∘F_)
-open import Categories.Functor.Monoidal.Symmetric Nat,+,0 Setoids-× using (module Lax)
-open import Categories.NaturalTransformation.Core using (NaturalTransformation; ntHelper)
-open import Data.Circuit.Value using (Monoid)
-open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ; _+_)
-open import Data.Product using (_,_; dmap; _×_) renaming (map to ×-map)
-open import Data.Product.Function.NonDependent.Setoid using (_×-function_; proj₁ₛ; proj₂ₛ; <_,_>ₛ; swapₛ)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
-open import Data.Setoid using (_⇒ₛ_; ∣_∣)
-open import Data.System {suc 0ℓ} using (Systemₛ; System; discrete; _≤_)
-open import Data.System.Values Monoid using (++ₛ; splitₛ; Values; ++-cong; _++_; [])
-open import Data.System.Values Value.Monoid using (_≋_; module ≋)
-open import Data.Unit.Polymorphic using (⊤; tt)
-open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_; id; case_of_)
-open import Function.Construct.Constant using () renaming (function to Const)
-open import Function.Construct.Identity using () renaming (function to Id)
-open import Function.Construct.Setoid using (_∙_; setoid)
-open import Functor.Instance.Nat.Pull using (Pull)
-open import Functor.Instance.Nat.Push using (Push)
-open import Functor.Instance.Nat.System using (Sys; Sys-defs)
-open import Functor.Monoidal.Braided.Strong.Properties Pull,++,[]B using (braiding-compat-inv)
-open import Functor.Monoidal.Instance.Nat.Push using (Push,++,[])
-open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (associativity-inv)
-open import Functor.Monoidal.Strong.Properties Pull,++,[].monoidalFunctor using (unitaryʳ-inv; unitaryˡ-inv; module Shorthands)
-open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
-
-open module ⇒ₛ {A} {B} = Setoid (setoid {0ℓ} {0ℓ} {0ℓ} {0ℓ} A B) using (_≈_)
-
-open Cartesian (Setoids-Cartesian {suc 0ℓ} {suc 0ℓ}) using (products)
-
-open BinaryProducts products using (-×-)
-open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap; +₁∘i₁; +₁∘i₂)
-open Dual.op-binaryProducts using () renaming (×-assoc to +-assoc)
-open SymmetricMonoidalCategory using () renaming (braidedMonoidalCategory to B)
-
-open Func
-
-Sys-ε : ⊤ₛ {suc 0ℓ} {suc 0ℓ} ⟶ₛ Systemₛ 0
-Sys-ε = Const ⊤ₛ (Systemₛ 0) (discrete 0)
-
-private
-
- variable
- n m o : ℕ
- c₁ c₂ c₃ c₄ c₅ c₆ : Level
- ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level
-
-_×-⇒_
- : {A : Setoid c₁ ℓ₁}
- {B : Setoid c₂ ℓ₂}
- {C : Setoid c₃ ℓ₃}
- {D : Setoid c₄ ℓ₄}
- {E : Setoid c₅ ℓ₅}
- {F : Setoid c₆ ℓ₆}
- → A ⟶ₛ B ⇒ₛ C
- → D ⟶ₛ E ⇒ₛ F
- → A ×ₛ D ⟶ₛ B ×ₛ E ⇒ₛ C ×ₛ F
-_×-⇒_ f g .to (x , y) = to f x ×-function to g y
-_×-⇒_ f g .cong (x , y) = cong f x , cong g y
-
-⊗ : System n × System m → System (n + m)
-⊗ {n} {m} (S₁ , S₂) = record
- { S = S₁.S ×ₛ S₂.S
- ; fₛ = S₁.fₛ ×-⇒ S₂.fₛ ∙ splitₛ
- ; fₒ = ++ₛ ∙ S₁.fₒ ×-function S₂.fₒ
- }
- where
- module S₁ = System S₁
- module S₂ = System S₂
-
-opaque
-
- _~_ : {A B : Setoid 0ℓ 0ℓ} → Func A B → Func A B → Set
- _~_ = _≈_
- infix 4 _~_
-
- sym-~
- : {A B : Setoid 0ℓ 0ℓ}
- {x y : Func A B}
- → x ~ y
- → y ~ x
- sym-~ {A} {B} {x} {y} = 0ℓ-Setoids-×.Equiv.sym {A} {B} {x} {y}
-
-⊗ₛ
- : {n m : ℕ}
- → Systemₛ n ×ₛ Systemₛ m ⟶ₛ Systemₛ (n + m)
-⊗ₛ .to = ⊗
-⊗ₛ {n} {m} .cong {a , b} {c , d} ((a≤c , c≤a) , (b≤d , d≤b)) = left , right
- where
- module a = System a
- module b = System b
- module c = System c
- module d = System d
- module a≤c = _≤_ a≤c
- module b≤d = _≤_ b≤d
- module c≤a = _≤_ c≤a
- module d≤b = _≤_ d≤b
-
- open _≤_
- left : ⊗ₛ ⟨$⟩ (a , b) ≤ ⊗ₛ ⟨$⟩ (c , d)
- left .⇒S = a≤c.⇒S ×-function b≤d.⇒S
- left .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (a≤c.≗-fₛ i₁) (b≤d.≗-fₛ i₂)
- left .≗-fₒ = cong ++ₛ ∘ dmap a≤c.≗-fₒ b≤d.≗-fₒ
-
- right : ⊗ₛ ⟨$⟩ (c , d) ≤ ⊗ₛ ⟨$⟩ (a , b)
- right .⇒S = c≤a.⇒S ×-function d≤b.⇒S
- right .≗-fₛ i with (i₁ , i₂) ← splitₛ ⟨$⟩ i = dmap (c≤a.≗-fₛ i₁) (d≤b.≗-fₛ i₂)
- right .≗-fₒ = cong ++ₛ ∘ dmap c≤a.≗-fₒ d≤b.≗-fₒ
-
-opaque
-
- unfolding Sys-defs
-
- System-⊗-≤
- : {n n′ m m′ : ℕ}
- (X : System n)
- (Y : System m)
- (f : Fin n → Fin n′)
- (g : Fin m → Fin m′)
- → ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y) ≤ Sys.₁ (f +₁ g) ⟨$⟩ ⊗ (X , Y)
- System-⊗-≤ {n} {n′} {m} {m′} X Y f g = record
- { ⇒S = Id (X.S ×ₛ Y.S)
- ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.sym-commute (f , g) {i}) {s}
- ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂}
- }
- where
- module X = System X
- module Y = System Y
-
- System-⊗-≥
- : {n n′ m m′ : ℕ}
- (X : System n)
- (Y : System m)
- (f : Fin n → Fin n′)
- (g : Fin m → Fin m′)
- → Sys.₁ (f +₁ g) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Sys.₁ f ⟨$⟩ X , Sys.₁ g ⟨$⟩ Y)
- System-⊗-≥ {n} {n′} {m} {m′} X Y f g = record
- { ⇒S = Id (X.S ×ₛ Y.S)
- ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ Y.fₛ) (Pull,++,[].⊗-homo.⇐.commute (f , g) {i}) {s}
- ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].⊗-homo.sym-commute (f , g) {X.fₒ′ s₁ , Y.fₒ′ s₂}
- }
- where
- module X = System X
- module Y = System Y
-
-⊗-homomorphism : NaturalTransformation (-×- ∘F (Sys ⁂ Sys)) (Sys ∘F -+-)
-⊗-homomorphism = ntHelper record
- { η = λ (n , m) → ⊗ₛ {n} {m}
- ; commute = λ { (f , g) {X , Y} → System-⊗-≤ X Y f g , System-⊗-≥ X Y f g }
- }
-
-opaque
-
- unfolding Sys-defs
-
- ⊗-assoc-≤
- : (X : System n)
- (Y : System m)
- (Z : System o)
- → Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z)) ≤ ⊗ (X , ⊗ (Y , Z))
- ⊗-assoc-≤ {n} {m} {o} X Y Z = record
- { ⇒S = assocˡ
- ; ≗-fₛ = λ i ((s₁ , s₂) , s₃) → cong (X.fₛ ×-⇒ (Y.fₛ ×-⇒ Z.fₛ) ∙ assocˡ) (associativity-inv {x = i}) {s₁ , s₂ , s₃}
- ; ≗-fₒ = λ ((s₁ , s₂) , s₃) → Push,++,[].associativity {x = (X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
- }
- where
- open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to 0ℓ-products)
- open BinaryProducts 0ℓ-products using (assocˡ)
-
- module X = System X
- module Y = System Y
- module Z = System Z
-
- ⊗-assoc-≥
- : (X : System n)
- (Y : System m)
- (Z : System o)
- → ⊗ (X , ⊗ (Y , Z)) ≤ Sys.₁ (+-assocˡ {n}) ⟨$⟩ (⊗ (⊗ (X , Y) , Z))
- ⊗-assoc-≥ {n} {m} {o} X Y Z = record
- { ⇒S = ×-assocʳ
- ; ≗-fₛ = λ i (s₁ , s₂ , s₃) → cong ((X.fₛ ×-⇒ Y.fₛ) ×-⇒ Z.fₛ) (sym-split-assoc {i}) {(s₁ , s₂) , s₃}
- ; ≗-fₒ = λ (s₁ , s₂ , s₃) → sym-++-assoc {(X.fₒ′ s₁ , Y.fₒ′ s₂) , Z.fₒ′ s₃}
- }
- where
- open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using () renaming (products to prod)
- open BinaryProducts prod using () renaming (assocʳ to ×-assocʳ; assocˡ to ×-assocˡ)
-
- +-assocℓ : Fin ((n + m) + o) → Fin (n + (m + o))
- +-assocℓ = +-assocˡ {n} {m} {o}
-
- opaque
-
- unfolding _~_
-
- associativity-inv-~ : splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ ~ ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ
- associativity-inv-~ {i} = associativity-inv {n} {m} {o} {i}
-
- associativity-~ : Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o) ~ ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ
- associativity-~ {i} = Push,++,[].associativity {n} {m} {o} {i}
-
- sym-split-assoc-~ : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ~ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ
- sym-split-assoc-~ = sym-~ associativity-inv-~
-
- sym-++-assoc-~ : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ~ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
- sym-++-assoc-~ = sym-~ associativity-~
-
- opaque
-
- unfolding _~_
-
- sym-split-assoc : ×-assocʳ ∙ Id (Values n) ×-function splitₛ ∙ splitₛ ≈ splitₛ ×-function Id (Values o) ∙ splitₛ ∙ Pull.₁ +-assocℓ
- sym-split-assoc {i} = sym-split-assoc-~ {i}
-
- sym-++-assoc : ++ₛ ∙ Id (Values n) ×-function ++ₛ ∙ ×-assocˡ ≈ Push.₁ (+-assocˡ {n} {m} {o}) ∙ ++ₛ ∙ ++ₛ ×-function Id (Values o)
- sym-++-assoc {i} = sym-++-assoc-~
-
- module X = System X
- module Y = System Y
- module Z = System Z
-
- Sys-unitaryˡ-≤ : (X : System n) → Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X)) ≤ X
- Sys-unitaryˡ-≤ {n} X = record
- { ⇒S = proj₂ₛ
- ; ≗-fₛ = λ i (_ , s) → cong (X.fₛ ∙ proj₂ₛ {A = ⊤ₛ {0ℓ}}) (unitaryˡ-inv {n} {i})
- ; ≗-fₒ = λ (_ , s) → Push,++,[].unitaryˡ {n} {tt , X.fₒ′ s}
- }
- where
- module X = System X
-
- Sys-unitaryˡ-≥ : (X : System n) → X ≤ Sys.₁ id ⟨$⟩ (⊗ (discrete 0 , X))
- Sys-unitaryˡ-≥ {n} X = record
- { ⇒S = < Const X.S ⊤ₛ tt , Id X.S >ₛ
- ; ≗-fₛ = λ i s → cong (disc.fₛ ×-⇒ X.fₛ ∙ ε⇒ ×-function Id (Values n)) (sym-split-unitaryˡ {i})
- ; ≗-fₒ = λ s → sym-++-unitaryˡ {_ , X.fₒ′ s}
- }
- where
- module X = System X
- open SymmetricMonoidalCategory 0ℓ-Setoids-× using (module Equiv)
- open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (λ⇐)
- open Shorthands using (ε⇐; ε⇒)
- module disc = System (discrete 0)
- sym-split-unitaryˡ
- : λ⇐ ≈ ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)
- sym-split-unitaryˡ =
- 0ℓ-Setoids-×.Equiv.sym
- {Values n}
- {⊤ₛ ×ₛ Values n}
- {ε⇐ ×-function Id (Values n) ∙ splitₛ ∙ Pull.₁ ((λ ()) Vec.++ id)}
- {λ⇐}
- (unitaryˡ-inv {n})
- sym-++-unitaryˡ : proj₂ₛ {A = ⊤ₛ {0ℓ} {0ℓ}} ≈ Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)
- sym-++-unitaryˡ =
- 0ℓ-Setoids-×.Equiv.sym
- {⊤ₛ ×ₛ Values n}
- {Values n}
- {Push.₁ ((λ ()) Vec.++ id) ∙ ++ₛ ∙ Push,++,[].ε ×-function Id (Values n)}
- {proj₂ₛ}
- (Push,++,[].unitaryˡ {n})
-
-
- Sys-unitaryʳ-≤ : (X : System n) → Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0)) ≤ X
- Sys-unitaryʳ-≤ {n} X = record
- { ⇒S = proj₁ₛ
- ; ≗-fₛ = λ i (s , _) → cong (X.fₛ ∙ proj₁ₛ {B = ⊤ₛ {0ℓ}}) (unitaryʳ-inv {n} {i})
- ; ≗-fₒ = λ (s , _) → Push,++,[].unitaryʳ {n} {X.fₒ′ s , tt}
- }
- where
- module X = System X
-
- Sys-unitaryʳ-≥ : (X : System n) → X ≤ Sys.₁ (id Vec.++ (λ ())) ⟨$⟩ (⊗ {n} {0} (X , discrete 0))
- Sys-unitaryʳ-≥ {n} X = record
- { ⇒S = < Id X.S , Const X.S ⊤ₛ tt >ₛ
- ; ≗-fₛ = λ i s → cong (X.fₛ ×-⇒ disc.fₛ ∙ Id (Values n) ×-function ε⇒) sym-split-unitaryʳ {s , tt}
- ; ≗-fₒ = λ s → sym-++-unitaryʳ {X.fₒ′ s , tt}
- }
- where
- module X = System X
- module disc = System (discrete 0)
- open ⊗-Util.Shorthands 0ℓ-Setoids-×.monoidal using (ρ⇐)
- open Shorthands using (ε⇐; ε⇒)
- sym-split-unitaryʳ
- : ρ⇐ ≈ Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))
- sym-split-unitaryʳ =
- 0ℓ-Setoids-×.Equiv.sym
- {Values n}
- {Values n ×ₛ ⊤ₛ}
- {Id (Values n) ×-function ε⇐ ∙ splitₛ ∙ Pull.₁ (id Vec.++ (λ ()))}
- {ρ⇐}
- (unitaryʳ-inv {n})
- sym-++-unitaryʳ : proj₁ₛ {B = ⊤ₛ {0ℓ}} ≈ Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε
- sym-++-unitaryʳ =
- 0ℓ-Setoids-×.Equiv.sym
- {Values n ×ₛ ⊤ₛ}
- {Values n}
- {Push.₁ (id Vec.++ (λ ())) ∙ ++ₛ ∙ Id (Values n) ×-function Push,++,[].ε}
- {proj₁ₛ}
- (Push,++,[].unitaryʳ {n})
-
- Sys-braiding-compat-≤
- : (X : System n)
- (Y : System m)
- → Sys.₁ (+-swap {m} {n}) ⟨$⟩ (⊗ (X , Y)) ≤ ⊗ (Y , X)
- Sys-braiding-compat-≤ {n} {m} X Y = record
- { ⇒S = swapₛ
- ; ≗-fₛ = λ i (s₁ , s₂) → cong (Y.fₛ ×-⇒ X.fₛ ∙ swapₛ) (braiding-compat-inv {m} {n} {i}) {s₂ , s₁}
- ; ≗-fₒ = λ (s₁ , s₂) → Push,++,[].braiding-compat {n} {m} {X.fₒ′ s₁ , Y.fₒ′ s₂}
- }
- where
- module X = System X
- module Y = System Y
-
- Sys-braiding-compat-≥
- : (X : System n)
- (Y : System m)
- → ⊗ (Y , X) ≤ Sys.₁ (+-swap {m} {n}) ⟨$⟩ ⊗ (X , Y)
- Sys-braiding-compat-≥ {n} {m} X Y = record
- { ⇒S = swapₛ
- ; ≗-fₛ = λ i (s₂ , s₁) → cong (X.fₛ ×-⇒ Y.fₛ) (sym-braiding-compat-inv {i})
- ; ≗-fₒ = λ (s₂ , s₁) → sym-braiding-compat-++ {X.fₒ′ s₁ , Y.fₒ′ s₂}
- }
- where
- module X = System X
- module Y = System Y
- sym-braiding-compat-inv : swapₛ ∙ splitₛ {m} ≈ splitₛ ∙ Pull.₁ (+-swap {m} {n})
- sym-braiding-compat-inv {i} =
- 0ℓ-Setoids-×.Equiv.sym
- {Values (m + n)}
- {Values n ×ₛ Values m}
- {splitₛ ∙ Pull.₁ (+-swap {m} {n})}
- {swapₛ ∙ splitₛ {m}}
- (λ {j} → braiding-compat-inv {m} {n} {j}) {i}
- sym-braiding-compat-++ : ++ₛ {m} ∙ swapₛ ≈ Push.₁ (+-swap {m} {n}) ∙ ++ₛ
- sym-braiding-compat-++ {i} =
- 0ℓ-Setoids-×.Equiv.sym
- {Values n ×ₛ Values m}
- {Values (m + n)}
- {Push.₁ (+-swap {m} {n}) ∙ ++ₛ}
- {++ₛ {m} ∙ swapₛ}
- (Push,++,[].braiding-compat {n} {m})
-
-open Lax.SymmetricMonoidalFunctor
-
-Sys,⊗,ε : Lax.SymmetricMonoidalFunctor
-Sys,⊗,ε .F = Sys
-Sys,⊗,ε .isBraidedMonoidal = record
- { isMonoidal = record
- { ε = Sys-ε
- ; ⊗-homo = ⊗-homomorphism
- ; associativity = λ { {n} {m} {o} {(X , Y), Z} → ⊗-assoc-≤ X Y Z , ⊗-assoc-≥ X Y Z }
- ; unitaryˡ = λ { {n} {_ , X} → Sys-unitaryˡ-≤ X , Sys-unitaryˡ-≥ X }
- ; unitaryʳ = λ { {n} {X , _} → Sys-unitaryʳ-≤ X , Sys-unitaryʳ-≥ X }
- }
- ; braiding-compat = λ { {n} {m} {X , Y} → Sys-braiding-compat-≤ X Y , Sys-braiding-compat-≥ X Y }
- }
-
-module Sys,⊗,ε = Lax.SymmetricMonoidalFunctor Sys,⊗,ε
generated by cgit v1.2.3 (git 2.39.1) at 2026-01-28 15:21:53 +0000