From 02a7c2e196435b6b60a1164ff75a805685d2d151 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 19 Jun 2025 20:11:18 -0500
Subject: Add new hypergraph definitions

---
 Data/Hypergraph/Base.agda | 55 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 Data/Hypergraph/Base.agda

(limited to 'Data/Hypergraph')

diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
new file mode 100644
index 0000000..a2157fb
--- /dev/null
+++ b/Data/Hypergraph/Base.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Hypergraph.Base where
+
+open import Data.Castable using (IsCastable)
+open import Data.Nat.Base using (ℕ)
+open import Data.Fin using (Fin)
+
+import Data.Vec.Base as VecBase
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Relation.Binary.PropositionalEquality as ≡
+
+open import Relation.Binary using (Rel; IsDecTotalOrder)
+open import Data.Nat.Base using (ℕ)
+open import Level using (Level; suc; _⊔_)
+
+record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+  field
+    Label : ℕ → Set ℓ
+    isCastable : IsCastable Label
+    _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
+    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+    decTotalOrder : (n : ℕ) → IsDecTotalOrder (n [_≈_]) (n [_≤_])
+  open IsCastable isCastable public
+
+module Edge (HL : HypergraphLabel) where
+
+  open HypergraphLabel HL using (Label; cast)
+  open VecBase using (Vec)
+
+  record Edge (v : ℕ) : Set where
+    field
+      {arity} : ℕ
+      label : Label arity
+      ports : Vec (Fin v) arity
+
+  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
+
+module HypergraphList (HL : HypergraphLabel) where
+
+  open import Data.List.Base using (List)
+  open Edge HL using (Edge)
+
+  record Hypergraph (v : ℕ) : Set where
+    field
+      edges : List (Edge v)
-- 
cgit v1.2.3


From 6831517a4a8358415e5664b974000620b2581c3f Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 1 Jul 2025 23:09:57 -0500
Subject: Begin strict total order for hypergraph edges

---
 Data/Castable.agda        |  28 +++++++-
 Data/Hypergraph/Base.agda | 179 +++++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 198 insertions(+), 9 deletions(-)

(limited to 'Data/Hypergraph')

diff --git a/Data/Castable.agda b/Data/Castable.agda
index 2c6932e..4f85b3d 100644
--- a/Data/Castable.agda
+++ b/Data/Castable.agda
@@ -3,7 +3,8 @@
 module Data.Castable where
 
 open import Level using (Level; suc; _⊔_)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; subst)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong; module ≡-Reasoning)
+open import Relation.Binary using (Sym; Trans; _⇒_)
 
 record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
 
@@ -18,6 +19,31 @@ record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂
     cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x
     subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x
 
+  infix 3 _≈[_]_
+  _≈[_]_ : {n m : A} → B n → .(eq : n ≡ m) → B m → Set ℓ₂
+  _≈[_]_ x eq y = cast eq x ≡ y
+
+  ≈-reflexive : {n : A} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys)
+  ≈-reflexive {n} {x} {y} eq = trans (cast-is-id refl x) eq
+
+  ≈-sym : {m n : A} .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_
+  ≈-sym {m} {n} {m≡n} {x} {y} x≡y = begin
+      cast (sym m≡n) y             ≡⟨ cong (cast (sym m≡n)) x≡y ⟨
+      cast (sym m≡n) (cast m≡n x)  ≡⟨ cast-trans m≡n (sym m≡n) x ⟩
+      cast (trans m≡n (sym m≡n)) x ≡⟨ cast-is-id (trans m≡n (sym m≡n)) x ⟩
+      x ∎
+    where
+      open ≡-Reasoning
+
+  ≈-trans : {m n o : A} .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
+  ≈-trans {m} {n} {o} {m≡n} {n≡o} {x} {y} {z} x≡y y≡z = begin
+      cast (trans m≡n n≡o) x  ≡⟨ cast-trans m≡n n≡o x ⟨
+      cast n≡o (cast m≡n x)   ≡⟨ cong (cast n≡o) x≡y ⟩
+      cast n≡o y              ≡⟨ y≡z ⟩
+      z ∎
+    where
+      open ≡-Reasoning
+
 record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where
   field
     B : A → Set ℓ₂
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index a2157fb..f54468d 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -3,29 +3,57 @@
 module Data.Hypergraph.Base where
 
 open import Data.Castable using (IsCastable)
