Discrete reflexive relations
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-08-26.
Last modified on 2023-06-08.
module foundation.discrete-reflexive-relations where
Imports
open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.reflexive-relations open import foundation.universe-levels open import foundation-core.identity-types open import foundation-core.propositions
Idea
A reflexive relation R
on a type A
is said to be discrete if for every
x : A
the type Σ A (R x)
is contractible. The (standard) discrete reflexive
relation on a type is its identity type.
Definitions
Discrete reflexive relations
is-discrete-Reflexive-Relation-Prop : {l1 l2 : Level} {A : UU l1} (R : Reflexive-Relation l2 A) → Prop (l1 ⊔ l2) is-discrete-Reflexive-Relation-Prop {A = A} R = Π-Prop A (λ x → is-contr-Prop (Σ A (rel-Reflexive-Relation R x))) is-discrete-Reflexive-Relation : {l1 l2 : Level} {A : UU l1} (R : Reflexive-Relation l2 A) → UU (l1 ⊔ l2) is-discrete-Reflexive-Relation R = type-Prop (is-discrete-Reflexive-Relation-Prop R)
The standard discrete reflexive relation
Δ-Reflexive-Relation : {l1 : Level} (A : UU l1) → Reflexive-Relation l1 A pr1 (Δ-Reflexive-Relation A) = Id pr2 (Δ-Reflexive-Relation A) x = refl
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).