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/Label.agda | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 Data/Hypergraph/Label.agda

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

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