diff options
Diffstat (limited to 'Data/Hypergraph.agda')
| -rw-r--r-- | Data/Hypergraph.agda | 27 |
1 files changed, 25 insertions, 2 deletions
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda index 2e8498c..18a259b 100644 --- a/Data/Hypergraph.agda +++ b/Data/Hypergraph.agda @@ -6,9 +6,32 @@ open import Data.Hypergraph.Label using (HypergraphLabel) module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where +import Data.List.Relation.Binary.Pointwise as PW +import Data.Hypergraph.Edge HL as HypergraphEdge +import Function.Reasoning as →-Reasoning +import Relation.Binary.PropositionalEquality as ≡ + open import Data.Hypergraph.Base {c} HL public open import Data.Hypergraph.Setoid {c} {ℓ} HL public - -import Data.Hypergraph.Edge HL as HypergraphEdge +open import Data.Nat using (ℕ) +open import Function using (_∘_; _⟶ₛ_; Func) +open import Level using (0ℓ) +open import Relation.Binary using (Setoid) module Edge = HypergraphEdge + +open Edge using (Edgeₛ; ≈-Edge⇒≡) +open Func + +List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ +List∘Edgeₛ = PW.setoid ∘ Edgeₛ + +mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n +mkHypergraphₛ .to = mkHypergraph +mkHypergraphₛ {n} .cong ≋-edges = ≋-edges + |> PW.map ≈-Edge⇒≡ + |> PW.Pointwise-≡⇒≡ + |> ≡.cong mkHypergraph + |> Setoid.reflexive (Hypergraphₛ n) + where + open →-Reasoning |