From 298baf2b69620106e95b52206e02d58ad8cb9fc8 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Mon, 3 Nov 2025 23:29:21 -0600
Subject: Use permutation for equivalence of hypergraphs

---
 Data/Circuit.agda               |  78 +++------
 Data/Circuit/Convert.agda       |  84 ++++-----
 Data/Hypergraph.agda            |  63 ++++++-
 Data/Hypergraph/Base.agda       |  25 ---
 Data/Hypergraph/Edge.agda       | 368 +++++++---------------------------------
 Data/Hypergraph/Edge/Order.agda | 280 ++++++++++++++++++++++++++++++
 Data/Hypergraph/Setoid.agda     |  59 -------
 Functor/Instance/Nat/Circ.agda  |   2 +-
 Functor/Instance/Nat/Edge.agda  |  11 +-
 9 files changed, 452 insertions(+), 518 deletions(-)
 delete mode 100644 Data/Hypergraph/Base.agda
 create mode 100644 Data/Hypergraph/Edge/Order.agda
 delete mode 100644 Data/Hypergraph/Setoid.agda

diff --git a/Data/Circuit.agda b/Data/Circuit.agda
index 09dfb2e..46c4e18 100644
--- a/Data/Circuit.agda
+++ b/Data/Circuit.agda
@@ -1,70 +1,38 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; _⊔_)
+open import Level using (Level)
 
 module Data.Circuit {c ℓ : Level} where
 
-import Data.List as List
-
 open import Data.Circuit.Gate using (Gates)
 
+import Data.List as List
+import Data.Hypergraph {c} {ℓ} Gates as Hypergraph
+
 open import Data.Fin using (Fin)
-open import Data.Hypergraph {c} {ℓ} Gates
-  using
-    ( Hypergraph
-    ; Hypergraphₛ
-    ; mkHypergraphₛ
-    ; List∘Edgeₛ
-    ; module Edge
-    ; mkHypergraph
-    ; _≈_
-    ; mk≈
-    )
 open import Data.Nat using (ℕ)
-open import Relation.Binary using (Setoid)
-open import Function.Bundles using (Func; _⟶ₛ_)
-
-open List using (List)
-open Edge using (Edge; ≈-Edge⇒≡)
-
-Circuit : ℕ → Set c
-Circuit = Hypergraph
-
-map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m
-map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges)
-
-Circuitₛ : ℕ → Setoid c (c ⊔ ℓ)
-Circuitₛ = Hypergraphₛ
-
-mkCircuitₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Circuitₛ n
-mkCircuitₛ = mkHypergraphₛ
+open import Function using (Func; _⟶ₛ_)
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺)
 
 open Func
-open Edge.Sort using (sort)
+open Hypergraph using (List∘Edgeₛ)
+open Hypergraph
+  using (_≈_ ; mk≈ ; module Edge)
+  renaming
+    ( Hypergraph to Circuit
+    ; Hypergraphₛ to Circuitₛ
+    ; mkHypergraph to mkCircuit
+    ; mkHypergraphₛ to mkCircuitₛ
+    )
+  public
+open List using ([])
 
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ′)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺)
-open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise; Pointwise-≡⇒≡)
-open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation)
+map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m
+map f (mkCircuit edges) = mkCircuit (List.map (Edge.map f) edges)
 
-import Data.Permutation.Sort as ↭-Sort
+discrete : (n : ℕ) → Circuit n
+discrete n = mkCircuit []
 
 mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m
-mapₛ {n} {m} f .to = map f
-mapₛ {n} {m} f .cong {mkHypergraph xs} {mkHypergraph ys} x≈y = mk≈ ≡-norm
-  where
-    open _≈_ x≈y using (↭-edges)
-    open ↭-Sort (Edge.decTotalOrder {m}) using (sorted-≋)
-    open import Function.Reasoning
-    xs′ ys′ : List (Edge m)
-    xs′ = List.map (Edge.map f) xs
-    ys′ = List.map (Edge.map f) ys
-    ≡-norm : mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′)
-    ≡-norm = ↭-edges                        ∶ xs ↭ ys
-        |> map⁺ (Edge.map f)                ∶ xs′ ↭ ys′
-        |> ↭⇒↭ₛ′ Edge.≈-Edge-IsEquivalence  ∶ Permutation Edge.≈-Edge xs′ ys′
-        |> sorted-≋                         ∶ Pointwise Edge.≈-Edge (sort xs′) (sort ys′)
-        |> PW.map ≈-Edge⇒≡                  ∶ Pointwise _≡_ (sort xs′) (sort ys′)
-        |> Pointwise-≡⇒≡                    ∶ sort xs′ ≡ sort ys′
-        |> ≡.cong mkHypergraph              ∶ mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′)
+mapₛ f .to = map f
+mapₛ f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edge.map f) x≈y)
diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda
index 8562e92..d5abd35 100644
--- a/Data/Circuit/Convert.agda
+++ b/Data/Circuit/Convert.agda
@@ -4,50 +4,53 @@ module Data.Circuit.Convert where
 
 open import Level using (0ℓ)
 
+import Data.Vec as Vec
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Data.List.Relation.Binary.Permutation.Propositional as L
+import Data.Vec.Functional.Relation.Binary.Permutation as V
+import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph
+
 open import Data.Nat.Base using (ℕ)
 open import Data.Circuit.Gate using (Gate; Gates; cast-gate; cast-gate-is-id; subst-is-cast-gate)
+open import Data.Circuit {0ℓ} {0ℓ} using (Circuit; Circuitₛ; _≈_; mkCircuit; module Edge; mk≈)
 open import Data.Fin.Base using (Fin)
