Decidable relations on types

module foundation.decidable-relations where
Imports
open import foundation.binary-relations
open import foundation.decidable-types

open import foundation-core.decidable-propositions
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.universe-levels

Idea

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

Definitions

Decidable relations

is-decidable-Rel-Prop :
  {l1 l2 : Level} {A : UU l1}  Rel-Prop l2 A  UU (l1  l2)
is-decidable-Rel-Prop {A = A} R =
  (x y : A)  is-decidable ( type-Rel-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)
  where

  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} 
  Σ ( Rel-Prop l2 X)  R  is-decidable-Rel-Prop R) 
  Decidable-Relation l2 X
map-inv-equiv-relation-is-decidable-Decidable-Relation (R , d) x y =
  ( ( type-Rel-Prop R x y) ,
    ( is-prop-type-Rel-Prop R x y) ,
    ( d x y))

equiv-relation-is-decidable-Decidable-Relation :
  {l1 l2 : Level} {X : UU l1} 
  Decidable-Relation l2 X 
  Σ ( Rel-Prop l2 X)  R  is-decidable-Rel-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 =
  is-equiv-has-inverse
    ( map-inv-equiv-relation-is-decidable-Decidable-Relation)
    ( refl-htpy)
    ( refl-htpy)