Discrete binary relations

Content created by Egbert Rijke.

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

module foundation.discrete-binary-relations where
Imports 
open import foundation.binary-relations
open import foundation.empty-types
open import foundation.propositions
open import foundation.universe-levels

Idea

A binary relation R on A is said to be discrete 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 is a left adjoint to the forgetful functor (V , E) ↦ (V , ∅).

The condition of discreteness of binary relations compares to the condition of discreteness of reflexive relations 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 and hence it is an identity system.

Note: It is also possible to impose the torsoriality condition on an arbitrary binary relation. However, this leads to the concept of functional correspondence. 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

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

Recent changes