Decidable subtypes of finite types

module univalent-combinatorics.decidable-subtypes where
Imports
open import foundation.decidable-subtypes public

open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-propositions
open import foundation.embeddings
open import foundation.functions
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import univalent-combinatorics.decidable-dependent-pair-types
open import univalent-combinatorics.dependent-pair-types
open import univalent-combinatorics.equality-finite-types
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.function-types

Definitions

Finite subsets of a finite set

subset-𝔽 : {l1 : Level} (l2 : Level)  𝔽 l1  UU (l1  lsuc l2)
subset-𝔽 l2 X = decidable-subtype l2 (type-𝔽 X)

module _
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X)
  where

  subtype-subset-𝔽 : subtype l2 (type-𝔽 X)
  subtype-subset-𝔽 = subtype-decidable-subtype P

  is-decidable-subset-𝔽 : is-decidable-subtype subtype-subset-𝔽
  is-decidable-subset-𝔽 =
    is-decidable-decidable-subtype P

  is-in-subset-𝔽 : type-𝔽 X  UU l2
  is-in-subset-𝔽 = is-in-decidable-subtype P

  is-prop-is-in-subset-𝔽 :
    (x : type-𝔽 X)  is-prop (is-in-subset-𝔽 x)
  is-prop-is-in-subset-𝔽 = is-prop-is-in-decidable-subtype P

The underlying type of a decidable subtype

module _
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X)
  where

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

  inclusion-subset-𝔽 : type-subset-𝔽  type-𝔽 X
  inclusion-subset-𝔽 = inclusion-decidable-subtype P

  is-emb-inclusion-subset-𝔽 : is-emb inclusion-subset-𝔽
  is-emb-inclusion-subset-𝔽 = is-emb-inclusion-decidable-subtype P

  is-injective-inclusion-subset-𝔽 : is-injective inclusion-subset-𝔽
  is-injective-inclusion-subset-𝔽 =
    is-injective-inclusion-decidable-subtype P

  emb-subset-𝔽 : type-subset-𝔽  type-𝔽 X
  emb-subset-𝔽 = emb-decidable-subtype P

Properties

The type of decidable subtypes of a finite type is finite

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

Subset-𝔽 :
  {l1 : Level} (l2 : Level)  𝔽 l1  𝔽 (l1  lsuc l2)
pr1 (Subset-𝔽 l2 X) = subset-𝔽 l2 X
pr2 (Subset-𝔽 l2 X) = is-finite-decidable-subtype-is-finite (is-finite-type-𝔽 X)

The type of decidable subsets of a finite type has decidable equality

has-decidable-equality-Subset-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1) 
  has-decidable-equality (decidable-subtype l2 (type-𝔽 X))
has-decidable-equality-Subset-𝔽 {l1} {l2} X =
  has-decidable-equality-is-finite
    ( is-finite-decidable-subtype-is-finite (is-finite-type-𝔽 X))

Decidable subtypes of finite types are finite

is-finite-type-decidable-subtype :
  {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) 
    is-finite X  is-finite (type-decidable-subtype P)
is-finite-type-decidable-subtype P H =
  is-finite-Σ H
    ( λ x 
      is-finite-is-decidable-Prop
        ( prop-Decidable-Prop (P x))
        ( is-decidable-Decidable-Prop (P x)))

is-finite-type-subset-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X) 
  is-finite (type-subset-𝔽 X P)
is-finite-type-subset-𝔽 X P =
  is-finite-type-decidable-subtype P (is-finite-type-𝔽 X)

finite-type-subset-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1)  subset-𝔽 l2 X  𝔽 (l1  l2)
pr1 (finite-type-subset-𝔽 X P) = type-subset-𝔽 X P
pr2 (finite-type-subset-𝔽 X P) = is-finite-type-subset-𝔽 X P

The underlying type of a decidable subtype has decidable equality

has-decidable-equality-type-decidable-subtype-is-finite :
  {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X)  is-finite X 
  has-decidable-equality (type-decidable-subtype P)
has-decidable-equality-type-decidable-subtype-is-finite P H =
  has-decidable-equality-is-finite (is-finite-type-decidable-subtype P H)

has-decidable-equality-type-subset-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X) 
  has-decidable-equality (type-subset-𝔽 X P)
has-decidable-equality-type-subset-𝔽 X P =
  has-decidable-equality-is-finite (is-finite-type-subset-𝔽 X P)

The underlying type of a decidable subtype of a finite type is a set

is-set-type-subset-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X)  is-set (type-subset-𝔽 X P)
is-set-type-subset-𝔽 X P = is-set-type-decidable-subtype P (is-set-type-𝔽 X)

set-subset-𝔽 :
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X)  Set (l1  l2)
set-subset-𝔽 X P = set-decidable-subset (set-𝔽 X) P

The number of elements of a decidable subtype of a finite type is smaller than the number of elements of the ambient type

module _
  {l1 l2 : Level} (X : 𝔽 l1) (P : subset-𝔽 l2 X)
  where

  number-of-elements-subset-𝔽 : 
  number-of-elements-subset-𝔽 = number-of-elements-𝔽 (finite-type-subset-𝔽 X P)

A subtype S over a type A with decidable equalities such that the underlying type generated by S is finite is a decidable subtype

is-decidable-subtype-is-finite-has-decidable-eq :
  {l1 l2 : Level}  {A : UU l1}  (S : subtype l2 A) 
  has-decidable-equality A  is-finite (type-subtype S) 
  is-decidable-subtype S
is-decidable-subtype-is-finite-has-decidable-eq S dec-A fin-S a =
  apply-universal-property-trunc-Prop
    ( fin-S)
    ( is-decidable-Prop (S a))
    ( λ count-S 
      ind-coprod
        ( λ _  type-Prop (is-decidable-Prop (S a)))
        ( λ x  inl (tr (type-Prop  S) (inv (pr2 x)) (pr2 (pr1 x))))
        ( λ x  inr λ S-a  x (( (a , S-a) , refl)))
        ( is-decidable-Σ-count count-S λ s  dec-A a (pr1 s)))