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(-)

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