Decidability Properties
Table of Contents
1 Decidability properties
module Lib.Prop.Decidability where
This file contains the proof of some properties on decidability.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Lib.Data.Decidability import Lib.Prop.Proposition
1.2 Closure under equivalence
If A and B are equivalent, then whenever one of them is decidable, the other is also decidable.
is-decidable/closed-Equiv (A B : U) (e : Equiv A B) : is-decidable B → is-decidable A = split inl y → inl (Equiv/inv-map A B e y) inr f → inr (λy. f (Equiv/map A B e y)) is-decidable/closed-Equiv' (A B : U) (e : Equiv A B) : is-decidable A → is-decidable B = split inl x → inl (Equiv/map A B e x) inr f → inr (λx. f (Equiv/inv-map A B e x))
1.3 is-decidable is a proposition
Whenever A is a proposition, is-decidable A is a proposition.
is-decidable/is-prop/inl (A : U) (is-prop-A : is-prop A) (a : A) : (d : Coprod A (neg A)) → Path (Coprod A (neg A)) (inl a) d = split inl x → Coprod/Eq/map A (neg A) (inl a) (inl x) (is-prop-A a x) inr f → ex-falso (Path (Coprod A (neg A)) (inl a) (inr f)) (f a) is-decidable/is-prop/inr (A : U) (is-prop-A : is-prop A) (f : neg A) : (d : Coprod A (neg A)) → Path (Coprod A (neg A)) (inr f) d = split inl a → ex-falso (Path (Coprod A (neg A)) (inr f) (inl a)) (f a) inr g → Coprod/Eq/map A (neg A) (inr f) (inr g) (is-prop/pi A (λ_. Empty) (λ_. Empty/is-prop) f g) is-decidable/is-prop (A : U) (is-prop-A : is-prop A) : is-prop (is-decidable A) = split inl a → is-decidable/is-prop/inl A is-prop-A a inr f → is-decidable/is-prop/inr A is-prop-A f is-decidable/Prop (A : U) (is-prop-A : is-prop A) : UU-Prop = ( is-decidable A, is-decidable/is-prop A is-prop-A)
The same holds for decidable equality.
has-decidable-equality/is-prop (A : U) (H : (x y : A) → is-prop (Path A x y)) : is-prop (has-decidable-equality A) = is-prop/pi-2 A ( λ_. A) ( λx y. is-decidable (Path A x y)) ( λx y. is-decidable/is-prop ( Path A x y) ( H x y)) has-decidable-equality/Prop (A : U) (H : (x y : A) → is-prop (Path A x y)) : UU-Prop = ( has-decidable-equality A, has-decidable-equality/is-prop A H)
1.4 is-contr is decidable whenever the underlying type is a decidable proposition
is-contr/is-decidable (A : UU-Prop) : is-decidable (Prop/type A) → is-decidable (is-contr (Prop/type A)) = split inl a → inl (a, Prop/is-prop A a) inr f → inr (λc. f c.1)