-open import Data.Nat.Base using (ℕ)
 open import Data.Fin using (Fin)
 
+open import Relation.Binary
+  using
+    ( Rel
+    ; IsDecTotalOrder
+    ; IsStrictTotalOrder
+    ; Tri
+    ; Trichotomous
+    ; _Respectsˡ_
+    ; _Respectsʳ_
+    ; _Respects_
+    )
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Nullary using (¬_)
+open import Data.Nat.Base using (ℕ; _<_)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
+open import Level using (Level; suc; _⊔_)
+
 import Data.Vec.Base as VecBase
 import Data.Vec.Relation.Binary.Equality.Cast as VecCast
 import Relation.Binary.PropositionalEquality as ≡
-
-open import Relation.Binary using (Rel; IsDecTotalOrder)
-open import Data.Nat.Base using (ℕ)
-open import Level using (Level; suc; _⊔_)
+import Relation.Binary.Properties.DecTotalOrder as DTOP
 
 record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
   field
     Label : ℕ → Set ℓ
     isCastable : IsCastable Label
-    _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
+    -- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
     _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
-    decTotalOrder : (n : ℕ) → IsDecTotalOrder (n [_≈_]) (n [_≤_])
+    isDecTotalOrder : (n : ℕ) → IsDecTotalOrder ≡._≡_ (n [_≤_])
+  decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+  decTotalOrder n = record
+      { Carrier = Label n
+      ; _≈_ = ≡._≡_
+      ; _≤_ = n [_≤_]
+      ; isDecTotalOrder = isDecTotalOrder n
+      }
+
+  open DTOP using (<-strictTotalOrder) renaming (_<_ to <)
+  _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+  _[_<_] n =  < (decTotalOrder n)
+  strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+  strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
   open IsCastable isCastable public
 
 module Edge (HL : HypergraphLabel) where
 
-  open HypergraphLabel HL using (Label; cast)
+  module HL = HypergraphLabel HL
+  open HL using (Label; cast; cast-is-id; cast-trans)
   open VecBase using (Vec)
 
   record Edge (v : ℕ) : Set where
@@ -38,6 +66,7 @@ module Edge (HL : HypergraphLabel) where
   open VecCast using (_≈[_]_)
 
   record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
+    eta-equality
     module E = Edge E
     module E′ = Edge E′
     field
@@ -45,6 +74,140 @@ module Edge (HL : HypergraphLabel) where
       ≡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
+
+  open HL using (_[_<_])
+  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
+
+  <-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-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 (<-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-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ʳ-≈ : {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ʳ-≈)
+
+  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 y<x) = 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 ≡a y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+      ... | tri≈ x≮y x≡y y≮x = compare-ports
+        where
+          compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+          compare-ports = ?
+      ... | 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)
+  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
+
+  isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
+  isStrictTotalOrder = record
+      { isStrictPartialOrder = record
+          { isEquivalence = record
+              { refl = ≈-Edge-refl
+              ; sym = ≈-Edge-sym
+              ; trans = ≈-Edge-trans
+              }
+          ; irrefl = <-Edge-irrefl
+          ; trans = <-Edge-trans
+          ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
+          }
+      ; compare = tri
+      }
+
 module HypergraphList (HL : HypergraphLabel) where
 
   open import Data.List.Base using (List)
-- 
cgit v1.2.3


From 1ea3199a7806ecbefba986ea28cf976497da5ca4 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 3 Jul 2025 11:55:43 -0500
Subject: Finish strict total order for hypergraph edges

---
 Data/Hypergraph/Base.agda | 178 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 173 insertions(+), 5 deletions(-)

(limited to 'Data/Hypergraph')

diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index f54468d..0771a78 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -17,20 +17,31 @@ open import Relation.Binary
     ; _Respects_
     )
 open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Nullary using (¬_)
 open import Data.Nat.Base using (ℕ; _<_)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
