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

Complete undirected graphs

module graph-theory.complete-undirected-graphs where
Imports 
open import foundation.universe-levels

open import graph-theory.complete-multipartite-graphs
open import graph-theory.finite-graphs

open import univalent-combinatorics.finite-types

Idea

A complete undirected graph is a complete multipartite graph in which every block has exactly one vertex. In other words, it is an undirected graph in which every vertex is connected to every other vertex.

There are many ways of presenting complete undirected graphs. For example, the type of edges in a complete undirected graph is a 2-element subtype of the type of its vertices.

Definition

complete-Undirected-Graph-𝔽 : {l : Level} → 𝔽 l → Undirected-Graph-𝔽 l l
complete-Undirected-Graph-𝔽 X =
  complete-multipartite-Undirected-Graph-𝔽 X (λ x → unit-𝔽)