Acyclic undirected graphs

module graph-theory.acyclic-undirected-graphs where
Imports
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

Idea

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.

Definition

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)