-open import Level using (Level; suc; _⊔_)
+open import Level using (Level; suc; _⊔_; 0ℓ)
+open import Data.String using (String; _<+>_; unlines)
+open import Data.Fin.Show using () renaming (show to showFin)
+open import Data.List.Show using () renaming (show to showList)
+open import Data.List.Base using (map)
+open import Data.Vec.Show using () renaming (show to showVec)
 
+import Data.Fin.Base as Fin
+import Data.Fin.Properties as FinProp
 import Data.Vec.Base as VecBase
 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
 
 record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
   field
     Label : ℕ → Set ℓ
+    showLabel : (n : ℕ) → Label n → String
     isCastable : IsCastable Label
     -- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
     _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
@@ -105,6 +116,8 @@ module Edge (HL : HypergraphLabel) where
       module j≈k = ≈-Edge j≈k
 
   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}
@@ -115,19 +128,46 @@ module Edge (HL : HypergraphLabel) where
           (≡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)
+        → VecBase.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
+    where
+      open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
 
   <-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)
@@ -138,6 +178,19 @@ module Edge (HL : HypergraphLabel) where
     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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
+      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₁)
@@ -145,6 +198,18 @@ module Edge (HL : HypergraphLabel) where
     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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
+      open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
 
   open Tri
   open ≈-Edge
@@ -157,7 +222,8 @@ module Edge (HL : HypergraphLabel) where
     where
       ¬y<x :  ¬ <-Edge y x
       ¬y<x (<-arity y<x) = y≮x y<x
-      ¬y<x (<-label ≡a y<x) = x≢y (≡.sym ≡a)
+      ¬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
@@ -174,11 +240,89 @@ module Edge (HL : HypergraphLabel) where
         where
           ¬y<x :  ¬ <-Edge y x
           ¬y<x (<-arity y<x) = y≮x y<x
-          ¬y<x (<-label ≡a y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
-      ... | tri≈ x≮y x≡y y≮x = compare-ports
+          ¬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 = ?
+          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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
+              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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
+              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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
+              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)))
@@ -187,11 +331,13 @@ module Edge (HL : HypergraphLabel) 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
@@ -208,6 +354,19 @@ module Edge (HL : HypergraphLabel) where
       ; 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
+
+  showEdge : {v : ℕ} → Edge v → String
+  showEdge record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p
+
 module HypergraphList (HL : HypergraphLabel) where
 
   open import Data.List.Base using (List)
@@ -216,3 +375,12 @@ module HypergraphList (HL : HypergraphLabel) where
   record Hypergraph (v : ℕ) : Set where
     field
       edges : List (Edge v)
+
+  sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
+  sortHypergraph {v} H = record { edges = sort edges }
+    where
+      open Hypergraph H
+      open import Data.List.Sort.MergeSort (Edge.decTotalOrder HL) using (sort)
+
+  showHypergraph : {v : ℕ} → Hypergraph v → String
+  showHypergraph record { edges = e} = unlines (map (Edge.showEdge HL) e)
-- 
cgit v1.2.3


From ee5c56a58154840f08a18d581983d6f6f3630970 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 9 Jul 2025 12:15:51 -0500
Subject: Split hypergraph label and edge into separate files

---
 Data/Hypergraph/Base.agda  | 393 ++-------------------------------------------
 Data/Hypergraph/Edge.agda  | 326 +++++++++++++++++++++++++++++++++++++
 Data/Hypergraph/Label.agda |  36 +++++
 3 files changed, 378 insertions(+), 377 deletions(-)
 create mode 100644 Data/Hypergraph/Edge.agda
 create mode 100644 Data/Hypergraph/Label.agda

(limited to 'Data/Hypergraph')

diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index 0771a78..e43cbce 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -1,386 +1,25 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Data.Hypergraph.Base where
+open import Data.Hypergraph.Label using (HypergraphLabel)
 
-open import Data.Castable using (IsCastable)
-open import Data.Fin using (Fin)
+module Data.Hypergraph.Base (HL : HypergraphLabel) where
 
