diff options
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 |