diff options
Diffstat (limited to 'DecorationFunctor')
| -rw-r--r-- | DecorationFunctor/Graph.agda | 88 | ||||
| -rw-r--r-- | DecorationFunctor/Hypergraph.agda | 182 | ||||
| -rw-r--r-- | DecorationFunctor/Hypergraph/Labeled.agda | 304 | ||||
| -rw-r--r-- | DecorationFunctor/Trivial.agda | 85 |
4 files changed, 290 insertions, 369 deletions
diff --git a/DecorationFunctor/Graph.agda b/DecorationFunctor/Graph.agda index d8a0187..8b62430 100644 --- a/DecorationFunctor/Graph.agda +++ b/DecorationFunctor/Graph.agda @@ -4,62 +4,48 @@ module DecorationFunctor.Graph where import Categories.Morphism as Morphism +open import Level using (0ℓ) + open import Categories.Category.BinaryProducts using (module BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) -open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) open import Categories.Category.Product using (_⁂_) open import Categories.Functor using () renaming (_∘F_ to _∘′_) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Monoidal.Symmetric using (module Lax) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) - open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) - +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′) open import Data.Empty using (⊥-elim) -open import Data.Fin using (#_) -open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_) +open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_) open import Data.Fin.Patterns using (0F; 1F) open import Data.Fin.Properties using (splitAt-join; join-splitAt; splitAt-↑ˡ; splitAt⁻¹-↑ˡ) open import Data.Nat using (ℕ; _+_) open import Data.Product.Base using (_,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid) +open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ) open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap) renaming ([_,_]′ to [_,_]) open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; map-cong; swap-involutive) open import Data.Unit using (tt) -open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) - -open import Function.Base using (_∘_; id; const; case_of_) -open import Function.Bundles using (Func; Inverse; _↔_; mk↔) +open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔) open import Function.Construct.Composition using (_↔-∘_) +open import Function.Construct.Constant using () renaming (function to Const) open import Function.Construct.Identity using (↔-id) open import Function.Construct.Symmetry using (↔-sym) - -open import Level using (0ℓ; lift) - -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality using (_≗_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_; _≡_; erefl; refl; sym; trans; cong) open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning) open import Relation.Nullary.Negation.Core using (¬_) open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) -open Cocartesian Nat-Cocartesian using (coproducts) open FinitelyCocompleteCategory Nat-FinitelyCocomplete - using () - renaming (symmetricMonoidalCategory to Nat-smc) -open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) + using (-+-) + renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc) open Lax using (SymmetricMonoidalFunctor) - open BinaryProducts products using (-×-) -open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc) record Graph (v : ℕ) : Set where @@ -182,18 +168,15 @@ F = record ; F-resp-≈ = λ f≗g → F-resp-≈ f≗g } -empty-graph : Graph 0 -empty-graph = record +discrete : {n : ℕ} → Graph n +discrete = record { e = 0 ; s = λ () ; t = λ () } -ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Graph-setoid 0) -ε = record - { to = const empty-graph - ; cong = const Graph-same-refl - } +ε : Func ⊤ₛ (Graph-setoid 0) +ε = Const ⊤ₛ (Graph-setoid 0) discrete together : Graph n → Graph m → Graph (n + m) together {n} {m} G₁ G₂ = record @@ -521,7 +504,7 @@ associativity {X} {Y} {Z} G₁ G₂ G₃ = record (G₁+[G₂+G₃].t ∘ [ [ _↑ˡ G₂.e + G₃.e , (G₁.e ↑ʳ_) ∘ (_↑ˡ G₃.e) ] ∘ splitAt G₁.e , (G₁.e ↑ʳ_) ∘ (G₂.e ↑ʳ_) ] ∘ splitAt _) x ≡⟨⟩ (G₁+[G₂+G₃].t ∘ to (+-assoc-↔ G₁.e G₂.e G₃.e)) x ∎ -unitaryˡ : Graph-same (together empty-graph G) G +unitaryˡ : Graph-same (together (discrete {0}) G) G unitaryˡ = Graph-same-refl n+0↔n : ∀ n → Fin (n + 0) ↔ Fin n @@ -544,7 +527,7 @@ n+0↔n n = record unitaryʳ : {G : Graph n} - → Graph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together G empty-graph)) G + → Graph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together G discrete)) G unitaryʳ {n} {G} = record { ↔e = e+0↔e ; ≗s = ≗s+0 @@ -637,28 +620,27 @@ braiding {n} {m} {G₁} {G₂} = record ≡⟨ (cong (join m n ∘ map G₂.t G₁.t) ∘ splitAt-join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ⟨ (join m n ∘ map G₂.t G₁.t ∘ splitAt G₂.e ∘ join G₂.e G₁.e ∘ swap ∘ splitAt G₁.e) x ∎ -graph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) -graph = record - { F = F - ; isBraidedMonoidal = record - { isMonoidal = record - { ε = ε - ; ⊗-homo = ⊗-homomorphism - ; associativity = λ { {x} {y} {z} {(G₁ , G₂) , G₃} → associativity G₁ G₂ G₃ } - ; unitaryˡ = unitaryˡ - ; unitaryʳ = unitaryʳ - } - ; braiding-compat = λ { {x} {y} {G₁ , G₂} → braiding {G₁ = G₁} {G₂ = G₂} } - } - } +opaque + unfolding ×-symmetric′ + graph : SymmetricMonoidalFunctor Nat-smc Setoids-× + graph = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = λ { {x} {y} {z} {(G₁ , G₂) , G₃} → associativity G₁ G₂ G₃ } + ; unitaryˡ = unitaryˡ + ; unitaryʳ = unitaryʳ + } + ; braiding-compat = λ { {x} {y} {G₁ , G₂} → braiding {G₁ = G₁} {G₂ = G₂} } + } + } module F = SymmetricMonoidalFunctor graph -and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3) -and-gate = record - { to = λ { (lift tt) → and-graph } - ; cong = λ { (lift tt) → Graph-same-refl } - } +and-gate : Func ⊤ₛ (Graph-setoid 3) +and-gate = Const ⊤ₛ (Graph-setoid 3) and-graph where and-graph : Graph 3 and-graph = record diff --git a/DecorationFunctor/Hypergraph.agda b/DecorationFunctor/Hypergraph.agda index 5cd83f3..2f61bc3 100644 --- a/DecorationFunctor/Hypergraph.agda +++ b/DecorationFunctor/Hypergraph.agda @@ -3,65 +3,51 @@ module DecorationFunctor.Hypergraph where import Categories.Morphism as Morphism +open import Level using (0ℓ) open import Categories.Category.BinaryProducts using (module BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) open import Categories.Category.Product using (_⁂_) open import Categories.Functor using () renaming (_∘F_ to _∘′_) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Monoidal.Symmetric using (module Lax) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) - open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) - +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′) open import Data.Empty using (⊥-elim) -open import Data.Fin using (#_) -open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; Fin′; toℕ; cast) +open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; toℕ; cast) open import Data.Fin.Patterns using (0F; 1F; 2F) -open import Data.Fin.Permutation using (lift₀) open import Data.Fin.Properties using (splitAt-join; join-splitAt; cast-is-id; cast-trans; toℕ-cast; subst-is-cast; splitAt-↑ˡ; splitAt-↑ʳ; splitAt⁻¹-↑ˡ; ↑ˡ-injective) open import Data.Nat using (ℕ; _+_) open import Data.Product.Base using (_,_; Σ) -open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid) -open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_]) +open import Data.Setoid using (∣_∣) +open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ) +open import Data.Sum using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_]) open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive) open import Data.Unit using (tt) -open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) - -open import Function.Base using (_∘_; id; const; case_of_; case_returning_of_) -open import Function.Bundles using (Func; Inverse; _↔_; mk↔) +open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔; _⟨$⟩_) open import Function.Construct.Composition using (_↔-∘_) -open import Function.Construct.Identity using (↔-id) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using (↔-id) renaming (function to Id) open import Function.Construct.Symmetry using (↔-sym) - -open import Level using (0ℓ; lift) - -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality using (_≗_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality.Core using (_≗_; _≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app) open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong₂; subst-∘) open import Relation.Nullary.Negation.Core using (¬_) open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) -open Cocartesian Nat-Cocartesian using (coproducts) open FinitelyCocompleteCategory Nat-FinitelyCocomplete - using () - renaming (symmetricMonoidalCategory to Nat-smc) + using (-+-; _+₁_) + renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc) open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) open Lax using (SymmetricMonoidalFunctor) open BinaryProducts products using (-×-) -open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc) - record Hypergraph (v : ℕ) : Set where @@ -80,7 +66,6 @@ record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set where open Hypergraph H public open Hypergraph H′ renaming (h to h′; a to a′; arity to arity′; j to j′) public - field ↔h : Fin h ↔ Fin h′ @@ -165,8 +150,8 @@ Hypergraph-same-trans ≡H₁ ≡H₂ = record ≡⟨ cong (j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e))) (cast-trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e)) i) ⟩ j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e))) i) ∎ -Hypergraph-setoid : ℕ → Setoid 0ℓ 0ℓ -Hypergraph-setoid p = record +Hypergraphₛ : ℕ → Setoid 0ℓ 0ℓ +Hypergraphₛ p = record { Carrier = Hypergraph p ; _≈_ = Hypergraph-same ; isEquivalence = record @@ -192,12 +177,12 @@ Hypergraph-same-cong Hypergraph-same-cong f ≡H = record { ↔h = ↔h ; ≗a = ≗a - ; ≗j = λ { e i → cong f (≗j e i) } + ; ≗j = λ e i → cong f (≗j e i) } where open Hypergraph-same ≡H -Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraph-setoid n) (Hypergraph-setoid m) +Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraphₛ n) (Hypergraphₛ m) Hypergraph-Func f = record { to = map-nodes f ; cong = Hypergraph-same-cong f @@ -229,7 +214,7 @@ homomorphism {n} {m} {o} {H} f g = record F : Functor Nat (Setoids 0ℓ 0ℓ) F = record - { F₀ = Hypergraph-setoid + { F₀ = Hypergraphₛ ; F₁ = Hypergraph-Func ; identity = λ { {n} {H} → Hypergraph-same-refl {H = H} } ; homomorphism = λ { {f = f} {g = g} → homomorphism f g } @@ -238,18 +223,18 @@ F = record -- monoidal structure -empty-hypergraph : Hypergraph 0 -empty-hypergraph = record +discrete : {n : ℕ} → Hypergraph n +discrete {n} = record { h = 0 ; a = λ () ; j = λ () } -ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Hypergraph-setoid 0) -ε = record - { to = const empty-hypergraph - ; cong = const Hypergraph-same-refl - } +opaque + unfolding ×-symmetric′ + + ε : Func Setoids-×.unit (Hypergraphₛ 0) + ε = Const ⊤ₛ (Hypergraphₛ 0) discrete module _ (H₁ : Hypergraph n) (H₂ : Hypergraph m) where private @@ -364,7 +349,7 @@ commute → (g : Fin m → Fin m′) → Hypergraph-same (together (map-nodes f H₁) (map-nodes g H₂)) - (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂)) + (map-nodes (f +₁ g) (together H₁ H₂)) commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record { ↔h = ≡H₁+H₂.↔h ; ≗a = ≡H₁+H₂.≗a @@ -380,23 +365,36 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record ≗j : (e : Fin (H₁.h + H₂.h)) (i : Fin ((ℕ.suc ∘ [ H₁.a , H₂.a ] ∘ splitAt H₁.h) e)) → j (together (map-nodes f H₁) (map-nodes g H₂)) e i - ≡ j (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i) + ≡ j (map-nodes (f +₁ g) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i) ≗j e i with splitAt H₁.h e ... | inj₁ e₁ rewrite splitAt-↑ˡ n (H₁.j e₁ (cast refl i)) m = cong ((_↑ˡ m′) ∘ f ∘ H₁.j e₁) (sym (cast-is-id refl i)) ... | inj₂ e₂ rewrite splitAt-↑ʳ n m (H₂.j e₂ (cast refl i)) = cong ((n′ ↑ʳ_) ∘ g ∘ H₂.j e₂) (sym (cast-is-id refl i)) -⊗-homomorphism : NaturalTransformation (-×- ∘′ (F ⁂ F)) (F ∘′ -+-) -⊗-homomorphism = record - { η = λ { (m , n) → η } - ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g } - ; sym-commute = λ { (f , g) {H₁ , H₂} → Hypergraph-same-sym (commute {H₁ = H₁} {H₂ = H₂} f g) } +open Setoids-× using (_⊗₀_; _⊗₁_) +opaque + unfolding ×-symmetric′ + η : Func (Hypergraphₛ n ⊗₀ Hypergraphₛ m) (Hypergraphₛ (n + m)) + η = record + { to = λ (H₁ , H₂) → together H₁ H₂ + ; cong = λ (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ + } + +opaque + unfolding η + commute′ + : (f : Fin n → Fin n′) + → (g : Fin m → Fin m′) + → {x : ∣ Hypergraphₛ n ⊗₀ Hypergraphₛ m ∣} + → Hypergraph-same + (η ⟨$⟩ (Hypergraph-Func f ⊗₁ Hypergraph-Func g ⟨$⟩ x)) + (map-nodes (f +₁ g) (η ⟨$⟩ x)) + commute′ f g {H₁ , H₂} = commute {H₁ = H₁} {H₂} f g + +⊗-homomorphism : NaturalTransformation (Setoids-×.⊗ ∘′ (F ⁂ F)) (F ∘′ -+-) +⊗-homomorphism = ntHelper record + { η = λ (n , m) → η {n} {m} + ; commute = λ (f , g) → commute′ f g } - where - η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m)) - η = record - { to = λ { (H₁ , H₂) → together H₁ H₂ } - ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } - } +-assoc-↔ : ∀ (x y z : ℕ) → Fin (x + y + z) ↔ Fin (x + (y + z)) +-assoc-↔ x y z = record @@ -412,13 +410,13 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record associativity : {X Y Z : ℕ} - → {H₁ : Hypergraph X} - → {H₂ : Hypergraph Y} - → {H₃ : Hypergraph Z} + → (H₁ : Hypergraph X) + → (H₂ : Hypergraph Y) + → (H₃ : Hypergraph Z) → Hypergraph-same (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together H₁ H₂) H₃)) (together H₁ (together H₂ H₃)) -associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record +associativity {X} {Y} {Z} H₁ H₂ H₃ = record { ↔h = ↔h ; ≗a = ≗a ; ≗j = ≗j @@ -472,7 +470,6 @@ associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record rewrite splitAt-↑ˡ (X + Y) (H₁.j e₁ i ↑ˡ Y) Z rewrite splitAt-↑ˡ X (H₁.j e₁ i) Y = cong ((_↑ˡ Y + Z) ∘ H₁.j e₁) (sym (cast-is-id refl i)) ≗j e i | inj₁ e₁₂ | inj₂ e₂ - rewrite splitAt-↑ʳ H₁.h H₂.h e₂ rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h) rewrite splitAt-↑ˡ H₂.h e₂ H₃.h rewrite splitAt-↑ˡ (X + Y) (X ↑ʳ H₂.j e₂ i) Z @@ -500,7 +497,7 @@ n+0↔n n = record to∘from : (x : Fin n) → to (from x) ≡ x to∘from x rewrite splitAt-↑ˡ n x 0 = refl -unitaryʳ : Hypergraph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together H empty-hypergraph)) H +unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H discrete)) H unitaryʳ {n} {H} = record { ↔h = h+0↔h ; ≗a = ≗a @@ -508,22 +505,22 @@ unitaryʳ {n} {H} = record } where module H = Hypergraph H - module H+0 = Hypergraph (together H empty-hypergraph) + module H+0 = Hypergraph (together {n} {0} H discrete) h+0↔h : Fin H+0.h ↔ Fin H.h h+0↔h = n+0↔n H.h ≗a : (e : Fin (H.h + 0)) → [ H.a , (λ ()) ] (splitAt H.h e) ≡ H.a (Inverse.to h+0↔h e) ≗a e with inj₁ e₁ ← splitAt H.h e in eq = refl ≗j : (e : Fin (H.h + 0)) (i : Fin (ℕ.suc ([ H.a , (λ ()) ] (splitAt H.h e)))) - → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H empty-hypergraph e i)) + → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H discrete e i)) ≡ H.j (Inverse.to h+0↔h e) (cast (cong ℕ.suc (≗a e)) i) - ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H empty-hypergraph e) refl (≗a e) i + ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H discrete e) refl (≗a e) i where ≗j-aux : (w : Fin H.h ⊎ Fin 0) → (eq₁ : splitAt H.h e ≡ w) → (w₁ : Fin (ℕ.suc ([ H.a , (λ ()) ] w)) → Fin (n + 0)) - → j+j H empty-hypergraph e ≡ subst (λ hole → Fin (ℕ.suc ([ H.a , (λ ()) ] hole)) → Fin (n + 0)) (sym eq₁) w₁ + → j+j H discrete e ≡ subst (λ hole → Fin (ℕ.suc ([ H.a , (λ ()) ] hole)) → Fin (n + 0)) (sym eq₁) w₁ → (w₂ : [ H.a , (λ ()) ] w ≡ H.a (Inverse.to h+0↔h e)) (i : Fin (ℕ.suc ([ H.a , (λ ()) ] w))) → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i)) @@ -594,43 +591,60 @@ braiding {n} {m} {H₁} {H₂} = record rewrite splitAt-↑ʳ n m (H₂.j e₂ i) rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = cong ((_↑ˡ n) ∘ H₂.j e₂) (sym (cast-is-id refl i)) -hypergraph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) +opaque + unfolding η ε + + associativity′ + : {n m o : ℕ} + → {x : ∣ (Hypergraphₛ n ⊗₀ Hypergraphₛ m) ⊗₀ Hypergraphₛ o ∣} + → Hypergraph-same + (map-nodes (Inverse.to (+-assoc-↔ n m o)) (η {n + m} {o} ⟨$⟩ ((η {n} {m} ⊗₁ (Id _)) ⟨$⟩ x))) + (η {n} {m + o} ⟨$⟩ ((Id _ ⊗₁ η {m} {o}) ⟨$⟩ (Setoids-×.associator.from ⟨$⟩ x))) + associativity′ {n} {m} {o} {(x , y) , z} = associativity x y z + + unitaryˡ′ + : {X : ∣ Setoids-×.unit ⊗₀ Hypergraphₛ n ∣} + → Hypergraph-same (η {0} {n} ⟨$⟩ ((ε ⊗₁ Id _) ⟨$⟩ X)) (Setoids-×.unitorˡ.from ⟨$⟩ X) + unitaryˡ′ = Hypergraph-same-refl + + unitaryʳ′ + : {X : ∣ Hypergraphₛ n ⊗₀ Setoids-×.unit ∣} + → Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (η {n} {0} ⟨$⟩ ((Id _ ⊗₁ ε) ⟨$⟩ X))) (Setoids-×.unitorʳ.from ⟨$⟩ X) + unitaryʳ′ = unitaryʳ + + braiding-compat + : {n m : ℕ} + → {X : ∣ Hypergraphₛ n ⊗₀ Hypergraphₛ m ∣} + → Hypergraph-same + (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (η {n} {m} ⟨$⟩ X)) + (η {m} {n} ⟨$⟩ (Setoids-×.braiding.⇒.η (Hypergraphₛ n , Hypergraphₛ m) ⟨$⟩ X)) + braiding-compat {n} {m} {H₁ , H₂} = braiding {n} {m} {H₁} {H₂} + +hypergraph : SymmetricMonoidalFunctor Nat-smc Setoids-× hypergraph = record { F = F ; isBraidedMonoidal = record { isMonoidal = record { ε = ε - ; ⊗-homo = ntHelper record - { η = λ { (m , n) → η } - ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g } - } - ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} } - ; unitaryˡ = Hypergraph-same-refl - ; unitaryʳ = unitaryʳ + ; ⊗-homo = ⊗-homomorphism + ; associativity = associativity′ + ; unitaryˡ = unitaryˡ′ + ; unitaryʳ = unitaryʳ′ } - ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} } + ; braiding-compat = braiding-compat } } - where - η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m)) - η = record - { to = λ { (H₁ , H₂) → together H₁ H₂ } - ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } - } module F = SymmetricMonoidalFunctor hypergraph -and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3) -and-gate = record - { to = λ { (lift tt) → and-graph } - ; cong = λ { (lift tt) → Hypergraph-same-refl } - } +and-gate : Func ⊤ₛ (F.₀ 3) +and-gate = Const ⊤ₛ (Hypergraphₛ 3) and-graph where and-graph : Hypergraph 3 and-graph = record { h = 1 ; a = λ { 0F → 2 } - ; j = λ { 0F → edge-0-nodes } + ; j = λ { 0F → id } } where edge-0-nodes : Fin 3 → Fin 3 diff --git a/DecorationFunctor/Hypergraph/Labeled.agda b/DecorationFunctor/Hypergraph/Labeled.agda index d8f6e64..31402b1 100644 --- a/DecorationFunctor/Hypergraph/Labeled.agda +++ b/DecorationFunctor/Hypergraph/Labeled.agda @@ -1,33 +1,27 @@ {-# OPTIONS --without-K --safe #-} -module DecorationFunctor.Hypergraph.Labeled where +open import Level using (Level) + +module DecorationFunctor.Hypergraph.Labeled {c ℓ : Level} where import Categories.Morphism as Morphism open import Categories.Category.BinaryProducts using (module BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) open import Categories.Category.Product using (_⁂_) open import Categories.Functor using () renaming (_∘F_ to _∘′_) open import Categories.Functor.Core using (Functor) open import Categories.Functor.Monoidal.Symmetric using (module Lax) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) - open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) - -open import Data.Empty using (⊥-elim) -open import Data.Fin using (#_) -open import Data.Fin.Base using (Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; Fin′; cast) -open import Data.Fin.Patterns using (0F; 1F) -open import Data.Fin.Permutation using (lift₀) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′) +open import Data.Fin using (#_; Fin; splitAt; join; zero; suc; _↑ˡ_; _↑ʳ_; cast) +open import Data.Fin.Patterns using (0F; 1F; 2F) open import Data.Fin.Properties using ( splitAt-join ; join-splitAt @@ -37,89 +31,45 @@ open import Data.Fin.Properties ) open import Data.Nat using (ℕ; _+_) open import Data.Product.Base using (_,_; Σ) -open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid.Unit {c} {ℓ} using (⊤ₛ) open import Data.Sum.Base using (_⊎_; map; inj₁; inj₂; swap; map₂) renaming ([_,_]′ to [_,_]) open import Data.Sum.Properties using (map-map; [,]-map; [,]-∘; [-,]-cong; [,-]-cong; [,]-cong; map-cong; swap-involutive) -open import Data.Unit using (tt) open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) - -open import Function.Base using (_∘_; id; const; case_of_; case_returning_of_) -open import Function.Bundles using (Func; Inverse; _↔_; mk↔) +open import Function using (_∘_; id; const; Func; Inverse; _↔_; mk↔; _⟶ₛ_) open import Function.Construct.Composition using (_↔-∘_) +open import Function.Construct.Constant using () renaming (function to Const) open import Function.Construct.Identity using (↔-id) open import Function.Construct.Symmetry using (↔-sym) - -open import Level using (0ℓ; lift) - -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.PropositionalEquality using (_≗_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app) +open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_; _≡_; erefl; refl; sym; trans; cong; cong₂; subst; cong-app) open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence; module ≡-Reasoning; dcong; dcong₂; subst-∘; subst-subst; sym-cong; subst-subst-sym; trans-cong; cong-∘; trans-reflʳ) open import Relation.Nullary.Negation.Core using (¬_) -open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) -open Cocartesian Nat-Cocartesian using (coproducts) +open Cartesian (Setoids-Cartesian {c} {ℓ}) using (products) open FinitelyCocompleteCategory Nat-FinitelyCocomplete - using () - renaming (symmetricMonoidalCategory to Nat-smc) -open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) + using (-+-) + renaming (symmetricMonoidalCategory to Nat-smc; +-assoc to Nat-+-assoc) +open import Category.Monoidal.Instance.Nat using (Nat,+,0) +open Morphism (Setoids c ℓ) using (_≅_) open Lax using (SymmetricMonoidalFunctor) open BinaryProducts products using (-×-) -open BinaryCoproducts coproducts using (-+-) renaming (+-assoc to Nat-+-assoc) - - -data Gate : ℕ → Set where - ZERO : Gate 1 - ONE : Gate 1 - NOT : Gate 2 - AND : Gate 3 - OR : Gate 3 - XOR : Gate 3 - NAND : Gate 3 - NOR : Gate 3 - XNOR : Gate 3 - -cast-gate : {e e′ : ℕ} → .(e ≡ e′) → Gate e → Gate e′ -cast-gate {1} {1} eq g = g -cast-gate {2} {2} eq g = g -cast-gate {3} {3} eq g = g - -cast-gate-trans - : {m n o : ℕ} - → .(eq₁ : m ≡ n) - .(eq₂ : n ≡ o) - (g : Gate m) - → cast-gate eq₂ (cast-gate eq₁ g) ≡ cast-gate (trans eq₁ eq₂) g -cast-gate-trans {1} {1} {1} eq₁ eq₂ g = refl -cast-gate-trans {2} {2} {2} eq₁ eq₂ g = refl -cast-gate-trans {3} {3} {3} eq₁ eq₂ g = refl - -cast-gate-is-id : {m : ℕ} .(eq : m ≡ m) (g : Gate m) → cast-gate eq g ≡ g -cast-gate-is-id {1} eq g = refl -cast-gate-is-id {2} eq g = refl -cast-gate-is-id {3} eq g = refl - -subst-is-cast-gate : {m n : ℕ} (eq : m ≡ n) (g : Gate m) → subst Gate eq g ≡ cast-gate eq g -subst-is-cast-gate refl g = sym (cast-gate-is-id refl g) - -record Hypergraph (v : ℕ) : Set where - field - h : ℕ - a : Fin h → ℕ +open import Data.Circuit.Gate using (Gate; cast-gate; cast-gate-trans; cast-gate-is-id; subst-is-cast-gate) - arity : Fin h → ℕ - arity = ℕ.suc ∘ a +record Hypergraph (v : ℕ) : Set c where field - j : (e : Fin h) → Fin (arity e) → Fin v - l : (e : Fin h) → Gate (arity e) + h : ℕ + a : Fin h → ℕ + j : (e : Fin h) → Fin (a e) → Fin v + l : (e : Fin h) → Gate (a e) -record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set where +record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set ℓ where open Hypergraph H public - open Hypergraph H′ renaming (h to h′; a to a′; arity to arity′; j to j′; l to l′) public + open Hypergraph H′ renaming (h to h′; a to a′; j to j′; l to l′) public field ↔h : Fin h ↔ Fin h′ @@ -128,18 +78,13 @@ record Hypergraph-same {n : ℕ} (H H′ : Hypergraph n) : Set where field ≗a : a ≗ a′ ∘ to - - ≗arity : arity ≗ arity′ ∘ to - ≗arity e = cong ℕ.suc (≗a e) - - field ≗j : (e : Fin h) - (i : Fin (arity e)) + (i : Fin (a e)) → j e i - ≡ j′ (to e) (cast (≗arity e) i) + ≡ j′ (to e) (cast (≗a e) i) ≗l : (e : Fin h) → l e - ≡ cast-gate (sym (≗arity e)) (l′ (to e)) + ≡ cast-gate (sym (≗a e)) (l′ (to e)) private @@ -179,28 +124,28 @@ Hypergraph-same-sym {V} {H} {H′} ≡H = record a′ x ∎ id≗to∘from : id ≗ to ∘ from id≗to∘from e = sym (inverseˡ refl) - ≗arity′ : arity′ ≗ arity ∘ from - ≗arity′ e = cong ℕ.suc (sym (a∘from≗a′ e)) - ≗arity- : arity′ ≗ arity′ ∘ to ∘ from - ≗arity- e = cong arity′ (id≗to∘from e) + ≗arity′ : a′ ≗ a ∘ from + ≗arity′ e = sym (a∘from≗a′ e) + ≗arity- : a′ ≗ a′ ∘ to ∘ from + ≗arity- e = cong a′ (id≗to∘from e) - ≗j′ : (e : Fin h′) (i : Fin (arity′ e)) → j′ e i ≡ j (from e) (cast (≗arity′ e) i) + ≗j′ : (e : Fin h′) (i : Fin (a′ e)) → j′ e i ≡ j (from e) (cast (≗arity′ e) i) ≗j′ e i = begin - j′ e i ≡⟨ dcong₂ j′ (id≗to∘from e) (subst-∘ (id≗to∘from e)) ⟩ - j′ (to (from e)) (subst Fin (cong arity′ (id≗to∘from e)) i) ≡⟨ cong (j′ (to (from e))) (subst-is-cast (cong arity′ (id≗to∘from e)) i) ⟩ - j′ (to (from e)) (cast (cong arity′ (id≗to∘from e)) i) ≡⟨⟩ - j′ (to (from e)) (cast (trans (≗arity′ e) (≗arity (from e))) i) ≡⟨ cong (j′ (to (from e))) (cast-trans (≗arity′ e) (≗arity (from e)) i) ⟨ - j′ (to (from e)) (cast (≗arity (from e)) (cast (≗arity′ e) i)) ≡⟨ ≗j (from e) (cast (≗arity′ e) i) ⟨ - j (from e) (cast (≗arity′ e) i) ∎ - - ≗l′ : (e : Fin h′) → l′ e ≡ cast-gate (sym (cong ℕ.suc (sym (a∘from≗a′ e)))) (l (from e)) + j′ e i ≡⟨ dcong₂ j′ (id≗to∘from e) (subst-∘ (id≗to∘from e)) ⟩ + j′ (to (from e)) (subst Fin (cong a′ (id≗to∘from e)) i) ≡⟨ cong (j′ (to (from e))) (subst-is-cast (cong a′ (id≗to∘from e)) i) ⟩ + j′ (to (from e)) (cast (cong a′ (id≗to∘from e)) i) ≡⟨⟩ + j′ (to (from e)) (cast (trans (≗arity′ e) (≗a (from e))) i) ≡⟨ cong (j′ (to (from e))) (cast-trans (≗arity′ e) (≗a (from e)) i) ⟨ + j′ (to (from e)) (cast (≗a (from e)) (cast (≗arity′ e) i)) ≡⟨ ≗j (from e) (cast (≗arity′ e) i) ⟨ + j (from e) (cast (≗arity′ e) i) ∎ + + ≗l′ : (e : Fin h′) → l′ e ≡ cast-gate (sym (sym (a∘from≗a′ e))) (l (from e)) ≗l′ e = begin l′ e ≡⟨ dcong l′ (sym (id≗to∘from e)) ⟨ - subst (Gate ∘ arity′) (sym (id≗to∘from e)) (l′ (to (from e))) ≡⟨ subst-∘ (sym (id≗to∘from e)) ⟩ - subst Gate (cong arity′ (sym (id≗to∘from e))) (l′ (to (from e))) ≡⟨ subst-is-cast-gate (cong arity′ (sym (id≗to∘from e))) (l′ (to (from e))) ⟩ - cast-gate _ (l′ (to (from e))) ≡⟨ cast-gate-trans _ (sym (cong ℕ.suc (sym (a∘from≗a′ e)))) (l′ (to (from e))) ⟨ - cast-gate (sym (cong ℕ.suc (sym (a∘from≗a′ e)))) (cast-gate _ (l′ (to (from e)))) ≡⟨ cong (cast-gate (sym (cong ℕ.suc (sym (a∘from≗a′ e))))) (≗l (from e)) ⟨ - cast-gate (sym (cong ℕ.suc (sym (a∘from≗a′ e)))) (l (from e)) ∎ + subst (Gate ∘ a′) (sym (id≗to∘from e)) (l′ (to (from e))) ≡⟨ subst-∘ (sym (id≗to∘from e)) ⟩ + subst Gate (cong a′ (sym (id≗to∘from e))) (l′ (to (from e))) ≡⟨ subst-is-cast-gate (cong a′ (sym (id≗to∘from e))) (l′ (to (from e))) ⟩ + cast-gate _ (l′ (to (from e))) ≡⟨ cast-gate-trans _ (sym (sym (a∘from≗a′ e))) (l′ (to (from e))) ⟨ + cast-gate (sym (sym (a∘from≗a′ e))) (cast-gate _ (l′ (to (from e)))) ≡⟨ cong (cast-gate (sym (sym (a∘from≗a′ e)))) (≗l (from e)) ⟨ + cast-gate (sym (sym (a∘from≗a′ e))) (l (from e)) ∎ Hypergraph-same-trans : Hypergraph-same H H′ → Hypergraph-same H′ H″ → Hypergraph-same H H″ Hypergraph-same-trans ≡H₁ ≡H₂ = record @@ -214,19 +159,19 @@ Hypergraph-same-trans ≡H₁ ≡H₂ = record open Inverse open ≡-Reasoning ≗j₂ : (e : Fin (h ≡H₁)) - (i : Fin (arity ≡H₁ e)) - → j ≡H₂ (to (↔h ≡H₁) e) (cast (≗arity ≡H₁ e) i) - ≡ j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e))) i) + (i : Fin (a ≡H₁ e)) + → j ≡H₂ (to (↔h ≡H₁) e) (cast (≗a ≡H₁ e) i) + ≡ j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗a ≡H₁ e) (≗a ≡H₂ (to (↔h ≡H₁) e))) i) ≗j₂ e i = begin - j ≡H₂ (to (↔h ≡H₁) e) (cast (≗arity ≡H₁ e) i) - ≡⟨ ≗j ≡H₂ (to (↔h ≡H₁) e) (cast (≗arity ≡H₁ e) i) ⟩ - j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (≗arity ≡H₂ (to (↔h ≡H₁) e)) (cast (≗arity ≡H₁ e) i)) - ≡⟨ cong (j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e))) (cast-trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e)) i) ⟩ - j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗arity ≡H₁ e) (≗arity ≡H₂ (to (↔h ≡H₁) e))) i) ∎ + j ≡H₂ (to (↔h ≡H₁) e) (cast (≗a ≡H₁ e) i) + ≡⟨ ≗j ≡H₂ (to (↔h ≡H₁) e) (cast (≗a ≡H₁ e) i) ⟩ + j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (≗a ≡H₂ (to (↔h ≡H₁) e)) (cast (≗a ≡H₁ e) i)) + ≡⟨ cong (j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e))) (cast-trans (≗a ≡H₁ e) (≗a ≡H₂ (to (↔h ≡H₁) e)) i) ⟩ + j′ ≡H₂ (to (↔h ≡H₂) (to (↔h ≡H₁) e)) (cast (trans (≗a ≡H₁ e) (≗a ≡H₂ (to (↔h ≡H₁) e))) i) ∎ ≗l₂ : (e : Fin (h ≡H₁)) → cast-gate _ (l′ ≡H₁ (to ≡H₁ e)) ≡ cast-gate _ (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e))) - ≗l₂ e = trans (cong (cast-gate _) (≗l ≡H₂ (to ≡H₁ e))) (cast-gate-trans _ (sym (≗arity ≡H₁ e)) (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e)))) + ≗l₂ e = trans (cong (cast-gate _) (≗l ≡H₂ (to ≡H₁ e))) (cast-gate-trans _ (sym (≗a ≡H₁ e)) (l′ ≡H₂ (to ≡H₂ (to ≡H₁ e)))) -Hypergraph-setoid : ℕ → Setoid 0ℓ 0ℓ +Hypergraph-setoid : ℕ → Setoid c ℓ Hypergraph-setoid p = record { Carrier = Hypergraph p ; _≈_ = Hypergraph-same @@ -260,7 +205,7 @@ Hypergraph-same-cong f ≡H = record where open Hypergraph-same ≡H -Hypergraph-Func : (Fin n → Fin m) → Func (Hypergraph-setoid n) (Hypergraph-setoid m) +Hypergraph-Func : (Fin n → Fin m) → Hypergraph-setoid n ⟶ₛ Hypergraph-setoid m Hypergraph-Func f = record { to = map-nodes f ; cong = Hypergraph-same-cong f @@ -292,9 +237,9 @@ homomorphism {n} {m} {o} {H} f g = record where open Hypergraph-same Hypergraph-same-refl -F : Functor Nat (Setoids 0ℓ 0ℓ) +F : Functor Nat (Setoids c ℓ) F = record - { F₀ = Hypergraph-setoid + { F₀ = λ n → Hypergraph-setoid n ; F₁ = Hypergraph-Func ; identity = λ { {n} {H} → Hypergraph-same-refl {H = H} } ; homomorphism = λ { {f = f} {g = g} → homomorphism f g } @@ -303,31 +248,28 @@ F = record -- monoidal structure -empty-hypergraph : Hypergraph 0 -empty-hypergraph = record +discrete : {n : ℕ} → Hypergraph n +discrete = record { h = 0 ; a = λ () ; j = λ () ; l = λ () } -ε : Func (SingletonSetoid {0ℓ} {0ℓ}) (Hypergraph-setoid 0) -ε = record - { to = const empty-hypergraph - ; cong = const Hypergraph-same-refl - } +ε : ⊤ₛ ⟶ₛ Hypergraph-setoid 0 +ε = Const ⊤ₛ (Hypergraph-setoid 0) discrete module _ (H₁ : Hypergraph n) (H₂ : Hypergraph m) where private module H₁ = Hypergraph H₁ module H₂ = Hypergraph H₂ j+j : (e : Fin (H₁.h + H₂.h)) - → Fin (ℕ.suc ([ H₁.a , H₂.a ] (splitAt H₁.h e))) + → Fin ([ H₁.a , H₂.a ] (splitAt H₁.h e)) → Fin (n + m) j+j e i with splitAt H₁.h e ... | inj₁ e₁ = H₁.j e₁ i ↑ˡ m ... | inj₂ e₂ = n ↑ʳ H₂.j e₂ i - l+l : (e : Fin (H₁.h + H₂.h)) → Gate (ℕ.suc ([ H₁.a , H₂.a ] (splitAt H₁.h e))) + l+l : (e : Fin (H₁.h + H₂.h)) → Gate ([ H₁.a , H₂.a ] (splitAt H₁.h e)) l+l e with splitAt H₁.h e ... | inj₁ e₁ = H₁.l e₁ ... | inj₂ e₂ = H₂.l e₂ @@ -421,17 +363,15 @@ together-resp-same {n} {H₁} {H₁′} {m} {H₂} {H₂′} ≡H₁ ≡H₂ = r ([ ≡H₁.a′ ∘ ≡H₁.to , ≡H₂.a′ ∘ ≡H₂.to ] ∘ splitAt ≡H₁.h) e ≡⟨ [,]-map (splitAt ≡H₁.h e) ⟨ ([ ≡H₁.a′ , ≡H₂.a′ ] ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ≡⟨ (cong [ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt-join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ⟨ ([ ≡H₁.a′ , ≡H₂.a′ ] ∘ splitAt ≡H₁.h′ ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h) e ∎ - ≗arity : H₁+H₂.arity ≗ H₁+H₂′.arity ∘ join ≡H₁.h′ ≡H₂.h′ ∘ map ≡H₁.to ≡H₂.to ∘ splitAt ≡H₁.h - ≗arity = cong ℕ.suc ∘ ≗a ≗j : (e : Fin H₁+H₂.h) - (i : Fin (H₁+H₂.arity e)) + (i : Fin (H₁+H₂.a e)) → H₁+H₂.j e i - ≡ H₁+H₂′.j (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e) (cast (≗arity e) i) + ≡ H₁+H₂′.j (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e) (cast (≗a e) i) ≗j e i with splitAt ≡H₁.h e ... | inj₁ e₁ rewrite splitAt-↑ˡ ≡H₁.h′ (≡H₁.to e₁) ≡H₂.h′ = cong (_↑ˡ m) (≡H₁.≗j e₁ i) ... | inj₂ e₂ rewrite splitAt-↑ʳ ≡H₁.h′ ≡H₂.h′ (≡H₂.to e₂) = cong (n ↑ʳ_) (≡H₂.≗j e₂ i) - ≗l : (e : Fin H₁+H₂.h) → l+l H₁ H₂ e ≡ cast-gate (sym (≗arity e)) (l+l H₁′ H₂′ (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e)) - ≗l e with splitAt ≡H₁.h e | .{≗arity e} + ≗l : (e : Fin H₁+H₂.h) → l+l H₁ H₂ e ≡ cast-gate (sym (≗a e)) (l+l H₁′ H₂′ (to (+-resp-↔ ≡H₁.↔h ≡H₂.↔h) e)) + ≗l e with splitAt ≡H₁.h e | .{≗a e} ... | inj₁ e₁ rewrite splitAt-↑ˡ ≡H₁.h′ (≡H₁.to e₁) ≡H₂.h′ = ≡H₁.≗l e₁ ... | inj₂ e₂ rewrite splitAt-↑ʳ ≡H₁.h′ ≡H₂.h′ (≡H₂.to e₂) = ≡H₂.≗l e₂ @@ -455,7 +395,7 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record open Hypergraph open ≡-Reasoning ≗j : (e : Fin (H₁.h + H₂.h)) - (i : Fin ((ℕ.suc ∘ [ H₁.a , H₂.a ] ∘ splitAt H₁.h) e)) + (i : Fin (([ H₁.a , H₂.a ] ∘ splitAt H₁.h) e)) → j (together (map-nodes f H₁) (map-nodes g H₂)) e i ≡ j (map-nodes ([ (_↑ˡ m′) ∘ f , (n′ ↑ʳ_) ∘ g ] ∘ splitAt n) (together H₁ H₂)) (≡H₁+H₂.to e) (cast refl i) ≗j e i rewrite (cast-is-id refl i) with splitAt H₁.h e @@ -475,7 +415,7 @@ commute {n} {n′} {m} {m′} {H₁} {H₂} f g = record ; sym-commute = λ { (f , g) {H₁ , H₂} → Hypergraph-same-sym (commute {H₁ = H₁} {H₂ = H₂} f g) } } where - η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m)) + η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m) η = record { to = λ { (H₁ , H₂) → together H₁ H₂ } ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } @@ -545,9 +485,9 @@ associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record ≡⟨ cong ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h) ([-,]-cong ([,]-∘ [ _↑ˡ H₂.h + H₃.h , H₁.h ↑ʳ_ ] ∘ splitAt H₁.h) (splitAt (H₁.h + H₂.h) x)) ⟩ ([ H₁.a , [ H₂.a , H₃.a ] ∘ splitAt H₂.h ] ∘ splitAt H₁.h ∘ [ [ _↑ˡ H₂.h + H₃.h , (H₁.h ↑ʳ_) ∘ (_↑ˡ H₃.h) ] ∘ splitAt H₁.h , (H₁.h ↑ʳ_) ∘ (H₂.h ↑ʳ_) ] ∘ splitAt (H₁.h + H₂.h)) x ∎ ≗j : (e : Fin (H₁.h + H₂.h + H₃.h)) - (i : Fin (ℕ.suc ([ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] (splitAt (H₁.h + H₂.h) e)))) + (i : Fin ([ [ H₁.a , H₂.a ] ∘ splitAt H₁.h , H₃.a ] (splitAt (H₁.h + H₂.h) e))) → Inverse.to (+-assoc-↔ X Y Z) (j+j (together H₁ H₂) H₃ e i) - ≡ j+j H₁ (together H₂ H₃) (Inverse.to ↔h e) (cast (cong ℕ.suc (≗a e)) i) + ≡ j+j H₁ (together H₂ H₃) (Inverse.to ↔h e) (cast (≗a e) i) ≗j e i with splitAt (H₁.h + H₂.h) e ≗j e i | inj₁ e₁₂ with splitAt H₁.h e₁₂ ≗j e i | inj₁ e₁₂ | inj₁ e₁ @@ -555,7 +495,6 @@ associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record rewrite splitAt-↑ˡ (X + Y) (H₁.j e₁ i ↑ˡ Y) Z rewrite splitAt-↑ˡ X (H₁.j e₁ i) Y = cong ((_↑ˡ Y + Z) ∘ H₁.j e₁) (sym (cast-is-id refl i)) ≗j e i | inj₁ e₁₂ | inj₂ e₂ - rewrite splitAt-↑ʳ H₁.h H₂.h e₂ rewrite splitAt-↑ʳ H₁.h (H₂.h + H₃.h) (e₂ ↑ˡ H₃.h) rewrite splitAt-↑ˡ H₂.h e₂ H₃.h rewrite splitAt-↑ˡ (X + Y) (X ↑ʳ H₂.j e₂ i) Z @@ -566,7 +505,7 @@ associativity {X} {Y} {Z} {H₁} {H₂} {H₃} = record rewrite splitAt-↑ʳ (X + Y) Z (H₃.j e₃ i) = cong ((X ↑ʳ_) ∘ (Y ↑ʳ_) ∘ H₃.j e₃) (sym (cast-is-id refl i)) ≗l : (e : Fin (H₁.h + H₂.h + H₃.h)) → l (map-nodes (Inverse.to (+-assoc-↔ X Y Z)) (together (together H₁ H₂) H₃)) e - ≡ cast-gate (sym (cong ℕ.suc (≗a e))) (l (together H₁ (together H₂ H₃)) (Inverse.to ↔h e)) + ≡ cast-gate (sym (≗a e)) (l (together H₁ (together H₂ H₃)) (Inverse.to ↔h e)) ≗l e with splitAt (H₁.h + H₂.h) e ≗l e | inj₁ e₁₂ with splitAt H₁.h e₁₂ ≗l e | inj₁ e₁₂ | inj₁ e₁ @@ -596,7 +535,7 @@ n+0↔n n = record to∘from : (x : Fin n) → to (from x) ≡ x to∘from x rewrite splitAt-↑ˡ n x 0 = refl -unitaryʳ : Hypergraph-same (map-nodes ([ (λ x → x) , (λ ()) ] ∘ splitAt n) (together H empty-hypergraph)) H +unitaryʳ : Hypergraph-same (map-nodes ([ id , (λ ()) ] ∘ splitAt n) (together H (discrete {0}))) H unitaryʳ {n} {H} = record { ↔h = h+0↔h ; ≗a = ≗a @@ -605,34 +544,34 @@ unitaryʳ {n} {H} = record } where module H = Hypergraph H - module H+0 = Hypergraph (together H empty-hypergraph) + module H+0 = Hypergraph (together H (discrete {0})) h+0↔h : Fin H+0.h ↔ Fin H.h h+0↔h = n+0↔n H.h ≗a : (e : Fin (H.h + 0)) → [ H.a , (λ ()) ] (splitAt H.h e) ≡ H.a (Inverse.to h+0↔h e) ≗a e with inj₁ e₁ ← splitAt H.h e in eq = refl ≗j : (e : Fin (H.h + 0)) - (i : Fin (ℕ.suc ([ H.a , (λ ()) ] (splitAt H.h e)))) - → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H empty-hypergraph e i)) - ≡ H.j (Inverse.to h+0↔h e) (cast (cong ℕ.suc (≗a e)) i) - ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H empty-hypergraph e) refl (≗a e) i + (i : Fin ([ H.a , (λ ()) ] (splitAt H.h e))) + → [ (λ x → x) , (λ ()) ] (splitAt n (j+j H discrete e i)) + ≡ H.j (Inverse.to h+0↔h e) (cast (≗a e) i) + ≗j e i = ≗j-aux (splitAt H.h e) refl (j+j H discrete e) refl (≗a e) i where ≗j-aux : (w : Fin H.h ⊎ Fin 0) → (eq₁ : splitAt H.h e ≡ w) - → (w₁ : Fin (ℕ.suc ([ H.a , (λ ()) ] w)) → Fin (n + 0)) - → j+j H empty-hypergraph e ≡ subst (λ hole → Fin (ℕ.suc ([ H.a , (λ ()) ] hole)) → Fin (n + 0)) (sym eq₁) w₁ + → (w₁ : Fin ([ H.a , (λ ()) ] w) → Fin (n + 0)) + → j+j H discrete e ≡ subst (λ hole → Fin ([ H.a , (λ ()) ] hole) → Fin (n + 0)) (sym eq₁) w₁ → (w₂ : [ H.a , (λ ()) ] w ≡ H.a (Inverse.to h+0↔h e)) - (i : Fin (ℕ.suc ([ H.a , (λ ()) ] w))) + (i : Fin ([ H.a , (λ ()) ] w)) → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i)) - ≡ H.j (Inverse.to h+0↔h e) (cast (cong ℕ.suc w₂) i) + ≡ H.j (Inverse.to h+0↔h e) (cast w₂ i) ≗j-aux (inj₁ e₁) eq w₁ eq₁ w₂ i with (inj₁ x) ← splitAt n (w₁ i) in eq₂ rewrite eq = trans (↑ˡ-injective 0 x (H.j e₁ i) (trans (splitAt⁻¹-↑ˡ eq₂) (sym (cong-app eq₁ i)))) (cong (H.j e₁) (sym (cast-is-id refl i))) ≗l : (e : Fin (H.h + 0)) - → l+l H empty-hypergraph e - ≡ cast-gate (sym (cong ℕ.suc (≗a e))) (H.l (Inverse.to h+0↔h e)) + → l+l H discrete e + ≡ cast-gate (sym (≗a e)) (H.l (Inverse.to h+0↔h e)) ≗l e with splitAt H.h e | {(≗a e)} ... | inj₁ e₁ = sym (cast-gate-is-id refl (H.l e₁)) @@ -686,9 +625,9 @@ braiding {n} {m} {H₁} {H₂} = record [ H₂.a , H₁.a ] (swap (splitAt H₁.h e)) ≡⟨ cong [ H₂.a , H₁.a ] (splitAt-join H₂.h H₁.h (swap (splitAt H₁.h e))) ⟨ [ H₂.a , H₁.a ] (splitAt H₂.h (join H₂.h H₁.h (swap (splitAt H₁.h e)))) ∎ ≗j : (e : Fin (Hypergraph.h (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)))) - (i : Fin (Hypergraph.arity (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e)) + (i : Fin (Hypergraph.a (map-nodes ([ m ↑ʳ_ , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e)) → Hypergraph.j (map-nodes ([ _↑ʳ_ m , _↑ˡ n ] ∘ splitAt n) (together H₁ H₂)) e i - ≡ Hypergraph.j (together H₂ H₁) (Inverse.to (+-comm-↔ H₁.h H₂.h) e) (cast (cong ℕ.suc (≗a e)) i) + ≡ Hypergraph.j (together H₂ H₁) (Inverse.to (+-comm-↔ H₁.h H₂.h) e) (cast (≗a e) i) ≗j e i with splitAt H₁.h e ≗j e i | inj₁ e₁ rewrite splitAt-↑ˡ n (H₁.j e₁ i) m @@ -698,47 +637,48 @@ braiding {n} {m} {H₁} {H₂} = record rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = cong ((_↑ˡ n) ∘ H₂.j e₂) (sym (cast-is-id refl i)) ≗l : (e : Fin (H₁.h + H₂.h)) → l+l H₁ H₂ e - ≡ cast-gate (sym (cong ℕ.suc (≗a e))) (l+l H₂ H₁ (Inverse.to (+-comm-↔ H₁.h H₂.h) e)) + ≡ cast-gate (sym (≗a e)) (l+l H₂ H₁ (Inverse.to (+-comm-↔ H₁.h H₂.h) e)) ≗l e with splitAt H₁.h e | .{≗a e} ≗l e | inj₁ e₁ rewrite splitAt-↑ʳ H₂.h H₁.h e₁ = sym (cast-gate-is-id refl (H₁.l e₁)) ≗l e | inj₂ e₂ rewrite splitAt-↑ˡ H₂.h e₂ H₁.h = sym (cast-gate-is-id refl (H₂.l e₂)) -hypergraph : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) -hypergraph = record - { F = F - ; isBraidedMonoidal = record - { isMonoidal = record - { ε = ε - ; ⊗-homo = ntHelper record - { η = λ { (m , n) → η } - ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g } - } - ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} } - ; unitaryˡ = Hypergraph-same-refl - ; unitaryʳ = unitaryʳ - } - ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} } - } - } - where - η : Func (×-setoid (Hypergraph-setoid n) (Hypergraph-setoid m)) (Hypergraph-setoid (n + m)) - η = record - { to = λ { (H₁ , H₂) → together H₁ H₂ } - ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } - } - -module F = SymmetricMonoidalFunctor hypergraph - -and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) (F.₀ 3) -and-gate = record - { to = λ { (lift tt) → and-graph } - ; cong = λ { (lift tt) → Hypergraph-same-refl } - } +opaque + unfolding ×-symmetric′ + Circ : SymmetricMonoidalFunctor Nat,+,0 Setoids-× + Circ = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ntHelper record + { η = λ { (m , n) → η } + ; commute = λ { (f , g) {H₁ , H₂} → commute {H₁ = H₁} {H₂ = H₂} f g } + } + ; associativity = λ { {X} {Y} {Z} {(H₁ , H₂) , H₃} → associativity {X} {Y} {Z} {H₁} {H₂} {H₃} } + ; unitaryˡ = Hypergraph-same-refl + ; unitaryʳ = unitaryʳ + } + ; braiding-compat = λ { {X} {Y} {H₁ , H₂} → braiding {X} {Y} {H₁} {H₂} } + } + } + where + η : Hypergraph-setoid n ×ₛ Hypergraph-setoid m ⟶ₛ Hypergraph-setoid (n + m) + η = record + { to = λ { (H₁ , H₂) → together H₁ H₂ } + ; cong = λ { (≡H₁ , ≡H₂) → together-resp-same ≡H₁ ≡H₂ } + } + +module F = SymmetricMonoidalFunctor Circ + +open Gate + +and-gate : ⊤ₛ ⟶ₛ Hypergraph-setoid 3 +and-gate = Const ⊤ₛ (Hypergraph-setoid 3) and-graph where and-graph : Hypergraph 3 and-graph = record { h = 1 - ; a = λ { 0F → 2 } + ; a = λ { 0F → 3 } ; j = λ { 0F → edge-0-nodes } ; l = λ { 0F → AND } } diff --git a/DecorationFunctor/Trivial.agda b/DecorationFunctor/Trivial.agda index 3b88010..6278d05 100644 --- a/DecorationFunctor/Trivial.agda +++ b/DecorationFunctor/Trivial.agda @@ -2,85 +2,70 @@ module DecorationFunctor.Trivial where -import Categories.Morphism as Morphism +open import Level using (0ℓ) open import Categories.Category.BinaryProducts using (module BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) -open import Categories.Category.Core using (Category) -open import Categories.Category.Instance.Nat using (Nat-Cocartesian) open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) -open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian) open import Categories.Category.Product using (_⁂_) -open import Categories.Functor using () renaming (_∘F_ to _∘_) -open import Categories.Functor.Core using (Functor) +open import Categories.Functor using (Functor) renaming (_∘F_ to _∘_) open import Categories.Functor.Monoidal.Symmetric using (module Lax) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.Setoids.SymmetricMonoidal using (Setoids-×) open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomplete) -open import Data.Nat using (ℕ) -open import Data.Product.Base using (_,_) +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×; ×-symmetric′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid.Unit {0ℓ} {0ℓ} using (⊤ₛ) open import Data.Unit using (tt) -open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-setoid) -open import Function.Base using (const) -open import Function.Bundles using (Func) -open import Level using (0ℓ; suc; lift) -open import Relation.Binary.Bundles using (Setoid) +open import Data.Unit.Properties using () renaming (≡-setoid to ⊤-≡ₛ) +open import Function using (Func; const) +open import Function.Construct.Constant using () renaming (function to Const) open import Relation.Binary.PropositionalEquality.Core using (refl) open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) -open Cocartesian Nat-Cocartesian using (coproducts) +open BinaryProducts products using (-×-) open FinitelyCocompleteCategory Nat-FinitelyCocomplete - using () - renaming (symmetricMonoidalCategory to Nat-smc) -open Morphism (Setoids 0ℓ 0ℓ) using (_≅_) + using (-+-) + renaming (symmetricMonoidalCategory to Nat-smc) open Lax using (SymmetricMonoidalFunctor) -open BinaryProducts products using (-×-) -open BinaryCoproducts coproducts using (-+-) - - F : Functor Nat (Setoids 0ℓ 0ℓ) F = record - { F₀ = const (⊤-setoid) - ; F₁ = const (record { to = const tt ; cong = const refl }) + { F₀ = const ⊤-≡ₛ + ; F₁ = const (Const ⊤-≡ₛ ⊤-≡ₛ tt) ; identity = refl ; homomorphism = refl ; F-resp-≈ = const refl } -ε : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid -ε = record - { to = const tt - ; cong = const refl - } +ε : Func ⊤ₛ ⊤-≡ₛ +ε = Const ⊤ₛ ⊤-≡ₛ tt ⊗-homomorphism : NaturalTransformation (-×- ∘ (F ⁂ F)) (F ∘ -+-) ⊗-homomorphism = ntHelper record - { η = const (record { to = const tt ; cong = const refl }) + { η = const (Const (⊤-≡ₛ ×ₛ ⊤-≡ₛ) ⊤-≡ₛ tt) ; commute = const refl } -trivial : SymmetricMonoidalFunctor Nat-smc (Setoids-× {0ℓ}) -trivial = record - { F = F - ; isBraidedMonoidal = record - { isMonoidal = record - { ε = ε - ; ⊗-homo = ⊗-homomorphism - ; associativity = refl - ; unitaryˡ = refl - ; unitaryʳ = refl - } - ; braiding-compat = refl - } - } +opaque + unfolding ×-symmetric′ -and-gate : Func (SingletonSetoid {0ℓ} {0ℓ}) ⊤-setoid -and-gate = record - { to = const tt - ; cong = const refl - } + trivial : SymmetricMonoidalFunctor Nat-smc Setoids-× + trivial = record + { F = F + ; isBraidedMonoidal = record + { isMonoidal = record + { ε = ε + ; ⊗-homo = ⊗-homomorphism + ; associativity = refl + ; unitaryˡ = refl + ; unitaryʳ = refl + } + ; braiding-compat = refl + } + } + +and-gate : Func ⊤ₛ ⊤-≡ₛ +and-gate = Const ⊤ₛ ⊤-≡ₛ tt |