-open import Relation.Binary
-  using
-    ( Rel
-    ; IsDecTotalOrder
-    ; IsStrictTotalOrder
-    ; Tri
-    ; Trichotomous
-    ; _Respectsˡ_
-    ; _Respectsʳ_
-    ; _Respects_
-    )
-open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
-open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Nullary using (¬_)
-open import Data.Nat.Base using (ℕ; _<_)
-open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
-open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
-open import Level using (Level; suc; _⊔_; 0ℓ)
-open import Data.String using (String; _<+>_; unlines)
-open import Data.Fin.Show using () renaming (show to showFin)
-open import Data.List.Show using () renaming (show to showList)
-open import Data.List.Base using (map)
-open import Data.Vec.Show using () renaming (show to showVec)
+open import Data.Hypergraph.Edge HL using (Edge; decTotalOrder; showEdge)
+open import Data.List.Base using (List; map)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String; unlines)
 
-import Data.Fin.Base as Fin
-import Data.Fin.Properties as FinProp
-import Data.Vec.Base as VecBase
-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
+import Data.List.Sort.MergeSort as MergeSort
 
-record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+record Hypergraph (v : ℕ) : Set where
   field
-    Label : ℕ → Set ℓ
-    showLabel : (n : ℕ) → Label n → String
-    isCastable : IsCastable Label
-    -- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
-    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
-    isDecTotalOrder : (n : ℕ) → IsDecTotalOrder ≡._≡_ (n [_≤_])
-  decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
-  decTotalOrder n = record
-      { Carrier = Label n
-      ; _≈_ = ≡._≡_
-      ; _≤_ = n [_≤_]
-      ; isDecTotalOrder = isDecTotalOrder n
-      }
+    edges : List (Edge v)
 
-  open DTOP using (<-strictTotalOrder) renaming (_<_ to <)
-  _[_<_] : (n : ℕ) → Rel (Label n) ℓ
-  _[_<_] n =  < (decTotalOrder n)
-  strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
-  strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
-  open IsCastable isCastable public
+sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
+sortHypergraph {v} H = record { edges = sort edges }
+  where
+    open Hypergraph H
+    open MergeSort decTotalOrder using (sort)
 
