# Decidable subtypes

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-02-15.

module foundation.decidable-subtypes where

Imports
open import foundation.1-types
open import foundation.coproduct-types
open import foundation.decidable-embeddings
open import foundation.decidable-maps
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositional-maps
open import foundation.sets
open import foundation.structured-type-duality
open import foundation.subtypes
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.transport-along-identifications
open import foundation-core.truncated-types
open import foundation-core.truncation-levels


## Idea

A decidable subtype of a type consists of a family of decidable propositions over it.

## Definitions

### Decidable subtypes

is-decidable-subtype-Prop :
{l1 l2 : Level} {A : UU l1} → subtype l2 A → Prop (l1 ⊔ l2)
is-decidable-subtype-Prop {A = A} P =
Π-Prop A (λ a → is-decidable-Prop (P a))

is-decidable-subtype : {l1 l2 : Level} {A : UU l1} → subtype l2 A → UU (l1 ⊔ l2)
is-decidable-subtype P = type-Prop (is-decidable-subtype-Prop P)

is-prop-is-decidable-subtype :
{l1 l2 : Level} {A : UU l1} (P : subtype l2 A) →
is-prop (is-decidable-subtype P)
is-prop-is-decidable-subtype P = is-prop-type-Prop (is-decidable-subtype-Prop P)

decidable-subtype : {l1 : Level} (l : Level) (X : UU l1) → UU (l1 ⊔ lsuc l)
decidable-subtype l X = X → Decidable-Prop l


### The underlying subtype of a decidable subtype

module _
{l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A)
where

subtype-decidable-subtype : subtype l2 A
subtype-decidable-subtype a = prop-Decidable-Prop (P a)

is-decidable-decidable-subtype :
is-decidable-subtype subtype-decidable-subtype
is-decidable-decidable-subtype a =
is-decidable-Decidable-Prop (P a)

is-in-decidable-subtype : A → UU l2
is-in-decidable-subtype = is-in-subtype subtype-decidable-subtype

is-prop-is-in-decidable-subtype :
(a : A) → is-prop (is-in-decidable-subtype a)
is-prop-is-in-decidable-subtype =
is-prop-is-in-subtype subtype-decidable-subtype


### The underlying type of a decidable subtype

module _
{l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A)
where

type-decidable-subtype : UU (l1 ⊔ l2)
type-decidable-subtype = type-subtype (subtype-decidable-subtype P)

inclusion-decidable-subtype : type-decidable-subtype → A
inclusion-decidable-subtype = inclusion-subtype (subtype-decidable-subtype P)

is-emb-inclusion-decidable-subtype : is-emb inclusion-decidable-subtype
is-emb-inclusion-decidable-subtype =
is-emb-inclusion-subtype (subtype-decidable-subtype P)

is-decidable-map-inclusion-decidable-subtype :
is-decidable-map inclusion-decidable-subtype
is-decidable-map-inclusion-decidable-subtype x =
is-decidable-equiv
( equiv-fiber-pr1 (type-Decidable-Prop ∘ P) x)
( is-decidable-Decidable-Prop (P x))

is-injective-inclusion-decidable-subtype :
is-injective inclusion-decidable-subtype
is-injective-inclusion-decidable-subtype =
is-injective-inclusion-subtype (subtype-decidable-subtype P)

emb-decidable-subtype : type-decidable-subtype ↪ A
emb-decidable-subtype = emb-subtype (subtype-decidable-subtype P)

is-decidable-emb-inclusion-decidable-subtype :
is-decidable-emb inclusion-decidable-subtype
is-decidable-emb-inclusion-decidable-subtype =
( is-emb-inclusion-decidable-subtype ,
is-decidable-map-inclusion-decidable-subtype)

decidable-emb-decidable-subtype : type-decidable-subtype ↪ᵈ A
decidable-emb-decidable-subtype =
( inclusion-decidable-subtype ,
is-decidable-emb-inclusion-decidable-subtype)


### The decidable subtype associated to a decidable embedding

module _
{l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X ↪ᵈ Y)
where

decidable-subtype-decidable-emb : decidable-subtype (l1 ⊔ l2) Y
pr1 (decidable-subtype-decidable-emb y) =
fiber (map-decidable-emb f) y
pr2 (decidable-subtype-decidable-emb y) =
is-decidable-prop-map-is-decidable-emb
( is-decidable-emb-map-decidable-emb f)
( y)

compute-type-decidable-type-decidable-emb :
type-decidable-subtype decidable-subtype-decidable-emb ≃ X
compute-type-decidable-type-decidable-emb =
equiv-total-fiber (map-decidable-emb f)

inv-compute-type-decidable-type-decidable-emb :
X ≃ type-decidable-subtype decidable-subtype-decidable-emb
inv-compute-type-decidable-type-decidable-emb =
inv-equiv-total-fiber (map-decidable-emb f)


## Examples

### The decidable subtypes of left and right elements in a coproduct type

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

is-decidable-is-left : (x : A + B) → is-decidable (is-left x)
is-decidable-is-left (inl x) = is-decidable-unit
is-decidable-is-left (inr x) = is-decidable-empty

is-left-Decidable-Prop : A + B → Decidable-Prop lzero
pr1 (is-left-Decidable-Prop x) = is-left x
pr1 (pr2 (is-left-Decidable-Prop x)) = is-prop-is-left x
pr2 (pr2 (is-left-Decidable-Prop x)) = is-decidable-is-left x

is-decidable-is-right : (x : A + B) → is-decidable (is-right x)
is-decidable-is-right (inl x) = is-decidable-empty
is-decidable-is-right (inr x) = is-decidable-unit

