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-12-03.

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

open import foundation-core.identity-types

Idea

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.

Definitions

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)
  where

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

  refl-Reflexive-Relation : is-reflexive rel-Reflexive-Relation
  refl-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))

Properties

A formulation of the dependent action on identifications of reflexivity

Consider a reflexive relation R on a type A with reflexivity r : (x : A) → R x x, and consider an identification p : x ＝ y in A. The usual action on identifications yields a dependent identification

  tr (λ u → R u u) p (r x) ＝ (r y).

However, since R is a binary indexed family of types, there is also the binary dependent identity type, which can be used to express another version of the action on identifications of the reflexivity element r:

  binary-dependent-identification R p p (r x) (r y).

This action on identifications can be seen as an instance of a dependent function over the diagonal map Δ : A → A × A, a situation wich can be generalized. At the time of writing, however, the library lacks infrastructure for the general formulation of the action on identifications of dependent functions over functions yielding binary dependent identifications.

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

  binary-dependent-identification-refl-Reflexive-Relation :
    {x y : A} (p : x ＝ y) →
    binary-dependent-identification
      ( rel-Reflexive-Relation R)
      ( p)
      ( p)
      ( refl-Reflexive-Relation R x)
      ( refl-Reflexive-Relation R y)
  binary-dependent-identification-refl-Reflexive-Relation refl = refl

Recent changes