-open import Data.Hypergraph.Edge Gates using (Edge)
-open import Data.Hypergraph.Base {0ℓ} Gates using (Hypergraph; normalize; mkHypergraph)
-open import Data.Hypergraph.Setoid {0ℓ} {0ℓ} Gates using (Hypergraphₛ; _≈_)
+open import Data.Product.Base using (_,_)
 open import Data.Permutation using (fromList-↭; toList-↭)
 open import Data.List using (length)
 open import Data.Vec.Functional using (toVec; fromVec; toList; fromList)
 open import Function.Bundles using (Equivalence; _↔_)
 open import Function.Base using (_∘_; id)
+open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast)
+open import Data.Fin.Base using () renaming (cast to fincast)
+open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id)
 open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation)
 open import Data.Product.Base using (proj₁; proj₂; _×_)
 open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
-import Function.Reasoning as →-Reasoning
-import Data.List.Relation.Binary.Permutation.Propositional as L
-import Data.Vec.Functional.Relation.Binary.Permutation as V
-import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph
-
 open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′)
 
-to : {v : ℕ} → Hypergraph v → Hypergraph′ v
-to H = record
+to : {v : ℕ} → Circuit v → Hypergraph′ v
+to C = record
     { h = length edges
     ; a = arity ∘ fromList edges
     ; j = fromVec ∘ ports ∘ fromList edges
     ; l = label ∘ fromList edges
     }
   where
-    open Edge using (arity; ports; label)
-    open Hypergraph H
+    open Edge.Edge using (arity; ports; label)
+    open Circuit C
 
-from : {v : ℕ} → Hypergraph′ v → Hypergraph v
+from : {v : ℕ} → Hypergraph′ v → Circuit v
 from {v} H = record
     { edges = toList asEdge
     }
   where
     open Hypergraph′ H
-    asEdge : Fin h → Edge v
+    asEdge : Fin h → Edge.Edge v
     asEdge e = record { label = l e ; ports = toVec (j e) }
 
-to-cong : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → Hypergraph-same (to H) (to H′)
+to-cong : {v : ℕ} {H H′ : Circuit v} → H ≈ H′ → Hypergraph-same (to H) (to H′)
 to-cong {v} {H} {H′} ≈H = record
     { ↔h = flip ρ
     ; ≗a = ≗a
@@ -55,7 +58,7 @@ to-cong {v} {H} {H′} ≈H = record
     ; ≗l = ≗l
     }
   where
-    open Edge using (arity; ports; label)
+    open Edge.Edge using (arity; ports; label)
     open _≈_ ≈H
     open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ)
     open import Data.Fin.Base using (cast)
@@ -92,11 +95,6 @@ to-cong {v} {H} {H′} ≈H = record
           ≡.refl
 
 module _ {v : ℕ} where
-  open import Data.Hypergraph.Edge Gates using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡)
-  open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭)
-  open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋)
-  open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map)
-  open import Data.Product.Base using (_,_)
   open import Data.Hypergraph.Label using (HypergraphLabel)
   open HypergraphLabel Gates using (isCastable)
   open import Data.Castable using (IsCastable)
@@ -105,15 +103,14 @@ module _ {v : ℕ} where
       : {H H′ : Hypergraph′ v}
       → Hypergraph-same H H′
       → from H ≈ from H′
-  from-cong {H} {H′} ≈H = record
-      { ≡-normalized = ≡-normalized
-      }
+  from-cong {H} {H′} ≈H = mk≈ (toList-↭ (flip ↔h , H∘ρ≗H′))
     where
+ 
       module H = Hypergraph′ H
       module H′ = Hypergraph′ H′
       open Hypergraph′
       open Hypergraph-same ≈H using (↔h; ≗a; ≗l; ≗j; inverseˡ) renaming (from to f; to to t)
-      asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge v
+      asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge.Edge v
       asEdge H e = record { label = l H e ; ports = toVec (j H e) }
 
       to-from : (e : Fin H′.h) → t (f e) ≡ e
@@ -134,13 +131,6 @@ module _ {v : ℕ} where
       ≗l′ : (e : Fin H′.h) → cast-gate (≗a′ e) (H.l (f e)) ≡ H′.l e
       ≗l′ e = ≈-trans {H.a _} (l≗ (f e)) (l∘to-from e)
 
-      import Data.Vec.Relation.Binary.Equality.Cast as VecCast
-      open import Data.Vec using (cast) renaming (map to vecmap)
-      open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast)
-
-      open import Data.Fin.Base using () renaming (cast to fincast)
-      open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id)
-
       j∘to-from
           : (e : Fin H′.h) (i : Fin (H′.a (t (f e))))
           → H′.j (t (f e)) i
@@ -161,40 +151,28 @@ module _ {v : ℕ} where
             {A : Set}
             (m≡n : m ≡ n)
             (f : Fin n → A)
-          → cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f
+          → Vec.cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f
       cast-toVec m≡n f rewrite m≡n = begin
-          cast _ (toVec (f ∘ (fincast _)))  ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩
+          Vec.cast _ (toVec (f ∘ (fincast _)))  ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩
           toVec (f ∘ fincast _)             ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩
-          vecmap f (toVec (fincast _))      ≡⟨ ≡.cong (vecmap f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩
-          vecmap f (toVec id)               ≡⟨ tabulate-∘ f id ⟨
+          Vec.map f (toVec (fincast _))     ≡⟨ ≡.cong (Vec.map f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩
+          Vec.map f (toVec id)              ≡⟨ tabulate-∘ f id ⟨
           toVec f                           ∎
 
-      ≗p′ : (e : Fin H′.h) → cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e)
+      ≗p′ : (e : Fin H′.h) → Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e)
       ≗p′ e = begin
