aboutsummaryrefslogtreecommitdiff
path: root/DecorationFunctor/Hypergraph
diff options
context:
space:
mode:
Diffstat (limited to 'DecorationFunctor/Hypergraph')
-rw-r--r--DecorationFunctor/Hypergraph/Labeled.agda111
1 files changed, 47 insertions, 64 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 21:52:23 +0000