Use permutation for equivalence of hypergraphs

1 files changed, 0 insertions, 59 deletions

diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda
deleted file mode 100644
index d9cc024..0000000
--- a/Data/Hypergraph/Setoid.agda
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level; _⊔_)
-open import Data.Hypergraph.Label using (HypergraphLabel)
-
-module Data.Hypergraph.Setoid {c ℓ : Level} (HL : HypergraphLabel) where
-
-import Data.List.Relation.Binary.Permutation.Propositional as List-↭
-
-open import Data.Hypergraph.Edge HL using (module Sort)
-open import Data.Hypergraph.Base {c} HL using (Hypergraph; normalize)
-open import Data.Nat using (ℕ)
-open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-
--- an equivalence relation on hypergraphs
-record _≈_ {v : ℕ} (H H′ : Hypergraph v) : Set (c ⊔ ℓ) where
-
-  constructor mk≈
-
-  module H = Hypergraph H
-  module H′ = Hypergraph H′
-
-  field
-    ≡-normalized : normalize H ≡ normalize H′
-
-  open Hypergraph using (edges)
-
-  ≡-edges : edges (normalize H) ≡ edges (normalize H′)
-  ≡-edges = ≡.cong edges ≡-normalized
-
-  open List-↭ using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
-  open Sort using (sort-↭)
-
-  ↭-edges : H.edges ↭ H′.edges
-  ↭-edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡-edges) (sort-↭ H′.edges))
-
-infixr 4 _≈_
-
-≈-refl : {v : ℕ} {H : Hypergraph v} → H ≈ H
-≈-refl = mk≈ ≡.refl
-
-≈-sym : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H
-≈-sym (mk≈ ≡n) = mk≈ (≡.sym ≡n)
-
-≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″
-≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (≡.trans ≡n₁ ≡n₂)
-
--- The setoid of labeled hypergraphs with v nodes
-Hypergraphₛ : ℕ → Setoid c (c ⊔ ℓ)
-Hypergraphₛ v = record
-    { Carrier = Hypergraph v
-    ; _≈_ = _≈_
-    ; isEquivalence = record
-        { refl = ≈-refl
-        ; sym = ≈-sym
-        ; trans = ≈-trans
-        }
-    }