-module Edge (HL : HypergraphLabel) where
-
-  module HL = HypergraphLabel HL
-  open HL using (Label; cast; cast-is-id; cast-trans)
-  open VecBase using (Vec)
-
-  record Edge (v : ℕ) : Set where
-    field
-      {arity} : ℕ
-      label : Label arity
-      ports : Vec (Fin v) arity
-
-  open ≡ using (_≡_)
-  open VecCast using (_≈[_]_)
-
-  record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
-    eta-equality
-    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
-
-  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)
-        → VecBase.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
-    where
-      open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
-
-  <-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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
-      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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
-      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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
-              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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
-              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 import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡)
-              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 = record
-              { refl = ≈-Edge-refl
-              ; sym = ≈-Edge-sym
-              ; trans = ≈-Edge-trans
-              }
-          ; 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
-
-  showEdge : {v : ℕ} → Edge v → String
-  showEdge record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p
-
-module HypergraphList (HL : HypergraphLabel) where
-
-  open import Data.List.Base using (List)
-  open Edge HL using (Edge)
-
-  record Hypergraph (v : ℕ) : Set where
-    field
-      edges : List (Edge v)
-
-  sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
-  sortHypergraph {v} H = record { edges = sort edges }
-    where
-      open Hypergraph H
-      open import Data.List.Sort.MergeSort (Edge.decTotalOrder HL) using (sort)
-
-  showHypergraph : {v : ℕ} → Hypergraph v → String
-  showHypergraph record { edges = e} = unlines (map (Edge.showEdge HL) e)
+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
new file mode 100644
index 0000000..3c2a3a1
--- /dev/null
+++ b/Data/Hypergraph/Edge.agda
@@ -0,0 +1,326 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Edge (HL : HypergraphLabel) where
+
+
+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.Base using (ℕ; _<_)
+open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+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.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Nullary using (¬_)
+
+import Data.Fin.Base as Fin
+import Data.Fin.Properties as FinProp
+import Data.Vec.Base as VecBase
+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
+
+module HL = HypergraphLabel HL
+open HL using (Label; cast; cast-is-id)
+open VecBase using (Vec)
+
+record Edge (v : ℕ) : Set where
+  field
+    {arity} : ℕ
+    label : Label arity
+    ports : Vec (Fin v) arity
+
+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
+
+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)
+      → VecBase.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 = record
+            { refl = ≈-Edge-refl
+            ; sym = ≈-Edge-sym
+            ; trans = ≈-Edge-trans
+            }
+        ; 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}
+    }
+
+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
diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda
new file mode 100644
index 0000000..c23d33a
--- /dev/null
+++ b/Data/Hypergraph/Label.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --safe #-}
+module Data.Hypergraph.Label where
+
+open import Data.Castable using (IsCastable)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String)
+open import Level using (Level; suc)
+open import Relation.Binary using (Rel; IsDecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Properties.DecTotalOrder using (<-strictTotalOrder; _<_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+
+  field
+    Label : ℕ → Set ℓ
+    showLabel : (n : ℕ) → Label n → String
+    isCastable : IsCastable Label
+    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+    isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
+
+  decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+  decTotalOrder n = record
+      { Carrier = Label n
+      ; _≈_ = _≡_
+      ; _≤_ = n [_≤_]
+      ; isDecTotalOrder = isDecTotalOrder n
+      }
+
+  _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+  _[_<_] n =  _<_ (decTotalOrder n)
+
+  strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+  strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
+
+  open IsCastable isCastable public
-- 
cgit v1.2.3


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/Base.agda   |  4 ++--
 Data/Hypergraph/Edge.agda   |  5 +++++
 Data/Hypergraph/Setoid.agda | 50 +++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 57 insertions(+), 2 deletions(-)
 create mode 100644 Data/Hypergraph/Setoid.agda

(limited to 'Data/Hypergraph')

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


From 21aa7526f51030be9ffd86be2eabd5d07f64b6f4 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 15 Oct 2025 13:31:13 -0500
Subject: Strengthen permutation sort theorem

---
 Data/Circuit/Convert.agda  | 42 +++++++++++++++++---------------
 Data/Hypergraph/Base.agda  |  1 +
 Data/Hypergraph/Edge.agda  | 14 +++++++----
 Data/Permutation/Sort.agda | 60 ++++++++++++++++++++++++++++++----------------
 4 files changed, 73 insertions(+), 44 deletions(-)

(limited to 'Data/Hypergraph')

diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda
index 497b0cd..ce6de69 100644
--- a/Data/Circuit/Convert.agda
+++ b/Data/Circuit/Convert.agda
@@ -5,16 +5,24 @@ module Data.Circuit.Convert where
 open import Data.Nat.Base using (ℕ)
 open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate)
 open import Data.Fin.Base using (Fin)
-open import Function.Bundles using (Equivalence)
 open import Data.Hypergraph.Edge GateLabel using (Edge)
-open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph)
+open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph)
 open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph)
 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.Base using (_∘_; id; _$_)
-
+open import Function.Bundles using (Equivalence; _↔_)
+open import Function.Base using (_∘_; 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 as LabeledHypergraph
+
 open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′)
 
 to : {v : ℕ} → Hypergraph v → Hypergraph′ v
@@ -37,9 +45,6 @@ from {v} H = record
     asEdge : Fin h → Edge v
     asEdge e = record { label = l e ; ports = toVec (j e) }
 
-open import Data.Product.Base using (proj₁; proj₂)
-open import Data.Fin.Permutation using (flip)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′)
 to-cong {v} {H} {H′} ≈H = record
     { ↔h = flip ρ
@@ -49,8 +54,6 @@ to-cong {v} {H} {H′} ≈H = record
     }
   where
     open Edge using (arity; ports; label)
-    open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
-    open import Function.Bundles using (_↔_)
     open ≈-Hypergraph ≈H
     open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ)
     open import Data.Fin.Base using (cast)
@@ -87,11 +90,9 @@ to-cong {v} {H} {H′} ≈H = record
           ≡.refl
 
 module _ {v : ℕ} where
