diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-30 19:23:31 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-30 19:23:31 -0500 |
| commit | d2ce2675b5e0331b6bf5647a4fc195e458d9b5ee (patch) | |
| tree | acf00b930c01778fc520ffe99fd046615cf2f3a5 /Data/Hypergraph.agda | |
| parent | e90c54ce55d36019d32e239509ff5f96c5dff2b3 (diff) | |
Add Circ functormain
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 |