From 76c5d87e9a6c8cd22ef867ca5991e2502b8134dd Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Tue, 19 Nov 2024 12:30:30 -0500 Subject: [PATCH] Correcting an incorrect definition of discrete relations and discrete graphs (#1222) This PR corrects an incorrect definition. --- .../torsorial-type-families.lagda.md | 4 +- src/foundation.lagda.md | 3 +- .../discrete-binary-relations.lagda.md | 66 +++++++ ... => discrete-reflexive-relations.lagda.md} | 52 +++--- .../functional-correspondences.lagda.md | 16 +- .../torsorial-type-families.lagda.md | 4 +- src/graph-theory.lagda.md | 3 +- .../discrete-directed-graphs.lagda.md | 171 ++++++++++++++++++ src/graph-theory/discrete-graphs.lagda.md | 78 -------- .../discrete-reflexive-graphs.lagda.md | 120 ++++++++++++ src/graph-theory/reflexive-graphs.lagda.md | 6 + 11 files changed, 401 insertions(+), 122 deletions(-) create mode 100644 src/foundation/discrete-binary-relations.lagda.md rename src/foundation/{discrete-relations.lagda.md => discrete-reflexive-relations.lagda.md} (54%) create mode 100644 src/graph-theory/discrete-directed-graphs.lagda.md delete mode 100644 src/graph-theory/discrete-graphs.lagda.md create mode 100644 src/graph-theory/discrete-reflexive-graphs.lagda.md diff --git a/src/foundation-core/torsorial-type-families.lagda.md b/src/foundation-core/torsorial-type-families.lagda.md index 35882429c6..e2dfd083f2 100644 --- a/src/foundation-core/torsorial-type-families.lagda.md +++ b/src/foundation-core/torsorial-type-families.lagda.md @@ -99,5 +99,5 @@ module _ ### See also -- [Discrete relations](foundation.discrete-relations.md) are binary torsorial - type families. +- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) are + binary torsorial type families. diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index dbf4204531..3c7bfe2497 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -130,7 +130,8 @@ open import foundation.diagonal-maps-of-types public open import foundation.diagonal-span-diagrams public open import foundation.diagonals-of-maps public open import foundation.diagonals-of-morphisms-arrows public -open import foundation.discrete-relations public +open import foundation.discrete-binary-relations public +open import foundation.discrete-reflexive-relations public open import foundation.discrete-relaxed-sigma-decompositions public open import foundation.discrete-sigma-decompositions public open import foundation.discrete-types public diff --git a/src/foundation/discrete-binary-relations.lagda.md b/src/foundation/discrete-binary-relations.lagda.md new file mode 100644 index 0000000000..9edf7ffd3f --- /dev/null +++ b/src/foundation/discrete-binary-relations.lagda.md @@ -0,0 +1,66 @@ +# Discrete binary relations + +```agda +module foundation.discrete-binary-relations where +``` + +
Imports + +```agda +open import foundation.binary-relations +open import foundation.empty-types +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +A [binary relation](foundation.binary-relations.md) `R` on `A` is said to be +{{#concept "discrete" Disambiguation="binary relation" Agda=is-discrete-Relation}} +if it does not relate any elements, i.e., if the type `R x y` is empty for all +`x y : A`. In other words, a binary relation is discrete if and only if it is +the initial binary relation. This definition ensures that the inclusion of +[discrete directed graphs](graph-theory.discrete-directed-graphs.md) is a left +adjoint to the forgetful functor `(V , E) ↦ (V , ∅)`. + +The condition of discreteness of binary relations compares to the condition of +[discreteness](foundation.discrete-reflexive-relations.md) of +[reflexive relations](foundation.reflexive-relations.md) in the sense that both +conditions imply initiality. A discrete binary relation is initial becauase it +is empty, while a discrete reflexive relation is initial because it is +[torsorial](foundation-core.torsorial-type-families.md) and hence it is an +[identity system](foundation.identity-systems.md). + +**Note:** It is also possible to impose the torsoriality condition on an +arbitrary binary relation. However, this leads to the concept of +[functional correspondence](foundation.functional-correspondences.md). That is, +a binary relation `R` on `A` such that `R x` is torsorial for every `x : A` is +the graph of a function. + +## Definitions + +### The predicate on relations of being discrete + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (R : Relation l2 A) + where + + is-discrete-prop-Relation : Prop (l1 ⊔ l2) + is-discrete-prop-Relation = + Π-Prop A (λ x → Π-Prop A (λ y → is-empty-Prop (R x y))) + + is-discrete-Relation : UU (l1 ⊔ l2) + is-discrete-Relation = type-Prop is-discrete-prop-Relation + + is-prop-is-discrete-Relation : is-prop is-discrete-Relation + is-prop-is-discrete-Relation = is-prop-type-Prop is-discrete-prop-Relation +``` + +## See also + +- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) +- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md) +- [Discrete-reflexive graphs](graph-theory.discrete-reflexive-graphs.md) diff --git a/src/foundation/discrete-relations.lagda.md b/src/foundation/discrete-reflexive-relations.lagda.md similarity index 54% rename from src/foundation/discrete-relations.lagda.md rename to src/foundation/discrete-reflexive-relations.lagda.md index 1a6535940b..236e380874 100644 --- a/src/foundation/discrete-relations.lagda.md +++ b/src/foundation/discrete-reflexive-relations.lagda.md @@ -1,7 +1,7 @@ -# Discrete relations +# Discrete reflexive relations ```agda -module foundation.discrete-relations where +module foundation.discrete-reflexive-relations where ```
Imports @@ -22,15 +22,15 @@ open import foundation-core.propositions ## Idea -A [relation](foundation.binary-relations.md) `R` on `A` is said to be -{{#concept "discrete" Disambiguation="binary relations valued in types" Agda=is-discrete-Relation}} +A [reflexive relation](foundation.binary-relations.md) `R` on `A` is said to be +{{#concept "discrete" Disambiguation="reflexive relations valued in types" Agda=is-discrete-Reflexive-Relation}} if, for every element `x : A`, the type family `R x` is [torsorial](foundation-core.torsorial-type-families.md). In other words, the [dependent sum](foundation.dependent-pair-types.md) `Σ (y : A), (R x y)` is -[contractible](foundation-core.contractible-types.md) for every `x`. The -{{#concept "standard discrete relation" Disambiguation="binary relations valued in types"}} -on a type `X` is the relation defined by -[identifications](foundation-core.identity-types.md), +[contractible](foundation-core.contractible-types.md) for every `x`. + +The {{#concept "standard discrete reflexive relation"}} on a type `X` is the +relation defined by [identifications](foundation-core.identity-types.md), ```text R x y := (x ＝ y). @@ -38,25 +38,6 @@ on a type `X` is the relation defined by ## Definitions -### The predicate on relations of being discrete - -```agda -module _ - {l1 l2 : Level} {A : UU l1} (R : Relation l2 A) - where - - is-discrete-prop-Relation : Prop (l1 ⊔ l2) - is-discrete-prop-Relation = Π-Prop A (λ x → is-torsorial-Prop (R x)) - - is-discrete-Relation : UU (l1 ⊔ l2) - is-discrete-Relation = - type-Prop is-discrete-prop-Relation - - is-prop-is-discrete-Relation : is-prop is-discrete-Relation - is-prop-is-discrete-Relation = - is-prop-type-Prop is-discrete-prop-Relation -``` - ### The predicate on reflexive relations of being discrete ```agda @@ -66,7 +47,7 @@ module _ is-discrete-prop-Reflexive-Relation : Prop (l1 ⊔ l2) is-discrete-prop-Reflexive-Relation = - is-discrete-prop-Relation (rel-Reflexive-Relation R) + Π-Prop A (λ a → is-torsorial-Prop (rel-Reflexive-Relation R a)) is-discrete-Reflexive-Relation : UU (l1 ⊔ l2) is-discrete-Reflexive-Relation = @@ -78,13 +59,22 @@ module _ is-prop-type-Prop is-discrete-prop-Reflexive-Relation ``` -### The standard discrete relation on a type +## Properties + +### The identity relation is discrete ```agda module _ {l : Level} (A : UU l) where - is-discrete-Id-Relation : is-discrete-Relation (Id {A = A}) - is-discrete-Id-Relation = is-torsorial-Id + is-discrete-Id-Reflexive-Relation : + is-discrete-Reflexive-Relation (Id-Reflexive-Relation A) + is-discrete-Id-Reflexive-Relation = is-torsorial-Id ``` + +## See also + +- [Discrete binary relations](foundation.discrete-binary-relations.md) +- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md) +- [Discrete reflexive graphs](graph-theory.discrete-reflexive-graphs.md) diff --git a/src/foundation/functional-correspondences.lagda.md b/src/foundation/functional-correspondences.lagda.md index a615239cd0..ed5998a661 100644 --- a/src/foundation/functional-correspondences.lagda.md +++ b/src/foundation/functional-correspondences.lagda.md @@ -14,6 +14,7 @@ open import foundation.equality-dependent-function-types open import foundation.function-extensionality open import foundation.fundamental-theorem-of-identity-types open import foundation.subtype-identity-principle +open import foundation.torsorial-type-families open import foundation.univalence open import foundation.universe-levels @@ -21,18 +22,19 @@ open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes -open import foundation-core.torsorial-type-families ```
## Idea -A functional dependent correspondence is a dependent binary correspondence -`C : Π (a : A) → B a → 𝒰` from a type `A` to a type family `B` over `A` such -that for every `a : A` the type `Σ (b : B a), C a b` is contractible. The type -of dependent functions from `A` to `B` is equivalent to the type of functional -dependent correspondences. +A +{{#concept "functional (dependent) correspondence" Agda=is-functional-correspondence}} +is a dependent binary correspondence `C : Π (a : A) → B a → 𝒰` from a type `A` +to a type family `B` over `A` such that for every `a : A` the type family +`C a : B a → Type` is [torsorial](foundation-core.torsorial-type-families.md). +The type of dependent functions from `A` to `B` is equivalent to the type of +functional dependent correspondences. ## Definition @@ -41,7 +43,7 @@ is-functional-correspondence-Prop : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) → Prop (l1 ⊔ l2 ⊔ l3) is-functional-correspondence-Prop {A = A} {B} C = - Π-Prop A (λ x → is-contr-Prop (Σ (B x) (C x))) + Π-Prop A (λ x → is-torsorial-Prop (C x)) is-functional-correspondence : {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (a : A) → B a → UU l3) → diff --git a/src/foundation/torsorial-type-families.lagda.md b/src/foundation/torsorial-type-families.lagda.md index db72746fb4..0929568e83 100644 --- a/src/foundation/torsorial-type-families.lagda.md +++ b/src/foundation/torsorial-type-families.lagda.md @@ -113,5 +113,5 @@ module _ ### See also -- [Discrete relations](foundation.discrete-relations.md) are binary torsorial - type families. +- [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) are + binary torsorial type families. diff --git a/src/graph-theory.lagda.md b/src/graph-theory.lagda.md index 9ac8fd5589..4355ecf1c8 100644 --- a/src/graph-theory.lagda.md +++ b/src/graph-theory.lagda.md @@ -15,7 +15,8 @@ open import graph-theory.connected-undirected-graphs public open import graph-theory.cycles-undirected-graphs public open import graph-theory.directed-graph-structures-on-standard-finite-sets public open import graph-theory.directed-graphs public -open import graph-theory.discrete-graphs public +open import graph-theory.discrete-directed-graphs public +open import graph-theory.discrete-reflexive-graphs public open import graph-theory.displayed-large-reflexive-graphs public open import graph-theory.edge-coloured-undirected-graphs public open import graph-theory.embeddings-directed-graphs public diff --git a/src/graph-theory/discrete-directed-graphs.lagda.md b/src/graph-theory/discrete-directed-graphs.lagda.md new file mode 100644 index 0000000000..c3ff8a436b --- /dev/null +++ b/src/graph-theory/discrete-directed-graphs.lagda.md @@ -0,0 +1,171 @@ +# Discrete directed graphs + +```agda +module graph-theory.discrete-directed-graphs where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.discrete-binary-relations +open import foundation.empty-types +open import foundation.equivalences +open import foundation.homotopies +open import foundation.retractions +open import foundation.sections +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.morphisms-directed-graphs +open import graph-theory.reflexive-graphs +``` + +
+ +## Idea + +A [directed graph](graph-theory.directed-graphs.md) `G ≐ (V , E)` is said to be +{{#concept "discrete" Disambiguation="directed graph" Agda=is-discrete-Directed-Graph}} +if it has no edges. In other words, a directed graph is discrete if it is of the +form `Δ A`, where `Δ` is the left adjoint to the forgetful functor `(V , E) ↦ V` +from directed graphs to types. + +Recall that [reflexive graphs](graph-theory.reflexive-graphs.md) are said to be +discrete if the edge relation is +[torsorial](foundation-core.torsorial-type-families.md). The condition that a +directed graph is discrete compares to the condition that a reflexive graph is +discrete in the sense that in both cases discreteness implies initiality of the +edge relation: The empty relation is the initial relation, while the identity +relation is the initial reflexive relation. + +One may wonder if the torsoriality condition of discreteness shouldn't directly +carry over to the discreteness condition on directed graphs. Indeed, an earlier +implementation of discreteness in agda-unimath had this faulty definition. +However, this leads to examples that are not typically considered discrete. +Consider, for example, the directed graph with `V := ℕ` the +[natural numbers](elementary-number-theory.natural-numbers.md) and +`E m n := (m + 1 ＝ n)` as in + +```text + 0 ---> 1 ---> 2 ---> ⋯. +``` + +This directed graph satisfies the condition that the type family `E m` is +torsorial for every `m : ℕ`, simply because `E` is a +[functional correspondence](foundation.functional-correspondences.md). However, +this graph is not considered discrete since it relates distinct vertices. + +## Definitions + +### The predicate on graphs of being discrete + +```agda +module _ + {l1 l2 : Level} (G : Directed-Graph l1 l2) + where + + is-discrete-prop-Directed-Graph : Prop (l1 ⊔ l2) + is-discrete-prop-Directed-Graph = + is-discrete-prop-Relation (edge-Directed-Graph G) + + is-discrete-Directed-Graph : UU (l1 ⊔ l2) + is-discrete-Directed-Graph = + is-discrete-Relation (edge-Directed-Graph G) + + is-prop-is-discrete-Directed-Graph : + is-prop is-discrete-Directed-Graph + is-prop-is-discrete-Directed-Graph = + is-prop-is-discrete-Relation (edge-Directed-Graph G) +``` + +### The standard discrete directed graph + +```agda +module _ + {l : Level} (A : UU l) + where + + discrete-Directed-Graph : Directed-Graph l lzero + pr1 discrete-Directed-Graph = A + pr2 discrete-Directed-Graph x y = empty +``` + +## Properties + +### Morphisms from a standard discrete directed graph are maps into vertices + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} (G : Directed-Graph l1 l2) + where + + ev-hom-discrete-Directed-Graph : + hom-Directed-Graph (discrete-Directed-Graph A) G → + A → vertex-Directed-Graph G + ev-hom-discrete-Directed-Graph = + vertex-hom-Directed-Graph (discrete-Directed-Graph _) G + + map-inv-ev-hom-discrete-Directed-Graph : + (A → vertex-Directed-Graph G) → + hom-Directed-Graph (discrete-Directed-Graph A) G + pr1 (map-inv-ev-hom-discrete-Directed-Graph f) = f + pr2 (map-inv-ev-hom-discrete-Directed-Graph f) x y () + + is-section-map-inv-ev-hom-discrete-Directed-Graph : + is-section + ( ev-hom-discrete-Directed-Graph) + ( map-inv-ev-hom-discrete-Directed-Graph) + is-section-map-inv-ev-hom-discrete-Directed-Graph f = refl + + htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph : + (f : hom-Directed-Graph (discrete-Directed-Graph A) G) → + htpy-hom-Directed-Graph + ( discrete-Directed-Graph A) + ( G) + ( map-inv-ev-hom-discrete-Directed-Graph + ( ev-hom-discrete-Directed-Graph f)) + ( f) + pr1 (htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) = + refl-htpy + pr2 (htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) x y () + + is-retraction-map-inv-ev-hom-discrete-Directed-Graph : + is-retraction + ( ev-hom-discrete-Directed-Graph) + ( map-inv-ev-hom-discrete-Directed-Graph) + is-retraction-map-inv-ev-hom-discrete-Directed-Graph f = + eq-htpy-hom-Directed-Graph + ( discrete-Directed-Graph A) + ( G) + ( map-inv-ev-hom-discrete-Directed-Graph + ( ev-hom-discrete-Directed-Graph f)) + ( f) + ( htpy-is-retraction-map-inv-ev-hom-discrete-Directed-Graph f) + + abstract + is-equiv-ev-hom-discrete-Directed-Graph : + is-equiv ev-hom-discrete-Directed-Graph + is-equiv-ev-hom-discrete-Directed-Graph = + is-equiv-is-invertible + map-inv-ev-hom-discrete-Directed-Graph + is-section-map-inv-ev-hom-discrete-Directed-Graph + is-retraction-map-inv-ev-hom-discrete-Directed-Graph + + ev-equiv-hom-discrete-Directed-Graph : + hom-Directed-Graph (discrete-Directed-Graph A) G ≃ + (A → vertex-Directed-Graph G) + pr1 ev-equiv-hom-discrete-Directed-Graph = + ev-hom-discrete-Directed-Graph + pr2 ev-equiv-hom-discrete-Directed-Graph = + is-equiv-ev-hom-discrete-Directed-Graph +``` + +## See also + +- [Discrete reflexive graphs](graph-theory.discrete-reflexive-graphs.md) diff --git a/src/graph-theory/discrete-graphs.lagda.md b/src/graph-theory/discrete-graphs.lagda.md deleted file mode 100644 index 4e5a0b8a2a..0000000000 --- a/src/graph-theory/discrete-graphs.lagda.md +++ /dev/null @@ -1,78 +0,0 @@ -# Discrete graphs - -```agda -module graph-theory.discrete-graphs where -``` - -
Imports - -```agda -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.discrete-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 [directed graph](graph-theory.directed-graphs.md) `G ≐ (V , E)` is said to be -{{#concept "discrete" Disambiguation="graph" Agda=is-discrete-Graph}} if, for -every vertex `x : V`, the type family of edges with source `x`, `E x`, is -[torsorial](foundation-core.torsorial-type-families.md). In other words, if the -[dependent sum](foundation.dependent-pair-types.md) `Σ (y : V), (E x y)` is -[contractible](foundation-core.contractible-types.md) for every `x`. The -{{#concept "standard discrete graph"}} associated to a type `X` is the graph -whose vertices are elements of `X`, and edges are -[identifications](foundation-core.identity-types.md), - -```text - E x y := (x ＝ y). -``` - -## Definitions - -### The predicate on graphs of being discrete - -```agda -module _ - {l1 l2 : Level} (G : Directed-Graph l1 l2) - where - - is-discrete-prop-Graph : Prop (l1 ⊔ l2) - is-discrete-prop-Graph = is-discrete-prop-Relation (edge-Directed-Graph G) - - is-discrete-Graph : UU (l1 ⊔ l2) - is-discrete-Graph = type-Prop is-discrete-prop-Graph - - is-prop-is-discrete-Graph : is-prop is-discrete-Graph - is-prop-is-discrete-Graph = is-prop-type-Prop is-discrete-prop-Graph -``` - -### The predicate on reflexive graphs of being discrete - -```agda -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-Graph (graph-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 -``` diff --git a/src/graph-theory/discrete-reflexive-graphs.lagda.md b/src/graph-theory/discrete-reflexive-graphs.lagda.md new file mode 100644 index 0000000000..845ca50851 --- /dev/null +++ b/src/graph-theory/discrete-reflexive-graphs.lagda.md @@ -0,0 +1,120 @@ +# Discrete reflexive graphs + +```agda +module graph-theory.discrete-reflexive-graphs where +``` + +
Imports + +```agda +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](graph-theory.reflexive-graphs.md) `G ≐ (V , E , r)` is said +to be +{{#concept "discrete" Disambiguation="reflexive graph" Agda=is-discrete-Reflexive-Graph}} +if, for every vertex `x : V`, the type family of edges with source `x`, `E x`, +is [torsorial](foundation-core.torsorial-type-families.md). In other words, if +the [dependent sum](foundation.dependent-pair-types.md) `Σ (y : V), (E x y)` is +[contractible](foundation-core.contractible-types.md) for every `x`. The +{{#concept "standard discrete graph"}} associated to a type `X` is the reflexive +graph whose vertices are elements of `X`, and edges are +[identifications](foundation-core.identity-types.md), + +```text + E x y := (x ＝ y). +``` + +For any type `A` there is a +{{#concept "standard discrete reflexive graph" Agda=standard-Discrete-Reflexive-Graph}} +`Δ A`, which is defined by + +```text + (Δ A)₀ := A + (Δ A)₁ := Id A + refl (Δ A) := refl +``` + +Since torsorial type families are +[identity systems](foundation.identity-systems.md), 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 + +```agda +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 + +```agda +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 + +```agda +module _ + {l1 : Level} (A : UU l1) + where + + discrete-Reflexive-Graph : Reflexive-Graph l1 l1 + pr1 discrete-Reflexive-Graph = A + pr1 (pr2 discrete-Reflexive-Graph) = Id + pr2 (pr2 discrete-Reflexive-Graph) a = 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 + +- [Discrete directed graphs](graph-theory.discrete-directed-graphs.md) diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md index 76f15912ae..a64a9e16cf 100644 --- a/src/graph-theory/reflexive-graphs.lagda.md +++ b/src/graph-theory/reflexive-graphs.lagda.md @@ -8,6 +8,7 @@ module graph-theory.reflexive-graphs where ```agda open import foundation.dependent-pair-types +open import foundation.reflexive-relations open import foundation.universe-levels open import graph-theory.directed-graphs @@ -41,6 +42,11 @@ module _ refl-Reflexive-Graph : (x : vertex-Reflexive-Graph) → edge-Reflexive-Graph x x refl-Reflexive-Graph = pr2 (pr2 G) + edge-reflexive-relation-Reflexive-Graph : + Reflexive-Relation l2 vertex-Reflexive-Graph + pr1 edge-reflexive-relation-Reflexive-Graph = edge-Reflexive-Graph + pr2 edge-reflexive-relation-Reflexive-Graph = refl-Reflexive-Graph + graph-Reflexive-Graph : Directed-Graph l1 l2 graph-Reflexive-Graph = vertex-Reflexive-Graph , edge-Reflexive-Graph ```