Discrete reflexive relations

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-08-26.
Last modified on 2024-11-19.

module foundation.discrete-reflexive-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 reflexive 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 reflexive relation on a type X is the relation defined by identifications,

  R x y := (x ＝ y).

Definitions

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 =
    Π-Prop A (λ a → is-torsorial-Prop (rel-Reflexive-Relation R a))

  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

Properties

The identity relation is discrete

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

  is-discrete-Id-Reflexive-Relation :
    is-discrete-Reflexive-Relation (Id-Reflexive-Relation A)
  is-discrete-Id-Reflexive-Relation = is-torsorial-Id

See also

Recent changes