Correcting an incorrect definition of discrete relations and discrete…

… graphs (#1222)

This PR corrects an incorrect definition.

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.

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

src/foundation/discrete-binary-relations.lagda.md

@@ -0,0 +1,66 @@
+# Discrete binary relations
+
+```agda
+module foundation.discrete-binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.empty-types
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## 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)

src/foundation/discrete-relations.lagda.md → 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
 ```
 
 <details><summary>Imports</summary>
@@ -22,41 +22,22 @@ 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).
 ```
 
 ## 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)

src/foundation/functional-correspondences.lagda.md

@@ -14,25 +14,27 @@ 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
 
 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
 ```
 
 </details>
 
 ## 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) →

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.

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