-          cast (≗a′ e) (toVec (H.j (f e)))    ≡⟨ ≡.cong (cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩
-          cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩
+          Vec.cast (≗a′ e) (toVec (H.j (f e)))    ≡⟨ ≡.cong (Vec.cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩
+          Vec.cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩
           toVec (H′.j e)                      ∎
 
       H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e
-      H∘ρ≗H′ e = ≈-Edge⇒≡ record
+      H∘ρ≗H′ e = Edge.≈⇒≡ record
           { ≡arity = ≗a′ e
           ; ≡label = ≗l′ e
           ; ≡ports = ≗p′ e
           }
 
-      open Hypergraph using (edges)
-      open →-Reasoning
-      ≡-normalized : normalize (from H) ≡ normalize (from H′)
-      ≡-normalized =
-             flip ↔h , H∘ρ≗H′             ∶ asEdge H V.↭ asEdge H′
-          |> toList-↭                     ∶ toList (asEdge H) L.↭ toList (asEdge H′)
-          |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′))
-          |> sorted-≋                     ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′)))
-          |> map ≈-Edge⇒≡                 ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′)))
-          |> Pointwise-≡⇒≡                ∶ sort (edges (from H)) ≡ sort (edges (from H′))
-          |> ≡.cong mkHypergraph          ∶ normalize (from H) ≡ normalize (from H′)
-
-equiv : (v : ℕ) → Equivalence (Hypergraphₛ v) (Hypergraph-Setoid′ v)
+equiv : (v : ℕ) → Equivalence (Circuitₛ v) (Hypergraph-Setoid′ v)
 equiv v = record
     { to = to
     ; from = from
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index 18a259b..ff92d0e 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -1,26 +1,71 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level)
-
+open import Level using (Level; 0ℓ)
 open import Data.Hypergraph.Label using (HypergraphLabel)
 
 module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
 
 import Data.List.Relation.Binary.Pointwise as PW
-import Data.Hypergraph.Edge HL as HypergraphEdge
 import Function.Reasoning as →-Reasoning
 import Relation.Binary.PropositionalEquality as ≡
+import Data.Hypergraph.Edge HL as Hyperedge
+import Data.List.Relation.Binary.Permutation.Propositional as List-↭
 
-open import Data.Hypergraph.Base {c} HL public
-open import Data.Hypergraph.Setoid {c} {ℓ} HL public
+open import Data.List using (List; map)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-refl; ↭-sym; ↭-trans)
 open import Data.Nat using (ℕ)
+open import Data.String using (String; unlines)
 open import Function using (_∘_; _⟶ₛ_; Func)
-open import Level using (0ℓ)
 open import Relation.Binary using (Setoid)
 
