Cardinals

Content created by Fredrik Bakke.

Created on 2026-01-10.
Last modified on 2026-01-10.

module set-theory.cardinals where
Imports 
open import foundation.equivalences
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.mere-equivalences
open import foundation.set-truncations
open import foundation.sets
open import foundation.universe-levels

Idea

The cardinality of a set is its isomorphism class. We take isomorphism classes of sets by set truncating the universe of sets of any given universe level, and such an isomorphism class is called a cardinal.

Note that this definition takes advantage of the univalence axiom: By the univalence axiom isomorphic sets are equal, and will be mapped to the same element in the set truncation of the universe of all sets.

Definition

Cardinals

Cardinal-Set : (l : Level) → Set (lsuc l)
Cardinal-Set l = trunc-Set (Set l)

Cardinal : (l : Level) → UU (lsuc l)
Cardinal l = type-Set (Cardinal-Set l)

is-set-Cardinal : {l : Level} → is-set (Cardinal l)
is-set-Cardinal {l} = is-set-type-Set (Cardinal-Set l)

The cardinality of a set

cardinality : {l : Level} → Set l → Cardinal l
cardinality A = unit-trunc-Set A

Recent changes