Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2022-07-15.
Last modified on 2023-11-09.

module graph-theory.hypergraphs where
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.universe-levels
open import foundation.unordered-tuples


A k-hypergraph consists of a type V of vertices and a family E of types indexed by the unordered k-tuples of vertices.


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)

  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

Recent changes