# Counting the elements of decidable subtypes

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-02-10.

module univalent-combinatorics.counting-decidable-subtypes where

open import foundation.decidable-subtypes public

Imports
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


## Properties

### The elements of a decidable subtype of a type equipped with a counting can be counted

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-Σ-coprod
( 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-coprod
( 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-Σ-coprod
( Fin k)
( unit)
( λ x → is-in-decidable-subtype P (map-equiv e x)))
( count-equiv'
( right-unit-law-coprod-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))))
( λ { (pair 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

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

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

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

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)))