diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-07-18 17:45:53 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-07-18 17:45:53 -0500 |
| commit | d91f74bce9a8eb1dd38f74de5fae597bde54df5a (patch) | |
| tree | a334149c6434dbce0b89097e26dfc929ffdef2c6 /Data/Hypergraph/Edge.agda | |
| parent | 2184a8f47f72a415e3387a9aaca042dd63c80fd9 (diff) | |
Add Hypergraph setoid
Diffstat (limited to 'Data/Hypergraph/Edge.agda')
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index 3c2a3a1..cbf61e6 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -324,3 +324,8 @@ showEdge : {v : ℕ} → Edge v → String showEdge record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public + +≈-Edge⇒≡ : {v : ℕ} {x y : Edge v} → ≈-Edge x y → x ≡ y +≈-Edge⇒≡ {v} {record { label = l ; ports = p }} record { ≡arity = ≡.refl ; ≡label = ≡.refl ; ≡ports = ≡.refl } + rewrite cast-is-id ≡.refl l + rewrite VecCast.cast-is-id ≡.refl p = ≡.refl |