aboutsummaryrefslogtreecommitdiff
path: root/Data/Hypergraph.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Data/Hypergraph.agda')
-rw-r--r--Data/Hypergraph.agda6
1 files changed, 5 insertions, 1 deletions
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index 7d22129..532e082 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -79,4 +79,8 @@ Multiset∘Edgeₛ = ↭-setoid ∘ Edgeₛ
mkHypergraphₛ : {n : ℕ} → Multiset∘Edgeₛ n ⟶ₛ Hypergraphₛ n
mkHypergraphₛ .to = mkHypergraph
-mkHypergraphₛ {n} .cong = mk≈
+mkHypergraphₛ .cong = mk≈
+
+edgesₛ : {n : ℕ} → Hypergraphₛ n ⟶ₛ Multiset∘Edgeₛ n
+edgesₛ .to = Hypergraph.edges
+edgesₛ .cong = _≈_.↭-edges