-  open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge⇒≡)
+  open import Data.Hypergraph.Edge GateLabel 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.Permutation.Propositional using (_↭_)
-  open import Data.Vec.Functional.Relation.Binary.Permutation using () renaming (_↭_ to _↭′_)
   open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map)
   open import Data.Product.Base using (_,_)
   open import Data.Hypergraph.Label using (HypergraphLabel)
@@ -172,21 +173,24 @@ module _ {v : ℕ} where
           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 (flip ↔h Data.Fin.Permutation.⟨$⟩ʳ e) ≡ asEdge H′ e
+      H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e
       H∘ρ≗H′ e = ≈-Edge⇒≡ record
           { ≡arity = ≗a′ e
           ; ≡label = ≗l′ e
           ; ≡ports = ≗p′ e
           }
 
+      open Hypergraph using (edges)
+      open →-Reasoning
       ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′)
       ≡sorted =
-          ≡.cong (λ x → record { edges = x } ) $
-          Pointwise-≡⇒≡ $
-          map ≈-Edge⇒≡ $
-          sorted-≋ $
-          toList-↭ $
-          flip ↔h , H∘ρ≗H′
+             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          ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′)
 
 equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v)
 equiv v = record
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index 5cf5388..6988cf0 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -12,6 +12,7 @@ open import Data.String using (String; unlines)
 import Data.List.Sort as Sort
 
 record Hypergraph (v : ℕ) : Set where
+  constructor mkHypergraph
   field
     edges : List (Edge v)
 
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index cbf61e6..13b9278 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -80,6 +80,14 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
     module i≈j = ≈-Edge i≈j
     module j≈k = ≈-Edge j≈k
 
+open import Relation.Binary using (IsEquivalence)
+≈-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})
@@ -300,11 +308,7 @@ tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)
 isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
 isStrictTotalOrder = record
     { isStrictPartialOrder = record
-        { isEquivalence = record
-            { refl = ≈-Edge-refl
-            ; sym = ≈-Edge-sym
-            ; trans = ≈-Edge-trans
-            }
+        { isEquivalence = ≈-Edge-IsEquivalence
         ; irrefl = <-Edge-irrefl
         ; trans = <-Edge-trans
         ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda
index 977443a..658997d 100644
--- a/Data/Permutation/Sort.agda
+++ b/Data/Permutation/Sort.agda
@@ -14,20 +14,23 @@ open DecTotalOrder dto
     )
   renaming (Carrier to A; trans to ≤-trans; reflexive to ≤-reflexive)
 
-open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (ℕ)
 open import Data.List.Base using (List; _++_; [_])
 open import Data.List.Membership.Setoid Eq.setoid using (_∈_)
 open import Data.List.Relation.Binary.Pointwise using (module Pointwise)
-open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans)
+open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans; ≋-length; Any-resp-≋)
 open import Data.List.Relation.Unary.Linked using (Linked)
 open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-trans; ↭-sym)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (↭-length)
+open import Data.List.Relation.Binary.Permutation.Homogeneous using (map)
+open import Data.List.Relation.Binary.Permutation.Propositional using () renaming (_↭_ to _↭′_)
+open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; ↭-trans; ↭-sym; refl; prep; swap; trans; ↭-reflexive-≋)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties Eq.setoid using (∈-resp-↭)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties (≡.setoid A) using (map⁺)
 open import Data.List.Relation.Unary.Any using (Any)
 open import Data.List.Sort dto using (sort; sort-↭; sort-↗)
 open import Relation.Nullary.Decidable.Core using (yes; no)
-open Fin
-open _↭_
+open ℕ
 open Any
 open List
 open Linked
@@ -110,29 +113,43 @@ insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) w
           x₁≤x = head-≤ s-xs x∈xs
 ... | no x≰x₀ = Eq.refl ∷ insert-remove s-xs x∈xs
 
