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

Discrete reflexive graphs

module _
  (l1 l2 : Level)
  where

  Discrete-Reflexive-Graph : UU (lsuc l1  lsuc l2)
  Discrete-Reflexive-Graph =
    Σ (Reflexive-Graph l1 l2) is-discrete-Reflexive-Graph

The standard discrete reflexive graph

module _
  {l1 : Level} (A : UU l1)
  where

  discrete-Reflexive-Graph : Reflexive-Graph l1 l1
  pr1 (pr1 discrete-Reflexive-Graph) = A
  pr2 (pr1 discrete-Reflexive-Graph) = Id
  pr2 discrete-Reflexive-Graph x = refl

  is-discrete-discrete-Reflexive-Graph :
    is-discrete-Reflexive-Graph discrete-Reflexive-Graph
  is-discrete-discrete-Reflexive-Graph =
    is-torsorial-Id

  standard-Discrete-Reflexive-Graph :
    Discrete-Reflexive-Graph l1 l1
  pr1 standard-Discrete-Reflexive-Graph = discrete-Reflexive-Graph
  pr2 standard-Discrete-Reflexive-Graph = is-discrete-discrete-Reflexive-Graph

See also

Recent changes