Acyclic undirected graphs

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-03.
Last modified on 2023-05-13.

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

open import graph-theory.geometric-realizations-undirected-graphs
open import graph-theory.reflecting-maps-undirected-graphs
open import graph-theory.undirected-graphs


An acyclic undirected graph is an undirected graph of which the geometric realization is contractible.

The notion of acyclic graphs is a generalization of the notion of undirected trees. Note that in this library, an undirected tree is an undirected graph in which the type of trails between any two points is contractible. The type of nodes of such undirected trees consequently has decidable equality. On the other hand, there are acyclic undirected graphs that are not undirected trees in this sense. One way to obtain them is via acyclic types, which are types of which the suspension is contractible. The undirected suspension diagram of such types is an acyclic graph. Furthermore, any directed tree induces an acyclic undirected graph by forgetting the directions of the edges.


Acyclic undirected graphs

The following is a preliminary definition that requires us to parametrize over an extra universe level. This will not be necessary anymore if we constructed a geometric realization of every undirected graph. Once we did that, we would simply say that the geometric realization of G is contractible.

is-acyclic-Undirected-Graph :
  {l1 l2 : Level} (l : Level) (G : Undirected-Graph l1 l2) 
  UU (l1  l2  lsuc l)
is-acyclic-Undirected-Graph l G =
  is-geometric-realization-reflecting-map-Undirected-Graph l G
    ( terminal-reflecting-map-Undirected-Graph G)

Recent changes