This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

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