Discrete reflexive graphs

Content created by Egbert Rijke.

Created on 2024-11-19.
Last modified on 2024-12-03.

module graph-theory.discrete-reflexive-graphs where

Imports

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.discrete-reflexive-relations
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.torsorial-type-families

open import graph-theory.directed-graphs
open import graph-theory.reflexive-graphs

Idea

A reflexive graph G ≐ (V , E , r) is said to be discrete^¶ if, for every vertex x : V, the type family of edges with source x, E x, is torsorial. In other words, if the dependent sum Σ (y : V), (E x y) is contractible for every x. The standard discrete graph^¶ associated to a type X is the reflexive graph whose vertices are elements of X, and edges are identifications,

  E x y := (x ＝ y).

For any type A there is a standard discrete reflexive graph^¶ Δ A, which is defined by

  (Δ A)₀ := A
  (Δ A)₁ := Id A
  refl (Δ A) := refl

Since torsorial type families are identity systems, it follows that a reflexive graph is discrete precisely when its edge relation is initial. In other words, the inclusion of the discrete reflexive graphs into the reflexive graphs satisfies the universal property of being left adjoint to the forgetful functor G ↦ Δ G₀, mapping a reflexive graph to the standard discrete graph on its type of vertices.

Definitions

The predicate on reflexive graphs of being discrete

module _
  {l1 l2 : Level} (G : Reflexive-Graph l1 l2)
  where

  is-discrete-prop-Reflexive-Graph : Prop (l1 ⊔ l2)
  is-discrete-prop-Reflexive-Graph =
    is-discrete-prop-Reflexive-Relation
      ( edge-reflexive-relation-Reflexive-Graph G)

  is-discrete-Reflexive-Graph : UU (l1 ⊔ l2)
  is-discrete-Reflexive-Graph =
    type-Prop is-discrete-prop-Reflexive-Graph

  is-prop-is-discrete-Reflexive-Graph : is-prop is-discrete-Reflexive-Graph
  is-prop-is-discrete-Reflexive-Graph =
    is-prop-type-Prop is-discrete-prop-Reflexive-Graph