diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-15 13:31:13 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-15 13:31:13 -0500 |
| commit | 21aa7526f51030be9ffd86be2eabd5d07f64b6f4 (patch) | |
| tree | f9765e3af0909cfd3f404dd70159902e1f852ad4 /Data/Hypergraph/Edge.agda | |
| parent | e5ef6bd45cd5fc77e14bea3d2d57b4fc789e6431 (diff) | |
Strengthen permutation sort theorem
Diffstat (limited to 'Data/Hypergraph/Edge.agda')
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 14 |
1 files changed, 9 insertions, 5 deletions
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ˡ-≈ |