Decidable relations on types

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

Created on 2022-06-23.
Last modified on 2023-09-11.

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

open import foundation-core.decidable-propositions
open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.propositions


A decidable (binary) relation on X is a binary relation R on X such that each R x y is a decidable proposition.


Decidable relations

is-decidable-Relation-Prop :
  {l1 l2 : Level} {A : UU l1}  Relation-Prop l2 A  UU (l1  l2)
is-decidable-Relation-Prop {A = A} R =
  (x y : A)  is-decidable ( type-Relation-Prop R x y)

Decidable-Relation : {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
Decidable-Relation l2 X = X  X  Decidable-Prop l2

module _
  {l1 l2 : Level} {X : UU l1} (R : Decidable-Relation l2 X)

  relation-Decidable-Relation : X  X  Prop l2
  relation-Decidable-Relation x y = prop-Decidable-Prop (R x y)

  rel-Decidable-Relation : X  X  UU l2
  rel-Decidable-Relation x y = type-Decidable-Prop (R x y)

  is-prop-rel-Decidable-Relation :
    (x y : X)  is-prop (rel-Decidable-Relation x y)
  is-prop-rel-Decidable-Relation x y = is-prop-type-Decidable-Prop (R x y)

  is-decidable-Decidable-Relation :
    (x y : X)  is-decidable (rel-Decidable-Relation x y)
  is-decidable-Decidable-Relation x y =
    is-decidable-Decidable-Prop (R x y)

map-inv-equiv-relation-is-decidable-Decidable-Relation :
  {l1 l2 : Level} {X : UU l1} 
  Σ ( Relation-Prop l2 X)  R  is-decidable-Relation-Prop R) 
  Decidable-Relation l2 X
map-inv-equiv-relation-is-decidable-Decidable-Relation (R , d) x y =
  ( ( type-Relation-Prop R x y) ,
    ( is-prop-type-Relation-Prop R x y) ,
    ( d x y))

equiv-relation-is-decidable-Decidable-Relation :
  {l1 l2 : Level} {X : UU l1} 
  Decidable-Relation l2 X 
  Σ ( Relation-Prop l2 X)  R  is-decidable-Relation-Prop R)
pr1 equiv-relation-is-decidable-Decidable-Relation dec-R =
  ( relation-Decidable-Relation dec-R ,
    is-decidable-Decidable-Relation dec-R)
pr2 equiv-relation-is-decidable-Decidable-Relation =
    ( map-inv-equiv-relation-is-decidable-Decidable-Relation)
    ( refl-htpy)
    ( refl-htpy)

Recent changes