# Counting the elements of decidable subtypes ```agda module univalent-combinatorics.counting-decidable-subtypes where open import foundation.decidable-subtypes public ``` <details><summary>Imports</summary> ```agda open import elementary-number-theory.natural-numbers open import foundation.contractible-types open import foundation.coproduct-types open import foundation.decidable-embeddings open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.propositional-maps open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.type-arithmetic-coproduct-types open import foundation.type-arithmetic-empty-type open import foundation.unit-type open import foundation.universe-levels open import univalent-combinatorics.counting open import univalent-combinatorics.decidable-propositions open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types ``` </details> ## Properties ### The elements of a decidable subtype of a type equipped with a counting can be counted ```agda abstract count-decidable-subtype' : {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) → (k : ℕ) (e : Fin k ≃ X) → count (type-decidable-subtype P) count-decidable-subtype' P zero-ℕ e = count-is-empty ( is-empty-is-zero-number-of-elements-count (pair zero-ℕ e) refl ∘ pr1) count-decidable-subtype' P (succ-ℕ k) e with is-decidable-decidable-subtype P (map-equiv e (inr star)) ... | inl p = count-equiv ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv)) ( count-equiv' ( right-distributive-Σ-coproduct ( Fin k) ( unit) ( λ x → is-in-decidable-subtype P (map-equiv e x))) ( pair ( succ-ℕ ( number-of-elements-count ( count-decidable-subtype' ( λ x → P (map-equiv e (inl x))) ( k) ( id-equiv)))) ( equiv-coproduct ( equiv-count ( count-decidable-subtype' ( λ x → P (map-equiv e (inl x))) ( k) ( id-equiv))) ( equiv-is-contr ( is-contr-unit) ( is-contr-Σ ( is-contr-unit) ( star) ( is-proof-irrelevant-is-prop ( is-prop-is-in-decidable-subtype P ( map-equiv e (inr star))) ( p))))))) ... | inr f = count-equiv ( equiv-Σ (is-in-decidable-subtype P) e (λ x → id-equiv)) ( count-equiv' ( right-distributive-Σ-coproduct ( Fin k) ( unit) ( λ x → is-in-decidable-subtype P (map-equiv e x))) ( count-equiv' ( right-unit-law-coproduct-is-empty ( Σ ( Fin k) ( λ x → is-in-decidable-subtype P (map-equiv e (inl x)))) ( Σ ( unit) ( λ x → is-in-decidable-subtype P (map-equiv e (inr x)))) ( λ where (star , p) → f p)) ( count-decidable-subtype' ( λ x → P (map-equiv e (inl x))) ( k) ( id-equiv)))) count-decidable-subtype : {l1 l2 : Level} {X : UU l1} (P : decidable-subtype l2 X) → (count X) → count (type-decidable-subtype P) count-decidable-subtype P e = count-decidable-subtype' P ( number-of-elements-count e) ( equiv-count e) ``` ### The elements in the domain of a decidable embedding can be counted if the elements of the codomain can be counted ```agda count-decidable-emb : {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X ↪ᵈ Y) → count Y → count X count-decidable-emb f e = count-equiv ( equiv-total-fiber (map-decidable-emb f)) ( count-decidable-subtype (decidable-subtype-decidable-emb f) e) ``` ### If the elements of a subtype of a type equipped with a counting can be counted, then the subtype is decidable ```agda is-decidable-count-subtype : {l1 l2 : Level} {X : UU l1} (P : subtype l2 X) → count X → count (type-subtype P) → (x : X) → is-decidable (type-Prop (P x)) is-decidable-count-subtype P e f x = is-decidable-count ( count-equiv ( equiv-fiber-pr1 (type-Prop ∘ P) x) ( count-decidable-subtype ( λ y → pair ( Id (pr1 y) x) ( pair ( is-set-count e (pr1 y) x) ( has-decidable-equality-count e (pr1 y) x))) ( f))) ``` ### If a subtype of a type equipped with a counting is finite, then its elements can be counted ```agda count-type-subtype-is-finite-type-subtype : {l1 l2 : Level} {A : UU l1} (e : count A) (P : subtype l2 A) → is-finite (type-subtype P) → count (type-subtype P) count-type-subtype-is-finite-type-subtype {l1} {l2} {A} e P f = count-decidable-subtype ( λ x → pair (type-Prop (P x)) (pair (is-prop-type-Prop (P x)) (d x))) ( e) where d : (x : A) → is-decidable (type-Prop (P x)) d x = apply-universal-property-trunc-Prop f ( is-decidable-Prop (P x)) ( λ g → is-decidable-count-subtype P e g x) ``` ### For any embedding `B ↪ A` into a type `A` equipped with a counting, if `B` is finite then its elements can be counted ```agda count-domain-emb-is-finite-domain-emb : {l1 l2 : Level} {A : UU l1} (e : count A) {B : UU l2} (f : B ↪ A) → is-finite B → count B count-domain-emb-is-finite-domain-emb e f H = count-equiv ( equiv-total-fiber (map-emb f)) ( count-type-subtype-is-finite-type-subtype e ( λ x → pair (fiber (map-emb f) x) (is-prop-map-emb f x)) ( is-finite-equiv' ( equiv-total-fiber (map-emb f)) ( H))) ```