# Decidable subtypes of finite types ```agda module univalent-combinatorics.decidable-subtypes where open import foundation.decidable-subtypes public ``` <details><summary>Imports</summary> ```agda 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.function-types 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.transport-along-identifications 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 ``` </details> ## Definitions ### Finite subsets of a finite set ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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 → rec-coproduct ( λ 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))) ```