-apply : {xs ys : List A} {x : A} → xs ↭ ys → x ∈ xs → x ∈ ys
-apply refl x-in-xs = x-in-xs
-apply (prep x xs↭ys) (here px) = here px
-apply (prep x xs↭ys) (there x-in-xs) = there (apply xs↭ys x-in-xs)
-apply (swap x y xs↭ys) (here px) = there (here px)
-apply (swap x y xs↭ys) (there (here px)) = here px
-apply (swap x y xs↭ys) (there (there x-in-xs)) = there (there (apply xs↭ys x-in-xs))
-apply (trans xs↭ys ys↭zs) x-in-xs = apply ys↭zs (apply xs↭ys x-in-xs)
+open import Data.List.Base using (length)
+open import Function.Base using (_∘_; flip; id)
+open import Data.List.Relation.Binary.Permutation.Propositional using (↭⇒↭ₛ)
+
+∈-resp-≋ : {xs ys : List A} {x : A} → xs ≋ ys → x ∈ xs → x ∈ ys
+∈-resp-≋ = Any-resp-≋ (flip Eq.trans)
+
+≋-remove
+    : {xs ys : List A}
+      {x : A}
+    → (xs≋ys : xs ≋ ys)
+    → (x∈xs : x ∈ xs)
+    → let x∈ys = ∈-resp-≋ xs≋ys x∈xs in
+      remove xs x∈xs ≋ remove ys x∈ys
+≋-remove (x≈y ∷ xs≋ys) (here px) = xs≋ys
+≋-remove (x≈y ∷ xs≋ys) (there x∈xs) = x≈y ∷ ≋-remove xs≋ys x∈xs
 
 ↭-remove
     : {xs ys : List A}
       {x : A}
     → (xs↭ys : xs ↭ ys)
     → (x∈xs : x ∈ xs)
-    → let x∈ys = apply xs↭ys x∈xs in
+    → let x∈ys = ∈-resp-↭ xs↭ys x∈xs in
       remove xs x∈xs ↭ remove ys x∈ys
-↭-remove refl x∈xs = refl
+↭-remove (refl xs≋ys) x∈xs = ↭-reflexive-≋ (≋-remove xs≋ys x∈xs)
 ↭-remove (prep x xs↭ys) (here px) = xs↭ys
 ↭-remove (prep x xs↭ys) (there x∈xs) = prep x (↭-remove xs↭ys x∈xs)
 ↭-remove (swap x y xs↭ys) (here px) = prep y xs↭ys
 ↭-remove (swap x y xs↭ys) (there (here px)) = prep x xs↭ys
 ↭-remove (swap x y xs↭ys) (there (there x∈xs)) = swap x y (↭-remove xs↭ys x∈xs)
-↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (apply xs↭ys x∈xs))
+↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (∈-resp-↭ xs↭ys x∈xs))
+
+↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys
+↭-length (refl xs≋ys)    = ≋-length xs≋ys
+↭-length (prep x lr)     = ≡.cong suc (↭-length lr)
+↭-length (swap x y lr)   = ≡.cong (suc ∘ suc) (↭-length lr)
+↭-length (trans lr₁ lr₂) = ≡.trans (↭-length lr₁) (↭-length lr₂)
 
 sorted-unique
     : {xs ys : List A}
@@ -147,7 +164,7 @@ sorted-unique xs@{x ∷ xs′} {ys} xs↭ys s-xs s-ys = ≋-trans ≋xs (≋-tra
     x∈xs : x ∈ xs
     x∈xs = here Eq.refl
     x∈ys : x ∈ ys
-    x∈ys = apply xs↭ys x∈xs
+    x∈ys = ∈-resp-↭ xs↭ys x∈xs
     s-xs′ : Sorted (remove xs x∈xs)
     s-xs′ = remove-sorted s-xs x∈xs
     s-ys′ : Sorted (remove ys x∈ys)
@@ -170,7 +187,10 @@ sorted-≋
 sorted-≋ {xs} {ys} xs↭ys =
     sorted-unique
       (↭-trans
-        (sort-↭ xs)
-        (↭-trans xs↭ys (↭-sym (sort-↭ ys))))
+        (⇒↭ (sort-↭ xs))
+        (↭-trans xs↭ys (↭-sym (⇒↭ (sort-↭ ys)))))
       (sort-↗ xs)
       (sort-↗ ys)
+  where
+    ⇒↭ : {xs ys : List A} → xs ↭′ ys → xs ↭ ys
+    ⇒↭ = map Eq.reflexive ∘ ↭⇒↭ₛ
-- 
cgit v1.2.3