is-right-Decidable-Prop : A + B → Decidable-Prop lzero
pr1 (is-right-Decidable-Prop x) = is-right x
pr1 (pr2 (is-right-Decidable-Prop x)) = is-prop-is-right x
pr2 (pr2 (is-right-Decidable-Prop x)) = is-decidable-is-right x


## Properties

### Types of decidable subtypes of any universe level are equivalent

module _
{l1 : Level} (X : UU l1)
where

equiv-universes-decidable-subtype :
(l l' : Level) → decidable-subtype l X ≃ decidable-subtype l' X
equiv-universes-decidable-subtype l l' =
equiv-Π
( λ _ → Decidable-Prop l')
( id-equiv)
( λ _ → equiv-universes-Decidable-Prop l l')

iff-universes-decidable-subtype :
(l l' : Level) (S : decidable-subtype l X) →
( (x : X) →
type-Decidable-Prop (S x) ↔
type-Decidable-Prop
( map-equiv (equiv-universes-decidable-subtype l l') S x))
iff-universes-decidable-subtype l l' S x =
tr
( λ P → type-Decidable-Prop (S x) ↔ type-Decidable-Prop P)
( inv
( compute-map-equiv-Π
( λ _ → Decidable-Prop l')
( id-equiv)
( λ _ → equiv-universes-Decidable-Prop l l')
( S)
( x)))
( iff-universes-Decidable-Prop l l' (S x))


### A decidable subtype of a k+1-truncated type is k+1-truncated

module _
{l1 l2 : Level} (k : 𝕋) {A : UU l1} (P : decidable-subtype l2 A)
where

abstract
is-trunc-type-decidable-subtype :
is-trunc (succ-𝕋 k) A → is-trunc (succ-𝕋 k) (type-decidable-subtype P)
is-trunc-type-decidable-subtype =
is-trunc-type-subtype k (subtype-decidable-subtype P)

module _
{l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A)
where

abstract
is-prop-type-decidable-subtype :
is-prop A → is-prop (type-decidable-subtype P)
is-prop-type-decidable-subtype =
is-prop-type-subtype (subtype-decidable-subtype P)

abstract
is-set-type-decidable-subtype : is-set A → is-set (type-decidable-subtype P)
is-set-type-decidable-subtype =
is-set-type-subtype (subtype-decidable-subtype P)

abstract
is-1-type-type-decidable-subtype :
is-1-type A → is-1-type (type-decidable-subtype P)
is-1-type-type-decidable-subtype =
is-1-type-type-subtype (subtype-decidable-subtype P)

prop-decidable-subprop :
{l1 l2 : Level} (A : Prop l1) (P : decidable-subtype l2 (type-Prop A)) →
Prop (l1 ⊔ l2)
prop-decidable-subprop A P = prop-subprop A (subtype-decidable-subtype P)

set-decidable-subset :
{l1 l2 : Level} (A : Set l1) (P : decidable-subtype l2 (type-Set A)) →
Set (l1 ⊔ l2)
set-decidable-subset A P = set-subset A (subtype-decidable-subtype P)


### The type of decidable subtypes of a type is a set

is-set-decidable-subtype :
{l1 l2 : Level} {X : UU l1} → is-set (decidable-subtype l2 X)
is-set-decidable-subtype =
is-set-function-type is-set-Decidable-Prop


### Extensionality of the type of decidable subtypes

module _
{l1 l2 : Level} {A : UU l1} (P : decidable-subtype l2 A)
where

has-same-elements-decidable-subtype :
{l3 : Level} → decidable-subtype l3 A → UU (l1 ⊔ l2 ⊔ l3)
has-same-elements-decidable-subtype Q =
has-same-elements-subtype
( subtype-decidable-subtype P)
( subtype-decidable-subtype Q)

extensionality-decidable-subtype :
(Q : decidable-subtype l2 A) →
(P ＝ Q) ≃ has-same-elements-decidable-subtype Q
extensionality-decidable-subtype =
extensionality-Π P
( λ x Q → (type-Decidable-Prop (P x)) ↔ (type-Decidable-Prop Q))
( λ x Q → extensionality-Decidable-Prop (P x) Q)

has-same-elements-eq-decidable-subtype :
(Q : decidable-subtype l2 A) →
(P ＝ Q) → has-same-elements-decidable-subtype Q
has-same-elements-eq-decidable-subtype Q =
map-equiv (extensionality-decidable-subtype Q)

eq-has-same-elements-decidable-subtype :
(Q : decidable-subtype l2 A) →
has-same-elements-decidable-subtype Q → P ＝ Q
eq-has-same-elements-decidable-subtype Q =
map-inv-equiv (extensionality-decidable-subtype Q)

refl-extensionality-decidable-subtype :
map-equiv (extensionality-decidable-subtype P) refl ＝ (λ x → pair id id)
refl-extensionality-decidable-subtype = refl


### The type of decidable subtypes of A is equivalent to the type of all decidable embeddings into a type A

equiv-Fiber-Decidable-Prop :
(l : Level) {l1 : Level} (A : UU l1) →
Σ (UU (l1 ⊔ l)) (λ X → X ↪ᵈ A) ≃ (decidable-subtype (l1 ⊔ l) A)
equiv-Fiber-Decidable-Prop l A =
( equiv-Fiber-structure l is-decidable-prop A) ∘e
( equiv-tot
( λ X →
equiv-tot
( λ f →
( inv-distributive-Π-Σ) ∘e
( equiv-product-left (equiv-is-prop-map-is-emb f)))))