From d91f74bce9a8eb1dd38f74de5fae597bde54df5a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Fri, 18 Jul 2025 17:45:53 -0500
Subject: Add Hypergraph setoid

---
 Data/Hypergraph/Edge.agda | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Data/Hypergraph/Edge.agda')

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
-- 
cgit v1.2.3