Hypergraphs
module graph-theory.hypergraphs where
Imports
open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation.unordered-tuples
Idea
A k
-hypergraph consists of a type V
of vertices and a family E
of types
indexed by the unordered k
-tuples of vertices.
Definition
Hypergraph : (l1 l2 : Level) (k : ℕ) → UU (lsuc l1 ⊔ lsuc l2) Hypergraph l1 l2 k = Σ (UU l1) (λ V → unordered-tuple k V → UU l2) module _ {l1 l2 : Level} {k : ℕ} (G : Hypergraph l1 l2 k) where vertex-Hypergraph : UU l1 vertex-Hypergraph = pr1 G unordered-tuple-vertices-Hypergraph : UU (lsuc lzero ⊔ l1) unordered-tuple-vertices-Hypergraph = unordered-tuple k vertex-Hypergraph simplex-Hypergraph : unordered-tuple-vertices-Hypergraph → UU l2 simplex-Hypergraph = pr2 G