-module Edge = HypergraphEdge
+module Edge = Hyperedge
+open Edge using (Edge; Edgeₛ)
+
+-- A hypergraph is a list of edges
+record Hypergraph (v : ℕ) : Set c where
+  constructor mkHypergraph
+  field
+    edges : List (Edge v)
+
+module _ {v : ℕ} where
+
+  show : Hypergraph v → String
+  show (mkHypergraph e) = unlines (map Edge.show e)
+
+  -- an equivalence relation on hypergraphs
+  record _≈_ (H H′ : Hypergraph v) : Set ℓ where
+
+    constructor mk≈
+
+    module H = Hypergraph H
+    module H′ = Hypergraph H′
+
+    field
+      ↭-edges : H.edges ↭ H′.edges
+
+  infixr 4 _≈_
+
+  ≈-refl : {H : Hypergraph v} → H ≈ H
+  ≈-refl = mk≈ ↭-refl
+
+  ≈-sym : {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H
+  ≈-sym (mk≈ ≡n) = mk≈ (↭-sym ≡n)
+
+  ≈-trans : {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″
+  ≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (↭-trans ≡n₁ ≡n₂)
+
+-- The setoid of labeled hypergraphs with v nodes
+Hypergraphₛ : ℕ → Setoid c ℓ
+Hypergraphₛ v = record
+    { Carrier = Hypergraph v
+    ; _≈_ = _≈_
+    ; isEquivalence = record
+        { refl = ≈-refl
+        ; sym = ≈-sym
+        ; trans = ≈-trans
+        }
+    }
 
-open Edge using (Edgeₛ; ≈-Edge⇒≡)
 open Func
 
 List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ
@@ -29,7 +74,7 @@ List∘Edgeₛ = PW.setoid ∘ Edgeₛ
 mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n
 mkHypergraphₛ .to = mkHypergraph
 mkHypergraphₛ {n} .cong ≋-edges = ≋-edges
-    |> PW.map ≈-Edge⇒≡
+    |> PW.map Edge.≈⇒≡
     |> PW.Pointwise-≡⇒≡
     |> ≡.cong mkHypergraph
     |> Setoid.reflexive (Hypergraphₛ n)
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
deleted file mode 100644
index 0910e02..0000000
--- a/Data/Hypergraph/Base.agda
+++ /dev/null
@@ -1,25 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level)
-open import Data.Hypergraph.Label using (HypergraphLabel)
-
-module Data.Hypergraph.Base {ℓ : Level} (HL : HypergraphLabel) where
-
-import Data.Hypergraph.Edge HL as Edge
-
-open import Data.List using (List; map)
-open import Data.Nat.Base using (ℕ)
-open import Data.String using (String; unlines)
-
-open Edge using (Edge)
-
-record Hypergraph (v : ℕ) : Set ℓ where
-  constructor mkHypergraph
-  field
-    edges : List (Edge v)
-
-normalize : {v : ℕ} → Hypergraph v → Hypergraph v
-normalize (mkHypergraph e) = mkHypergraph (Edge.sort e)
-
-show : {v : ℕ} → Hypergraph v → String
-show (mkHypergraph e) = unlines (map Edge.show e)
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index ee32393..1e24559 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -4,43 +4,32 @@ open import Data.Hypergraph.Label using (HypergraphLabel)
 
 module Data.Hypergraph.Edge (HL : HypergraphLabel) where
 
-import Data.List.Sort as ListSort
-import Data.Fin as Fin
-import Data.Fin.Properties as FinProp
 import Data.Vec as Vec
 import Data.Vec.Relation.Binary.Equality.Cast as VecCast
-import Data.Vec.Relation.Binary.Lex.Strict as Lex
 import Relation.Binary.PropositionalEquality as ≡
-import Relation.Binary.Properties.DecTotalOrder as DTOP
-import Relation.Binary.Properties.StrictTotalOrder as STOP
 
-open import Relation.Binary using (Rel; IsStrictTotalOrder; Tri; Trichotomous; _Respects_)
-open import Data.Castable using (IsCastable)
 open import Data.Fin using (Fin)
 open import Data.Fin.Show using () renaming (show to showFin)
-open import Data.Nat using (ℕ; _<_)
-open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
-open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Nat using (ℕ)
 open import Data.String using (String; _<+>_)
-open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
 open import Data.Vec.Show using () renaming (show to showVec)
 open import Level using (0ℓ)
-open import Relation.Binary using (Setoid; DecTotalOrder; StrictTotalOrder; IsEquivalence)
-open import Relation.Nullary using (¬_)
-
+open import Relation.Binary using (Setoid; IsEquivalence)
 
 module HL = HypergraphLabel HL
+
 open HL using (Label; cast; cast-is-id)
 open Vec using (Vec)
 
 record Edge (v : ℕ) : Set where
+  constructor mkEdge
   field
     {arity} : ℕ
     label : Label arity
     ports : Vec (Fin v) arity
 
 map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m
-map {n} {m} f edge = record
+map f edge = record
     { label = label
     ; ports = Vec.map f ports
     }
@@ -50,299 +39,58 @@ map {n} {m} f edge = record
 open ≡ using (_≡_)
 open VecCast using (_≈[_]_)
 
-record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
-  module E = Edge E
-  module E′ = Edge E′
-  field
-    ≡arity : E.arity ≡ E′.arity
-    ≡label : cast ≡arity E.label ≡ E′.label
-    ≡ports : E.ports ≈[ ≡arity ] E′.ports
-
-≈-Edge-refl : {v : ℕ} {x : Edge v} → ≈-Edge x x
-≈-Edge-refl {_} {x} = record
-    { ≡arity = ≡.refl
-    ; ≡label = HL.≈-reflexive ≡.refl
-    ; ≡ports = VecCast.≈-reflexive ≡.refl
-    }
-  where
-    open Edge x using (arity; label)
-    open DecTotalOrder (HL.decTotalOrder arity) using (module Eq)
-
-≈-Edge-sym : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ≈-Edge y x
-≈-Edge-sym {_} {x} {y} x≈y = record
-    { ≡arity = ≡.sym ≡arity
-    ; ≡label = HL.≈-sym ≡label
-    ; ≡ports = VecCast.≈-sym ≡ports
-    }
-  where
-    open ≈-Edge x≈y
-    open DecTotalOrder (HL.decTotalOrder E.arity) using (module Eq)
-
-≈-Edge-trans : {v : ℕ} {i j k : Edge v} → ≈-Edge i j → ≈-Edge j k → ≈-Edge i k
-≈-Edge-trans {_} {i} {j} {k} i≈j j≈k = record
-    { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity
-    ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label
-    ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports
-    }
-  where
-    module i≈j = ≈-Edge i≈j
-    module j≈k = ≈-Edge j≈k
-
-≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v})
-≈-Edge-IsEquivalence = record
-    { refl = ≈-Edge-refl
-    ; sym = ≈-Edge-sym
-    ; trans = ≈-Edge-trans
-    }
-
-open HL using (_[_<_])
-_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ
-_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v})
-data <-Edge {v : ℕ} : Edge v → Edge v → Set where
-  <-arity
-      : {x y : Edge v}
-      → Edge.arity x < Edge.arity y
-      → <-Edge x y
-  <-label
-      : {x y : Edge v}
-        (≡a : Edge.arity x ≡ Edge.arity y)
-      → Edge.arity y [ cast ≡a (Edge.label x) < Edge.label y ]
-      → <-Edge x y
-  <-ports
-      : {x y : Edge v}
-        (≡a : Edge.arity x ≡ Edge.arity y)
-        (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y)
-      → Vec.cast ≡a (Edge.ports x) << Edge.ports y
-      → <-Edge x y
-
-<-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y
-<-Edge-irrefl record { ≡arity = ≡a } (<-arity n<m) = <-irrefl ≡a n<m
-<-Edge-irrefl record { ≡label = ≡l } (<-label _ (_ , x≉y)) = x≉y ≡l
-<-Edge-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y)
-    = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y
-
-<-Edge-trans : {v : ℕ} {i j k : Edge v} → <-Edge i j → <-Edge j k → <-Edge i k
-<-Edge-trans (<-arity i<j) (<-arity j<k) = <-arity (<-trans i<j j<k)
-<-Edge-trans (<-arity i<j) (<-label ≡.refl j<k) = <-arity i<j
-<-Edge-trans (<-arity i<j) (<-ports ≡.refl _ j<k) = <-arity i<j
-<-Edge-trans (<-label ≡.refl i<j) (<-arity j<k) = <-arity j<k
-<-Edge-trans {_} {i} (<-label ≡.refl i<j) (<-label ≡.refl j<k)
-    = <-label ≡.refl (<-label-trans i<j (<-respˡ-≈ (HL.≈-reflexive ≡.refl) j<k))
-  where
-    open DTOP (HL.decTotalOrder (Edge.arity i)) using (<-respˡ-≈) renaming (<-trans to <-label-trans)
-<-Edge-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _)
-    = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j)
-  where
-    open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈)
-<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k
-<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k)
-    = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k)
-  where
-    open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈)
-<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k)
-  rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j))
-    = <-ports ≡.refl
-        (HL.≈-trans ≡l₁ ≡l₂)
-        (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k)
-  where
-    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
-
-<-Edge-respˡ-≈ : {v : ℕ} {y : Edge v} → (λ x → <-Edge x y) Respects ≈-Edge
-<-Edge-respˡ-≈ ≈x (<-arity x₁<y) = <-arity (proj₂ <-resp₂-≡ ≡arity x₁<y)
-  where
-    open ≈-Edge ≈x using (≡arity)
-<-Edge-respˡ-≈ {_} {y} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x₁<y)
-    = <-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x₁<y)
-  where
-    module y = Edge y
-    open DTOP (HL.decTotalOrder y.arity) using (<-respˡ-≈)
-<-Edge-respˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y)
-    = <-ports
-        ≡.refl
-        (≡.cong (cast _) (HL.≈-reflexive ≡.refl))
-        (Lex.<-respectsˡ
-            ≡-isPartialEquivalence
-            FinProp.<-respˡ-≡
-            (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
-            x₁<y)
-  where
-    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
-
-<-Edge-respʳ-≈ : {v : ℕ} {x : Edge v} → <-Edge x Respects ≈-Edge
-<-Edge-respʳ-≈ record { ≡arity = ≡a } (<-arity x<y₁) = <-arity (proj₁ <-resp₂-≡ ≡a x<y₁)
-<-Edge-respʳ-≈ {_} {x} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x<y₁)
-    = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y₁)
-  where
-    module x = Edge x
-    open DTOP (HL.decTotalOrder x.arity) using (<-respʳ-≈)
-<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁)
-    = <-ports
-        ≡.refl
-        (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl)))
-        (Lex.<-respectsʳ
-            ≡-isPartialEquivalence
-            FinProp.<-respʳ-≡
-            (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
-            x<y₁)
-  where
-    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
-
-open Tri
-open ≈-Edge
-tri : {v : ℕ} → Trichotomous (≈-Edge {v}) (<-Edge {v})
-tri x y with <-cmp x.arity y.arity
-  where
-    module x = Edge x
-    module y = Edge y
-tri x y | tri< x<y x≢y y≮x = tri< (<-arity x<y) (λ x≡y → x≢y (≡arity x≡y)) ¬y<x
-  where
-    ¬y<x :  ¬ <-Edge y x
-    ¬y<x (<-arity y<x) = y≮x y<x
-    ¬y<x (<-label ≡a _) = x≢y (≡.sym ≡a)
-    ¬y<x (<-ports ≡a _ _) = x≢y (≡.sym ≡a)
-tri x y | tri≈ x≮y ≡.refl y≮x = compare-label
-  where
-    module x = Edge x
-    module y = Edge y
-    open StrictTotalOrder (HL.strictTotalOrder x.arity) using (compare)
-    import Relation.Binary.Properties.DecTotalOrder
-    open DTOP (HL.decTotalOrder x.arity) using (<-respˡ-≈)
-    compare-label : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
-    compare-label with compare x.label y.label
-    ... | tri< x<y x≢y y≮x′ = tri<
-            (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y))
-            (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
-            ¬y<x
-      where
-        ¬y<x :  ¬ <-Edge y x
-        ¬y<x (<-arity y<x) = y≮x y<x
-        ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
-        ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label))
-    ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports
-      where
-        compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
-        compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports
-        ... | tri< x<y x≢y y≮x″ =
-                tri<
-                  (<-ports ≡.refl
-                    (HL.≈-reflexive x≡y′)
-                    (Lex.<-respectsˡ
-                      ≡-isPartialEquivalence
-                      FinProp.<-respˡ-≡
-                      (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
-                      x<y))
-                  (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
-                  ¬y<x
-          where
-            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
-            ¬y<x :  ¬ <-Edge y x
-            ¬y<x (<-arity y<x) = y≮x y<x
-            ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
-            ¬y<x (<-ports _ _ y<x) =
-                y≮x″
-                  (Lex.<-respectsˡ
-                    ≡-isPartialEquivalence
-                    FinProp.<-respˡ-≡
-                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
-                    y<x)
-        ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈
-                ¬x<y
-                (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) })
-                ¬y<x
-          where
-            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
-            ¬x<y : ¬ <-Edge x y
-            ¬x<y (<-arity x<y) = x≮y x<y
-            ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
-            ¬x<y (<-ports _ _ x<y) =
-                x≮y″
-                  (Lex.<-respectsˡ
-                    ≡-isPartialEquivalence
-                    FinProp.<-respˡ-≡
-                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
-                    x<y)
-            ¬y<x : ¬ <-Edge y x
-            ¬y<x (<-arity y<x) = y≮x y<x
-            ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
-            ¬y<x (<-ports _ _ y<x) =
-                y≮x″
-                  (Lex.<-respectsˡ
-                    ≡-isPartialEquivalence
-                    FinProp.<-respˡ-≡
-                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
-                    y<x)
-
-        ... | tri> x≮y″ x≢y y<x =
-                tri>
-                  ¬x<y
-                  (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
-                  (<-ports
-                    ≡.refl
-                    (HL.≈-sym (HL.≈-reflexive x≡y′))
-                    (Lex.<-respectsˡ
-                      ≡-isPartialEquivalence
-                      FinProp.<-respˡ-≡
-                      (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
-                      y<x))
-          where
-            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
-            ¬x<y : ¬ <-Edge x y
-            ¬x<y (<-arity x<y) = x≮y x<y
-            ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
-            ¬x<y (<-ports _ _ x<y) =
-                x≮y″
-                  (Lex.<-respectsˡ
-                    ≡-isPartialEquivalence
-                    FinProp.<-respˡ-≡
-                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
-                    x<y)
-    ... | tri> x≮y′ x≢y y<x = tri>
-            ¬x<y
-            (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
-            (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) y<x))
-      where
-        ¬x<y : ¬ <-Edge x y
-        ¬x<y (<-arity x<y) = x≮y x<y
-        ¬x<y (<-label ≡a x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
-        ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l)
-tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)) (<-arity y<x)
-  where
-    ¬x<y :  ¬ <-Edge x y
-    ¬x<y (<-arity x<y) = x≮y x<y
-    ¬x<y (<-label ≡a x<y) = x≢y ≡a
-    ¬x<y (<-ports ≡a _ _) = x≢y ≡a
-
-isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
-isStrictTotalOrder = record
-    { isStrictPartialOrder = record
-        { isEquivalence = ≈-Edge-IsEquivalence
-        ; irrefl = <-Edge-irrefl
-        ; trans = <-Edge-trans
-        ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
-        }
-    ; compare = tri
-    }
-
-strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ
-strictTotalOrder {v} = record
-    { Carrier = Edge v
-    ; _≈_ = ≈-Edge {v}
-    ; _<_ = <-Edge {v}
-    ; isStrictTotalOrder = isStrictTotalOrder {v}
-    }
-
-show : {v : ℕ} → Edge v → String
-show 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
-
-module Sort {v} = ListSort (decTotalOrder {v})
-open Sort using (sort) public
+module _ {v : ℕ} where
+
+  -- an equivalence relation on edges with v nodes
+  record _≈_ (E E′ : Edge v) : Set where
+    constructor mk≈
+    module E = Edge E
+    module E′ = Edge E′
+    field
+      ≡arity : E.arity ≡ E′.arity
+      ≡label : cast ≡arity E.label ≡ E′.label
+      ≡ports : E.ports ≈[ ≡arity ] E′.ports
+
+  ≈-refl : {x : Edge v} → x ≈ x
+  ≈-refl = record
+      { ≡arity = ≡.refl
+      ; ≡label = HL.≈-reflexive ≡.refl
+      ; ≡ports = VecCast.≈-reflexive ≡.refl
+      }
+
+  ≈-sym : {x y : Edge v} → x ≈ y → y ≈ x
+  ≈-sym x≈y = record
+      { ≡arity = ≡.sym ≡arity
+      ; ≡label = HL.≈-sym ≡label
+      ; ≡ports = VecCast.≈-sym ≡ports
+      }
+    where
+      open _≈_ x≈y
+
+  ≈-trans : {i j k : Edge v} → i ≈ j → j ≈ k → i ≈ k
+  ≈-trans {i} {j} {k} i≈j j≈k = record
+      { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity
+      ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label
+      ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports
+      }
+    where
+      module i≈j = _≈_ i≈j
+      module j≈k = _≈_ j≈k
+
+  ≈-IsEquivalence : IsEquivalence _≈_
+  ≈-IsEquivalence = record
+      { refl = ≈-refl
+      ; sym = ≈-sym
+      ; trans = ≈-trans
+      }
+
+  show : Edge v → String
+  show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin p
+
+  ≈⇒≡ : {x y : Edge v} → x ≈ y → x ≡ y
+  ≈⇒≡ {mkEdge l p} (mk≈ ≡.refl ≡.refl ≡.refl)
+    rewrite cast-is-id ≡.refl l
+    rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
 
 Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
-Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} }
+Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} }
diff --git a/Data/Hypergraph/Edge/Order.agda b/Data/Hypergraph/Edge/Order.agda
new file mode 100644
index 0000000..4b3c1e8
--- /dev/null
+++ b/Data/Hypergraph/Edge/Order.agda
@@ -0,0 +1,280 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Edge.Order (HL : HypergraphLabel) where
+
+import Data.List.Sort as ListSort
+import Data.Fin as Fin
+import Data.Fin.Properties as FinProp
+import Data.Vec as Vec
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Data.Vec.Relation.Binary.Lex.Strict as Lex
+import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Properties.DecTotalOrder as DTOP
+import Relation.Binary.Properties.StrictTotalOrder as STOP
+
+open import Data.Hypergraph.Edge HL using (Edge; ≈-Edge; ≈-Edge-IsEquivalence)
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ; _<_)
+open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-≡⇒≡)
+open import Level using (0ℓ)
+open import Relation.Binary
+  using
+    ( Rel
+    ; Tri ; Trichotomous
+    ; IsStrictTotalOrder ; IsEquivalence
+    ; _Respects_
+    ; DecTotalOrder ; StrictTotalOrder
+    )
+open import Relation.Nullary using (¬_)
+
+module HL = HypergraphLabel HL
+open HL using (Label; cast; cast-is-id)
+open Vec using (Vec)
+
+open ≡ using (_≡_)
+
+open HL using (_[_<_])
+_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ
+_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v})
+
+data <-Edge {v : ℕ} : Edge v → Edge v → Set where
+  <-arity
+      : {x y : Edge v}
+      → Edge.arity x < Edge.arity y
+      → <-Edge x y
+  <-label
+      : {x y : Edge v}
+        (≡a : Edge.arity x ≡ Edge.arity y)
+      → Edge.arity y [ cast ≡a (Edge.label x) < Edge.label y ]
+      → <-Edge x y
+  <-ports
+      : {x y : Edge v}
+        (≡a : Edge.arity x ≡ Edge.arity y)
+        (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y)
+      → Vec.cast ≡a (Edge.ports x) << Edge.ports y
+      → <-Edge x y
+
+<-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y
+<-Edge-irrefl record { ≡arity = ≡a } (<-arity n<m) = <-irrefl ≡a n<m
+<-Edge-irrefl record { ≡label = ≡l } (<-label _ (_ , x≉y)) = x≉y ≡l
+<-Edge-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y)
+    = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y
+
+<-Edge-trans : {v : ℕ} {i j k : Edge v} → <-Edge i j → <-Edge j k → <-Edge i k
+<-Edge-trans (<-arity i<j) (<-arity j<k) = <-arity (<-trans i<j j<k)
+<-Edge-trans (<-arity i<j) (<-label ≡.refl j<k) = <-arity i<j
+<-Edge-trans (<-arity i<j) (<-ports ≡.refl _ j<k) = <-arity i<j
+<-Edge-trans (<-label ≡.refl i<j) (<-arity j<k) = <-arity j<k
+<-Edge-trans {_} {i} (<-label ≡.refl i<j) (<-label ≡.refl j<k)
+    = <-label ≡.refl (<-label-trans i<j (<-respˡ-≈ (HL.≈-reflexive ≡.refl) j<k))
+  where
+    open DTOP (HL.decTotalOrder (Edge.arity i)) using (<-respˡ-≈) renaming (<-trans to <-label-trans)
+<-Edge-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _)
+    = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j)
+  where
+    open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈)
+<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k
+<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k)
+    = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k)
+  where
+    open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈)
+<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k)
+  rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j))
+    = <-ports ≡.refl
+        (HL.≈-trans ≡l₁ ≡l₂)
+        (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k)
+  where
+    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+<-Edge-respˡ-≈ : {v : ℕ} {y : Edge v} → (λ x → <-Edge x y) Respects ≈-Edge
+<-Edge-respˡ-≈ ≈x (<-arity x₁<y) = <-arity (proj₂ <-resp₂-≡ ≡arity x₁<y)
+  where
+    open ≈-Edge ≈x using (≡arity)
+<-Edge-respˡ-≈ {_} {y} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x₁<y)
+    = <-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x₁<y)
+  where
+    module y = Edge y
+    open DTOP (HL.decTotalOrder y.arity) using (<-respˡ-≈)
+<-Edge-respˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y)
+    = <-ports
+        ≡.refl
+        (≡.cong (cast _) (HL.≈-reflexive ≡.refl))
+        (Lex.<-respectsˡ
+            ≡-isPartialEquivalence
+            FinProp.<-respˡ-≡
+            (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+            x₁<y)
+  where
+    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+<-Edge-respʳ-≈ : {v : ℕ} {x : Edge v} → <-Edge x Respects ≈-Edge
+<-Edge-respʳ-≈ record { ≡arity = ≡a } (<-arity x<y₁) = <-arity (proj₁ <-resp₂-≡ ≡a x<y₁)
+<-Edge-respʳ-≈ {_} {x} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x<y₁)
+    = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y₁)
+  where
+    module x = Edge x
+    open DTOP (HL.decTotalOrder x.arity) using (<-respʳ-≈)
+<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁)
+    = <-ports
+        ≡.refl
+        (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl)))
+        (Lex.<-respectsʳ
+            ≡-isPartialEquivalence
+            FinProp.<-respʳ-≡
+            (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+            x<y₁)
+  where
+    open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+open Tri
+open ≈-Edge
+tri : {v : ℕ} → Trichotomous (≈-Edge {v}) (<-Edge {v})
+tri x y with <-cmp x.arity y.arity
+  where
+    module x = Edge x
+    module y = Edge y
+tri x y | tri< x<y x≢y y≮x = tri< (<-arity x<y) (λ x≡y → x≢y (≡arity x≡y)) ¬y<x
+  where
+    ¬y<x :  ¬ <-Edge y x
+    ¬y<x (<-arity y<x) = y≮x y<x
+    ¬y<x (<-label ≡a _) = x≢y (≡.sym ≡a)
+    ¬y<x (<-ports ≡a _ _) = x≢y (≡.sym ≡a)
+tri x y | tri≈ x≮y ≡.refl y≮x = compare-label
+  where
+    module x = Edge x
+    module y = Edge y
+    open StrictTotalOrder (HL.strictTotalOrder x.arity) using (compare)
+    import Relation.Binary.Properties.DecTotalOrder
+    open DTOP (HL.decTotalOrder x.arity) using (<-respˡ-≈)
+    compare-label : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+    compare-label with compare x.label y.label
+    ... | tri< x<y x≢y y≮x′ = tri<
+            (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y))
+            (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+            ¬y<x
+      where
+        ¬y<x :  ¬ <-Edge y x
+        ¬y<x (<-arity y<x) = y≮x y<x
+        ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+        ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label))
+    ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports
+      where
+        compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+        compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports
+        ... | tri< x<y x≢y y≮x″ =
+                tri<
+                  (<-ports ≡.refl
+                    (HL.≈-reflexive x≡y′)
+                    (Lex.<-respectsˡ
+                      ≡-isPartialEquivalence
+                      FinProp.<-respˡ-≡
+                      (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+                      x<y))
+                  (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
+                  ¬y<x
+          where
+            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+            ¬y<x :  ¬ <-Edge y x
+            ¬y<x (<-arity y<x) = y≮x y<x
+            ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+            ¬y<x (<-ports _ _ y<x) =
+                y≮x″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    y<x)
+        ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈
+                ¬x<y
+                (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) })
+                ¬y<x
+          where
+            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+            ¬x<y : ¬ <-Edge x y
+            ¬x<y (<-arity x<y) = x≮y x<y
+            ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+            ¬x<y (<-ports _ _ x<y) =
+                x≮y″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    x<y)
+            ¬y<x : ¬ <-Edge y x
+            ¬y<x (<-arity y<x) = y≮x y<x
+            ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+            ¬y<x (<-ports _ _ y<x) =
+                y≮x″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    y<x)
+
+        ... | tri> x≮y″ x≢y y<x =
+                tri>
+                  ¬x<y
+                  (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
+                  (<-ports
+                    ≡.refl
+                    (HL.≈-sym (HL.≈-reflexive x≡y′))
+                    (Lex.<-respectsˡ
+                      ≡-isPartialEquivalence
+                      FinProp.<-respˡ-≡
+                      (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+                      y<x))
+          where
+            open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+            ¬x<y : ¬ <-Edge x y
+            ¬x<y (<-arity x<y) = x≮y x<y
+            ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+            ¬x<y (<-ports _ _ x<y) =
+                x≮y″
+                  (Lex.<-respectsˡ
+                    ≡-isPartialEquivalence
+                    FinProp.<-respˡ-≡
+                    (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+                    x<y)
+    ... | tri> x≮y′ x≢y y<x = tri>
+            ¬x<y
+            (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+            (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) y<x))
+      where
+        ¬x<y : ¬ <-Edge x y
+        ¬x<y (<-arity x<y) = x≮y x<y
+        ¬x<y (<-label ≡a x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+        ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l)
+tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)) (<-arity y<x)
+  where
+    ¬x<y :  ¬ <-Edge x y
+    ¬x<y (<-arity x<y) = x≮y x<y
+    ¬x<y (<-label ≡a x<y) = x≢y ≡a
+    ¬x<y (<-ports ≡a _ _) = x≢y ≡a
+
+isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
+isStrictTotalOrder = record
+    { isStrictPartialOrder = record
+        { isEquivalence = ≈-Edge-IsEquivalence
+        ; irrefl = <-Edge-irrefl
+        ; trans = <-Edge-trans
+        ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
+        }
+    ; compare = tri
+    }
+
+strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ
+strictTotalOrder {v} = record
+    { Carrier = Edge v
+    ; _≈_ = ≈-Edge {v}
+    ; _<_ = <-Edge {v}
+    ; isStrictTotalOrder = isStrictTotalOrder {v}
+    }
+
+open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public
+
+module Sort {v} = ListSort (decTotalOrder {v})
+open Sort using (sort) public
diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda
deleted file mode 100644
index d9cc024..0000000
--- a/Data/Hypergraph/Setoid.agda
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level; _⊔_)
-open import Data.Hypergraph.Label using (HypergraphLabel)
-
-module Data.Hypergraph.Setoid {c ℓ : Level} (HL : HypergraphLabel) where
-
-import Data.List.Relation.Binary.Permutation.Propositional as List-↭
-
-open import Data.Hypergraph.Edge HL using (module Sort)
-open import Data.Hypergraph.Base {c} HL using (Hypergraph; normalize)
-open import Data.Nat using (ℕ)
-open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-
--- an equivalence relation on hypergraphs
-record _≈_ {v : ℕ} (H H′ : Hypergraph v) : Set (c ⊔ ℓ) where
-
-  constructor mk≈
-
-  module H = Hypergraph H
-  module H′ = Hypergraph H′
-
-  field
-    ≡-normalized : normalize H ≡ normalize H′
-
-  open Hypergraph using (edges)
-
-  ≡-edges : edges (normalize H) ≡ edges (normalize H′)
-  ≡-edges = ≡.cong edges ≡-normalized
-
-  open List-↭ using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
-  open Sort using (sort-↭)
-
-  ↭-edges : H.edges ↭ H′.edges
-  ↭-edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡-edges) (sort-↭ H′.edges))
-
-infixr 4 _≈_
-
-≈-refl : {v : ℕ} {H : Hypergraph v} → H ≈ H
-≈-refl = mk≈ ≡.refl
-
-≈-sym : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H
-≈-sym (mk≈ ≡n) = mk≈ (≡.sym ≡n)
-
-≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″
-≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (≡.trans ≡n₁ ≡n₂)
-
--- The setoid of labeled hypergraphs with v nodes
-Hypergraphₛ : ℕ → Setoid c (c ⊔ ℓ)
-Hypergraphₛ v = record
-    { Carrier = Hypergraph v
-    ; _≈_ = _≈_
-    ; isEquivalence = record
-        { refl = ≈-refl
-        ; sym = ≈-sym
-        ; trans = ≈-trans
-        }
-    }
diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda
index 0f18c4c..d5bcc9b 100644
--- a/Functor/Instance/Nat/Circ.agda
+++ b/Functor/Instance/Nat/Circ.agda
@@ -24,7 +24,7 @@ module List∘Edge = Functor List∘Edge
 open Func
 open Functor
 
