Countable sets

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elif Uskuplu and Elisabeth Stenholm.

Created on 2022-05-13.
Last modified on 2024-04-11.

module set-theory.countable-sets where
Imports 
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.type-arithmetic-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.decidable-subtypes
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equality-coproduct-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.maybe
open import foundation.negated-equality
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.shifting-sequences
open import foundation.surjective-maps
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types

open import univalent-combinatorics.standard-finite-types

Idea

A set X is said to be countable if there is a surjective map f : ℕ → X + 1. Equivalently, a set X is countable if there is a surjective map f : type-decidable-subset P → X for some decidable subset P of X.

Definition

First definition of countable types

module _
  {l : Level} (X : Set l)
  where

  enumeration : UU l
  enumeration = Σ (ℕ → Maybe (type-Set X)) is-surjective

  map-enumeration : enumeration → (ℕ → Maybe (type-Set X))
  map-enumeration E = pr1 E

  is-surjective-map-enumeration :
    (E : enumeration) → is-surjective (map-enumeration E)
  is-surjective-map-enumeration E = pr2 E

  is-countable-Prop : Prop l
  is-countable-Prop =
    ∃ (ℕ → Maybe (type-Set X)) (is-surjective-Prop)

  is-countable : UU l
  is-countable = type-Prop (is-countable-Prop)

  is-prop-is-countable : is-prop is-countable
  is-prop-is-countable = is-prop-type-Prop is-countable-Prop

Second definition of countable types

module _
  {l : Level} (X : Set l)
  where

  decidable-subprojection-ℕ : UU (lsuc l ⊔ l)
  decidable-subprojection-ℕ =
    Σ ( decidable-subtype l ℕ)
      ( λ P → type-decidable-subtype P ↠ type-Set X)

  is-countable-Prop' : Prop (lsuc l ⊔ l)
  is-countable-Prop' =
    exists-structure-Prop
      ( decidable-subtype l ℕ)
      ( λ P → type-decidable-subtype P ↠ type-Set X)

  is-countable' : UU (lsuc l ⊔ l)
  is-countable' = type-Prop is-countable-Prop'

  is-prop-is-countable' : is-prop is-countable'
  is-prop-is-countable' = is-prop-type-Prop is-countable-Prop'

Third definition of countable types

If a set X is inhabited, then it is countable if and only if there is a surjective map f : ℕ → X. Let us call the latter as "directly countable".

is-directly-countable-Prop : {l : Level} → Set l → Prop l
is-directly-countable-Prop X =
  ∃ (ℕ → type-Set X) (is-surjective-Prop)

is-directly-countable : {l : Level} → Set l → UU l
is-directly-countable X = type-Prop (is-directly-countable-Prop X)

is-prop-is-directly-countable :
  {l : Level} (X : Set l) → is-prop (is-directly-countable X)
is-prop-is-directly-countable X = is-prop-type-Prop
  (is-directly-countable-Prop X)

module _
  {l : Level} (X : Set l) (a : type-Set X)
  where

  is-directly-countable-is-countable :
    is-countable X → is-directly-countable X
  is-directly-countable-is-countable H =
    apply-universal-property-trunc-Prop H
      ( is-directly-countable-Prop X)
      ( λ P →
        unit-trunc-Prop
          ( pair
            ( f ∘ (pr1 P))
            ( is-surjective-comp is-surjective-f (pr2 P))))
    where
    f : Maybe (type-Set X) → type-Set X
    f (inl x) = x
    f (inr star) = a

    is-surjective-f : is-surjective f
    is-surjective-f x = unit-trunc-Prop (pair (inl x) refl)

  abstract
    is-countable-is-directly-countable :
      is-directly-countable X → is-countable X
    is-countable-is-directly-countable H =
      apply-universal-property-trunc-Prop H
        ( is-countable-Prop X)
        ( λ P →
          unit-trunc-Prop
            ( ( λ where
                zero-ℕ → inr star
                (succ-ℕ n) → inl ((shift-ℕ a (pr1 P)) n)) ,
              ( λ where
                ( inl x) →
                  apply-universal-property-trunc-Prop (pr2 P x)
                    ( trunc-Prop (fiber _ (inl x)))
                    ( λ (n , p) →
                      unit-trunc-Prop
                        ( succ-ℕ (succ-ℕ n) , ap inl p))
                ( inr star) → unit-trunc-Prop (zero-ℕ , refl))))

