# Discrete relations

Content created by Fredrik Bakke.

Created on 2024-04-11.

module foundation.discrete-relations where

Imports
open import foundation.binary-relations
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.reflexive-relations
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.propositions


## Idea

A relation R on A is said to be discrete if, for every element x : A, the type family R x is torsorial. In other words, the dependent sum Σ (y : A), (R x y) is contractible for every x. The standard discrete relation on a type X is the relation defined by identifications,

  R x y := (x ＝ y).


## 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 → 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

module _
{l1 l2 : Level} {A : UU l1} (R : Reflexive-Relation l2 A)
where

is-discrete-prop-Reflexive-Relation : Prop (l1 ⊔ l2)
is-discrete-prop-Reflexive-Relation =
is-discrete-prop-Relation (rel-Reflexive-Relation R)

is-discrete-Reflexive-Relation : UU (l1 ⊔ l2)
is-discrete-Reflexive-Relation =
type-Prop is-discrete-prop-Reflexive-Relation

is-prop-is-discrete-Reflexive-Relation :
is-prop is-discrete-Reflexive-Relation
is-prop-is-discrete-Reflexive-Relation =
is-prop-type-Prop is-discrete-prop-Reflexive-Relation


### The standard discrete relation on a type

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

is-discrete-Id-Relation : is-discrete-Relation (Id {A = A})
is-discrete-Id-Relation = is-torsorial-Id