Reflexive relations

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Julian KG, fernabnor and louismntnu.

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

module foundation.reflexive-relations where
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.identity-types


A reflexive relation on a type A is a type-valued binary relation R : A → A → 𝒰 equipped with a proof r : (x : A) → R x x.


Reflexive relations

Reflexive-Relation :
  {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
Reflexive-Relation l2 A = Σ (Relation l2 A)  R  is-reflexive R)

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

  rel-Reflexive-Relation : Relation l2 A
  rel-Reflexive-Relation = pr1 R

  is-reflexive-Reflexive-Relation : is-reflexive rel-Reflexive-Relation
  is-reflexive-Reflexive-Relation = pr2 R

The identity reflexive relation on a type

Id-Reflexive-Relation : {l : Level} (A : UU l)  Reflexive-Relation l A
Id-Reflexive-Relation A = (Id ,  x  refl))

Recent changes