-Circ : Functor Nat (Setoids c (c ⊔ ℓ))
+Circ : Functor Nat (Setoids c ℓ)
 Circ .F₀ = Circuitₛ
 Circ .F₁ = mapₛ
 Circ .identity = cong mkCircuitₛ List∘Edge.identity
diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda
index 618807d..f8d47c2 100644
--- a/Functor/Instance/Nat/Edge.agda
+++ b/Functor/Instance/Nat/Edge.agda
@@ -11,7 +11,7 @@ open import Categories.Category.Instance.Nat using (Nat)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
 open import Data.Fin using (Fin)
-open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ)
+open import Data.Hypergraph.Edge HL as Edge using (Edgeₛ; map; _≈_)
 open import Data.Nat using (ℕ)
 open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive)
 open import Level using (0ℓ)
@@ -22,10 +22,9 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 module HL = HypergraphLabel HL
 
 open Edge.Edge
+open Edge._≈_
 open Func
 open Functor
-open Setoid
-open ≈-Edge
 
 Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
 Edge₁ f .to = map f
@@ -35,7 +34,7 @@ Edge₁ f .cong x≈y = record
     ; ≡ports = ≈-cong′ (Vec.map f) (≡ports x≈y)
     }
 
-map-id : {v : ℕ} {e : Edge.Edge v} → ≈-Edge (map id e) e
+map-id : {v : ℕ} {e : Edge.Edge v} → map id e ≈ e
 map-id .≡arity = ≡.refl
 map-id .≡label = HL.≈-reflexive ≡.refl
 map-id {_} {e} .≡ports = ≈-reflexive (VecProps.map-id (ports e))
@@ -45,7 +44,7 @@ map-∘
       (f : Fin n → Fin m)
       (g : Fin m → Fin o)
       {e : Edge.Edge n}
-    → ≈-Edge (map (g ∘ f) e) (map g (map f e))
+    → map (g ∘ f) e ≈ map g (map f e)
 map-∘ f g .≡arity = ≡.refl
 map-∘ f g .≡label = HL.≈-reflexive ≡.refl
 map-∘ f g {e} .≡ports = ≈-reflexive (VecProps.map-∘ g f (ports e))
@@ -55,7 +54,7 @@ map-resp-≗
       {f g : Fin n → Fin m}
     → f ≗ g
     → {e : Edge.Edge n}
-    → ≈-Edge (map f e) (map g e)
+    → map f e ≈ map g e
 map-resp-≗ f≗g .≡arity = ≡.refl
 map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl
 map-resp-≗ f≗g {e} .≡ports = ≈-reflexive (VecProps.map-cong f≗g (ports e))
-- 
cgit v1.2.3