Properties

The two definitions of countability are equivalent

First, we will prove is-countable X → is-countable' X.

module _
  {l : Level} (X : Set l)
  where

  decidable-subprojection-ℕ-enumeration :
    enumeration X → decidable-subprojection-ℕ X
  pr1 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n) =
    f n ≠ inr star
  pr1 (pr2 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n)) =
    is-prop-neg
  pr2 (pr2 (pr1 (decidable-subprojection-ℕ-enumeration (f , H)) n)) =
    is-decidable-is-not-exception-Maybe (f n)
  pr1 (pr2 (decidable-subprojection-ℕ-enumeration (f , H))) (n , p) =
    value-is-not-exception-Maybe (f n) p
  pr2 (pr2 (decidable-subprojection-ℕ-enumeration (f , H))) x =
    apply-universal-property-trunc-Prop (H (inl x))
      ( trunc-Prop (fiber _ x))
      ( λ (n , p) →
        unit-trunc-Prop
          ( ( n , is-not-exception-is-value-Maybe (f n) (x , inv p)) ,
            ( is-injective-inl
              ( ( eq-is-not-exception-Maybe
                ( f n)
                ( is-not-exception-is-value-Maybe
                  ( f n) (x , inv p))) ∙
              ( p)))))

  is-countable'-is-countable :
    is-countable X → is-countable' X
  is-countable'-is-countable H =
    apply-universal-property-trunc-Prop H
      ( is-countable-Prop' X)
      ( λ E → unit-trunc-Prop (decidable-subprojection-ℕ-enumeration E))

Second, we will prove is-countable' X → is-countable X.

cases-map-decidable-subtype-ℕ :
  {l : Level} (X : Set l) →
  ( P : decidable-subtype l ℕ) →
  ( f : type-decidable-subtype P → type-Set X) →
  ( (n : ℕ) → is-decidable (pr1 (P n)) -> Maybe (type-Set X))
cases-map-decidable-subtype-ℕ X P f n (inl x) = inl (f (n , x))
cases-map-decidable-subtype-ℕ X P f n (inr x) = inr star

module _
  {l : Level} (X : Set l)
  ( P : decidable-subtype l ℕ)
  ( f : type-decidable-subtype P → type-Set X)
  where

  shift-decidable-subtype-ℕ : decidable-subtype l ℕ
  shift-decidable-subtype-ℕ zero-ℕ =
    ( raise-empty l) ,
    ( is-prop-raise-empty ,
      ( inr (is-empty-raise-empty)))
  shift-decidable-subtype-ℕ (succ-ℕ n) = P n

  map-shift-decidable-subtype-ℕ :
    type-decidable-subtype shift-decidable-subtype-ℕ → type-Set X
  map-shift-decidable-subtype-ℕ (zero-ℕ , map-raise ())
  map-shift-decidable-subtype-ℕ (succ-ℕ n , p) = f (n , p)

  map-enumeration-decidable-subprojection-ℕ : ℕ → Maybe (type-Set X)
  map-enumeration-decidable-subprojection-ℕ n =
    cases-map-decidable-subtype-ℕ
      ( X)
      ( shift-decidable-subtype-ℕ)
      ( map-shift-decidable-subtype-ℕ)
      ( n)
      (pr2 (pr2 (shift-decidable-subtype-ℕ n)))

  abstract
    is-surjective-map-enumeration-decidable-subprojection-ℕ :
      ( is-surjective f) →
      ( is-surjective map-enumeration-decidable-subprojection-ℕ)
    is-surjective-map-enumeration-decidable-subprojection-ℕ H (inl x) =
      ( apply-universal-property-trunc-Prop (H x)
        ( trunc-Prop (fiber map-enumeration-decidable-subprojection-ℕ (inl x)))
        ( λ where
          ( ( n , s) , refl) →
            unit-trunc-Prop
              ( ( succ-ℕ n) ,
                ( ap
                  ( cases-map-decidable-subtype-ℕ X
                    ( shift-decidable-subtype-ℕ)
                    ( map-shift-decidable-subtype-ℕ)
                    (succ-ℕ n))
                  ( pr1
                    ( is-prop-is-decidable (pr1 (pr2 (P n)))
                      ( pr2 (pr2 (P n)))
                      ( inl s)))))))
    is-surjective-map-enumeration-decidable-subprojection-ℕ H (inr star) =
      ( unit-trunc-Prop (0 , refl))

module _
  {l : Level} (X : Set l)
  where

  enumeration-decidable-subprojection-ℕ :
    decidable-subprojection-ℕ X → enumeration X
  enumeration-decidable-subprojection-ℕ (P , (f , H)) =
    ( map-enumeration-decidable-subprojection-ℕ X P f) ,
    ( is-surjective-map-enumeration-decidable-subprojection-ℕ X P f H)

  is-countable-is-countable' :
    is-countable' X → is-countable X
  is-countable-is-countable' H =
    apply-universal-property-trunc-Prop H
      ( is-countable-Prop X)
      ( λ D →
        ( unit-trunc-Prop (enumeration-decidable-subprojection-ℕ D)))

Useful Lemmas

There is a surjection from (Maybe A + Maybe B) to Maybe (A + B).

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

  map-maybe-coproduct : (Maybe A + Maybe B) → Maybe (A + B)
  map-maybe-coproduct (inl (inl x)) = inl (inl x)
  map-maybe-coproduct (inl (inr star)) = inr star
  map-maybe-coproduct (inr (inl x)) = inl (inr x)
  map-maybe-coproduct (inr (inr star)) = inr star

  is-surjective-map-maybe-coproduct : is-surjective map-maybe-coproduct
  is-surjective-map-maybe-coproduct (inl (inl x)) =
    unit-trunc-Prop ((inl (inl x)) , refl)
  is-surjective-map-maybe-coproduct (inl (inr x)) =
    unit-trunc-Prop ((inr (inl x)) , refl)
  is-surjective-map-maybe-coproduct (inr star) =
    unit-trunc-Prop ((inl (inr star)) , refl)

There is a surjection from (Maybe A × Maybe B) to Maybe (A × B).

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

  map-maybe-product : (Maybe A × Maybe B) → Maybe (A × B)
  map-maybe-product (inl a , inl b) = inl (a , b)
  map-maybe-product (inl a , inr star) = inr star
  map-maybe-product (inr star , inl b) = inr star
  map-maybe-product (inr star , inr star) = inr star

  is-surjective-map-maybe-product : is-surjective map-maybe-product
  is-surjective-map-maybe-product (inl (a , b)) =
    unit-trunc-Prop ((inl a , inl b) , refl)
  is-surjective-map-maybe-product (inr star) =
    unit-trunc-Prop ((inr star , inr star) , refl)

Examples

The set of natural numbers ℕ is itself countable.

abstract
  is-countable-ℕ : is-countable ℕ-Set
  is-countable-ℕ =
    unit-trunc-Prop
      ( ( λ where
          zero-ℕ → inr star
          (succ-ℕ n) → inl n) ,
        ( λ where
          ( inl n) → unit-trunc-Prop (succ-ℕ n , refl)
          ( inr star) → unit-trunc-Prop (zero-ℕ , refl)))

The empty set is countable.

is-countable-empty : is-countable empty-Set
is-countable-empty =
  is-countable-is-countable'
    ( empty-Set)
    ( unit-trunc-Prop ((λ _ → empty-Decidable-Prop) , (λ ()) , (λ ())))

The unit set is countable.

abstract
  is-countable-unit : is-countable unit-Set
  is-countable-unit =
    unit-trunc-Prop
      ( ( λ where
          zero-ℕ → inl star
          (succ-ℕ x) → inr star) ,
        ( λ where
          ( inl star) → unit-trunc-Prop (0 , refl)
          ( inr star) → unit-trunc-Prop (1 , refl)))

If X and Y are countable sets, then so is their coproduct X + Y.

module _
  {l1 l2 : Level} (X : Set l1) (Y : Set l2)
  where

  is-countable-coproduct :
    is-countable X → is-countable Y → is-countable (coproduct-Set X Y)
  is-countable-coproduct H H' =
    apply-twice-universal-property-trunc-Prop H' H
      ( is-countable-Prop (coproduct-Set X Y))
      ( λ h' h →
        ( unit-trunc-Prop
          ( pair
            ( map-maybe-coproduct ∘
              ( map-coproduct (pr1 h) (pr1 h') ∘ map-ℕ-to-ℕ+ℕ))
            ( is-surjective-comp
              ( is-surjective-map-maybe-coproduct)
              ( is-surjective-comp
                ( is-surjective-map-coproduct (pr2 h) (pr2 h'))
                ( is-surjective-is-equiv (is-equiv-map-ℕ-to-ℕ+ℕ)))))))

If X and Y are countable sets, then so is their coproduct X × Y.

module _
  {l1 l2 : Level} (X : Set l1) (Y : Set l2)
  where

  is-countable-product :
    is-countable X → is-countable Y → is-countable (product-Set X Y)
  is-countable-product H H' =
    apply-twice-universal-property-trunc-Prop H' H
      ( is-countable-Prop (product-Set X Y))
      ( λ h' h →
        ( unit-trunc-Prop
          ( pair
            ( map-maybe-product ∘
              ( map-product (pr1 h) (pr1 h') ∘ map-ℕ-to-ℕ×ℕ))
            ( is-surjective-comp
              ( is-surjective-map-maybe-product)
              ( is-surjective-comp
                ( is-surjective-map-product (pr2 h) (pr2 h'))
                ( is-surjective-is-equiv (is-equiv-map-ℕ-to-ℕ×ℕ)))))))

In particular, the sets ℕ + ℕ, ℕ × ℕ, and ℤ are countable.

is-countable-ℕ+ℕ : is-countable (coproduct-Set ℕ-Set ℕ-Set)
is-countable-ℕ+ℕ =
  is-countable-coproduct ℕ-Set ℕ-Set is-countable-ℕ is-countable-ℕ

is-countable-ℕ×ℕ : is-countable (product-Set ℕ-Set ℕ-Set)
is-countable-ℕ×ℕ =
  is-countable-product ℕ-Set ℕ-Set is-countable-ℕ is-countable-ℕ

is-countable-ℤ : is-countable (ℤ-Set)
is-countable-ℤ =
  is-countable-coproduct (ℕ-Set) (coproduct-Set unit-Set ℕ-Set)
    ( is-countable-ℕ)
    ( is-countable-coproduct (unit-Set) (ℕ-Set)
      ( is-countable-unit) (is-countable-ℕ))

All standart finite sets are countable.

is-countable-Fin-Set : (n : ℕ) → is-countable (Fin-Set n)
is-countable-Fin-Set zero-ℕ = is-countable-empty
is-countable-Fin-Set (succ-ℕ n) =
  is-countable-coproduct (Fin-Set n) (unit-Set)
    ( is-countable-Fin-Set n) (is-countable-unit)

Recent changes