From d2ce2675b5e0331b6bf5647a4fc195e458d9b5ee Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 30 Oct 2025 19:23:31 -0500 Subject: Add Circ functor --- Data/Hypergraph/Edge.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'Data/Hypergraph/Edge.agda') diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index 7d0fa7c..ee32393 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -25,8 +25,7 @@ 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.Binary using (Setoid; DecTotalOrder; StrictTotalOrder; IsEquivalence) open import Relation.Nullary using (¬_) @@ -89,7 +88,6 @@ 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 @@ -345,3 +343,6 @@ open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) publ module Sort {v} = ListSort (decTotalOrder {v}) open Sort using (sort) public + +Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ +Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} } -- cgit v1.2.3