From 6272b4e84650b9833a53239b354770e0deba7b9a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 9 Dec 2025 13:25:39 -0600 Subject: Add shorter name for singleton setoid --- DecorationFunctor/Hypergraph/Labeled.agda | 111 +++++++++++++----------------- 1 file changed, 47 insertions(+), 64 deletions(-) (limited to 'DecorationFunctor/Hypergraph') diff --git a/DecorationFunctor/Hypergraph/Labeled.agda b/DecorationFunctor/Hypergraph/Labeled.agda index 33a7a89..31402b1 100644 --- a/DecorationFunctor/Hypergraph/Labeled.agda +++ b/DecorationFunctor/Hypergraph/Labeled.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; 0ℓ; lift) +open import Level using (Level) module DecorationFunctor.Hypergraph.Labeled {c ℓ : Level} where @@ -8,28 +8,20 @@ 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 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.Permutation using (lift₀) open import Data.Fin.Properties using ( splitAt-join ; join-splitAt @@ -40,33 +32,29 @@ 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 (_×ₛ_) +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.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 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 {c} {ℓ}) 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 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) open import Data.Circuit.Gate using (Gate; cast-gate; cast-gate-trans; cast-gate-is-id; subst-is-cast-gate) @@ -260,19 +248,16 @@ F = record -- monoidal structure -empty-hypergraph : Hypergraph 0 -empty-hypergraph = record +discrete : {n : ℕ} → Hypergraph n +discrete = record { h = 0 ; a = λ () ; j = λ () ; l = λ () } -ε : SingletonSetoid {c} {ℓ} ⟶ₛ 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 @@ -510,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 @@ -551,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 ([ id , (λ ()) ] ∘ 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 @@ -560,22 +544,22 @@ 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 ([ 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 (≗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 ([ H.a , (λ ()) ] w) → Fin (n + 0)) - → j+j H empty-hypergraph e ≡ subst (λ hole → Fin ([ H.a , (λ ()) ] hole) → Fin (n + 0)) (sym eq₁) w₁ + → 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 ([ H.a , (λ ()) ] w)) → [ (λ x → x) , (λ ()) ] (splitAt n (w₁ i)) @@ -586,7 +570,7 @@ unitaryʳ {n} {H} = record (↑ˡ-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 + → 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₁)) @@ -658,39 +642,38 @@ braiding {n} {m} {H₁} {H₂} = record ≗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₂)) -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₂ } - } +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 : SingletonSetoid {c} {ℓ} ⟶ₛ F.₀ 3 -and-gate = record - { to = λ _ → and-graph - ; cong = λ _ → Hypergraph-same-refl - } +and-gate : ⊤ₛ ⟶ₛ Hypergraph-setoid 3 +and-gate = Const ⊤ₛ (Hypergraph-setoid 3) and-graph where and-graph : Hypergraph 3 and-graph = record -- cgit v1.2.3