diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-05-01 11:14:50 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-05-01 11:14:50 -0500 |
| commit | 2fa014cfc9196de99f3997090aec8128ec703dcc (patch) | |
| tree | d73925a6215efa378d5747a68340d5c05a1a7ab2 /DecorationFunctor/Hypergraph.agda | |
| parent | 665f9c6c3a60025f4f6bdf00c71227b2fa7d95f5 (diff) | |
Add labeled hypergraph decoration functor
Diffstat (limited to 'DecorationFunctor/Hypergraph.agda')
| -rw-r--r-- | DecorationFunctor/Hypergraph.agda | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/DecorationFunctor/Hypergraph.agda b/DecorationFunctor/Hypergraph.agda index a4e08df..5cd83f3 100644 --- a/DecorationFunctor/Hypergraph.agda +++ b/DecorationFunctor/Hypergraph.agda @@ -26,7 +26,7 @@ open import Category.Instance.Nat.FinitelyCocomplete using (Nat-FinitelyCocomple 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.Patterns using (0F; 1F) +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 (ℕ; _+_) @@ -629,9 +629,11 @@ and-gate = record and-graph : Hypergraph 3 and-graph = record { h = 1 - ; a = λ { 0F → 3 } - ; j = λ { 0F 0F → # 0 - ; 0F 1F → # 1 - ; 0F 2F → # 2 - } + ; a = λ { 0F → 2 } + ; j = λ { 0F → edge-0-nodes } } + where + edge-0-nodes : Fin 3 → Fin 3 + edge-0-nodes 0F = # 0 + edge-0-nodes 1F = # 1 + edge-0-nodes 2F = # 2 |