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/Hypergraph/Edge.agda | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

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

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