Finite graphs

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

Created on 2022-02-10.
Last modified on 2023-09-06.

module graph-theory.finite-graphs where
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.homotopies
open import foundation.universe-levels
open import foundation.unordered-pairs

open import graph-theory.undirected-graphs

open import univalent-combinatorics.finite-types


A finite undirected graph consists of a finite set of vertices and a family of finite types of edges indexed by unordered pairs of vertices.


Finite undirected graphs

Undirected-Graph-𝔽 : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Undirected-Graph-𝔽 l1 l2 = Σ (𝔽 l1)  X  unordered-pair (type-𝔽 X)  𝔽 l2)

module _
  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)

  vertex-Undirected-Graph-𝔽 : UU l1
  vertex-Undirected-Graph-𝔽 = type-𝔽 (pr1 G)

  unordered-pair-vertices-Undirected-Graph-𝔽 : UU (lsuc lzero  l1)
  unordered-pair-vertices-Undirected-Graph-𝔽 =
    unordered-pair vertex-Undirected-Graph-𝔽

  is-finite-vertex-Undirected-Graph-𝔽 : is-finite vertex-Undirected-Graph-𝔽
  is-finite-vertex-Undirected-Graph-𝔽 = is-finite-type-𝔽 (pr1 G)

  edge-Undirected-Graph-𝔽 :
    (p : unordered-pair-vertices-Undirected-Graph-𝔽)  UU l2
  edge-Undirected-Graph-𝔽 p = type-𝔽 (pr2 G p)

  is-finite-edge-Undirected-Graph-𝔽 :
    (p : unordered-pair-vertices-Undirected-Graph-𝔽) 
    is-finite (edge-Undirected-Graph-𝔽 p)
  is-finite-edge-Undirected-Graph-𝔽 p = is-finite-type-𝔽 (pr2 G p)

  total-edge-Undirected-Graph-𝔽 : UU (lsuc lzero  l1  l2)
  total-edge-Undirected-Graph-𝔽 =
    Σ unordered-pair-vertices-Undirected-Graph-𝔽 edge-Undirected-Graph-𝔽

  undirected-graph-Undirected-Graph-𝔽 : Undirected-Graph l1 l2
  pr1 undirected-graph-Undirected-Graph-𝔽 = vertex-Undirected-Graph-𝔽
  pr2 undirected-graph-Undirected-Graph-𝔽 = edge-Undirected-Graph-𝔽

The following type is expected to be equivalent to Undirected-Graph-𝔽

Undirected-Graph-𝔽' : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Undirected-Graph-𝔽' l1 l2 =
  Σ ( 𝔽 l1)
    ( λ V 
      Σ ( type-𝔽 V  type-𝔽 V  𝔽 l2)
        ( λ E 
          Σ ( (x y : type-𝔽 V)  type-𝔽 (E x y)  type-𝔽 (E y x))
            ( λ σ 
              (x y : type-𝔽 V)  map-equiv ((σ y x) ∘e (σ x y)) ~ id)))

The degree of a vertex x of a graph G is the set of occurences of x as an endpoint of x. Note that the unordered pair {x,x} adds two elements to the degree of x.

incident-edges-vertex-Undirected-Graph-𝔽 :
  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
  (x : vertex-Undirected-Graph-𝔽 G)  UU (lsuc lzero  l1)
incident-edges-vertex-Undirected-Graph-𝔽 G x =
  Σ ( unordered-pair (vertex-Undirected-Graph-𝔽 G))
    ( λ p  fiber (element-unordered-pair p) x)

Recent changes