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
- 2024-12-03. Egbert Rijke. Hofmann-Streicher universes for graphs and globular types (#1196).
- 2024-11-19. Egbert Rijke. Correcting an incorrect definition of discrete relations and discrete graphs (#1222).