Add Hypergraph setoid

3 files changed, 57 insertions, 2 deletions

diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index e43cbce..5cf5388 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -9,7 +9,7 @@ open import Data.List.Base using (List; map)
 open import Data.Nat.Base using (ℕ)
 open import Data.String using (String; unlines)
 
-import Data.List.Sort.MergeSort as MergeSort
+import Data.List.Sort as Sort
 
 record Hypergraph (v : ℕ) : Set where
   field
@@ -19,7 +19,7 @@ sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
 sortHypergraph {v} H = record { edges = sort edges }
   where
     open Hypergraph H
-    open MergeSort decTotalOrder using (sort)
+    open Sort decTotalOrder using (sort)
 
 showHypergraph : {v : ℕ} → Hypergraph v → String
 showHypergraph record { edges = e} = unlines (map showEdge e)
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
diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda
new file mode 100644
index 0000000..c39977d
--- /dev/null
+++ b/Data/Hypergraph/Setoid.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Setoid (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Edge HL using (decTotalOrder)
+open import Data.Hypergraph.Base HL using (Hypergraph; sortHypergraph)
+open import Data.Nat.Base using (ℕ)
+open import Level using (0ℓ)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+record ≈-Hypergraph {v : ℕ} (H H′ : Hypergraph v) : Set where
+  module H = Hypergraph H
+  module H′ = Hypergraph H′
+  field
+    ≡sorted : sortHypergraph H ≡ sortHypergraph H′
+  open Hypergraph using (edges)
+  ≡edges : edges (sortHypergraph H) ≡ edges (sortHypergraph H′)
+  ≡edges = ≡.cong edges ≡sorted
+  open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
+  open import Data.List.Sort decTotalOrder using (sort-↭)
+  ↭edges : H.edges ↭ H′.edges
+  ↭edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡edges) (sort-↭ H′.edges))
+
+≈-refl : {v : ℕ} {H : Hypergraph v} → ≈-Hypergraph H H
+≈-refl = record { ≡sorted = ≡.refl }
+
+≈-sym : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H
+≈-sym ≈H = record { ≡sorted = ≡.sym ≡sorted }
+  where
+    open ≈-Hypergraph ≈H 
+
+≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H″ → ≈-Hypergraph H H″
+≈-trans ≈H₁ ≈H₂ = record { ≡sorted = ≡.trans ≈H₁.≡sorted ≈H₂.≡sorted }
+  where
+    module ≈H₁ = ≈-Hypergraph ≈H₁
+    module ≈H₂ = ≈-Hypergraph ≈H₂
+
+Hypergraph-Setoid : (v : ℕ) → Setoid 0ℓ 0ℓ
+Hypergraph-Setoid v = record
+    { Carrier = Hypergraph v
+    ; _≈_ = ≈-Hypergraph
+    ; isEquivalence = record
+        { refl = ≈-refl
+        ; sym = ≈-sym
+        ; trans = ≈-trans
+        }
+    }