Cardinalities of sets
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Elif Uskuplu, Julian KG, Victor Blanchi, fernabnor and louismntnu.
Created on 2022-05-25.
Last modified on 2023-09-10.
module set-theory.cardinalities where
Imports
open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.functoriality-propositional-truncation open import foundation.identity-types open import foundation.law-of-excluded-middle open import foundation.mere-embeddings open import foundation.mere-equivalences open import foundation.propositional-extensionality open import foundation.propositions 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. 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
Cardinalities
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) cardinality : {l : Level} → Set l → cardinal l cardinality A = unit-trunc-Set A
Inequality of cardinalities
leq-cardinality-Prop' : {l1 l2 : Level} → Set l1 → cardinal l2 → Prop (l1 ⊔ l2) leq-cardinality-Prop' {l1} {l2} X = map-universal-property-trunc-Set ( Prop-Set (l1 ⊔ l2)) ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y')) compute-leq-cardinality-Prop' : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → Id ( leq-cardinality-Prop' X (cardinality Y)) ( mere-emb-Prop (type-Set X) (type-Set Y)) compute-leq-cardinality-Prop' {l1} {l2} X = triangle-universal-property-trunc-Set ( Prop-Set (l1 ⊔ l2)) ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y')) leq-cardinality-Prop : {l1 l2 : Level} → cardinal l1 → cardinal l2 → Prop (l1 ⊔ l2) leq-cardinality-Prop {l1} {l2} = map-universal-property-trunc-Set ( hom-Set (cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) ( leq-cardinality-Prop') leq-cardinality : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) leq-cardinality X Y = type-Prop (leq-cardinality-Prop X Y) infix 6 _≤-cardinality_ _≤-cardinality_ : {l1 l2 : Level} → cardinal l1 → cardinal l2 → UU (l1 ⊔ l2) _≤-cardinality_ = leq-cardinality is-prop-leq-cardinality : {l1 l2 : Level} {X : cardinal l1} {Y : cardinal l2} → is-prop (X ≤-cardinality Y) is-prop-leq-cardinality {X = X} {Y = Y} = is-prop-type-Prop (leq-cardinality-Prop X Y) compute-leq-cardinality : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → ( cardinality X ≤-cardinality cardinality Y) ≃ ( mere-emb (type-Set X) (type-Set Y)) compute-leq-cardinality {l1} {l2} X Y = equiv-eq-Prop ( ( htpy-eq ( triangle-universal-property-trunc-Set ( hom-Set (cardinal-Set l2) (Prop-Set (l1 ⊔ l2))) ( leq-cardinality-Prop') X) (cardinality Y)) ∙ ( compute-leq-cardinality-Prop' X Y)) unit-leq-cardinality : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → mere-emb (type-Set X) (type-Set Y) → cardinality X ≤-cardinality cardinality Y unit-leq-cardinality X Y = map-inv-equiv (compute-leq-cardinality X Y) inv-unit-leq-cardinality : {l1 l2 : Level} (X : Set l1) (Y : Set l2) → cardinality X ≤-cardinality cardinality Y → mere-emb (type-Set X) (type-Set Y) inv-unit-leq-cardinality X Y = pr1 (compute-leq-cardinality X Y) refl-leq-cardinality : {l : Level} → is-reflexive (leq-cardinality {l}) refl-leq-cardinality {l} = apply-dependent-universal-property-trunc-Set' ( λ X → set-Prop (leq-cardinality-Prop X X)) ( λ A → unit-leq-cardinality A A (refl-mere-emb (type-Set A))) transitive-leq-cardinality : {l1 l2 l3 : Level} (X : cardinal l1) (Y : cardinal l2) (Z : cardinal l3) → X ≤-cardinality Y → Y ≤-cardinality Z → X ≤-cardinality Z transitive-leq-cardinality X Y Z = apply-dependent-universal-property-trunc-Set' (λ u → set-Prop (function-Prop (u ≤-cardinality Y) (function-Prop (Y ≤-cardinality Z) (leq-cardinality-Prop u Z)))) (λ a → apply-dependent-universal-property-trunc-Set' (λ v → set-Prop (function-Prop ((cardinality a) ≤-cardinality v) (function-Prop (v ≤-cardinality Z) (leq-cardinality-Prop (cardinality a) Z)))) (λ b → apply-dependent-universal-property-trunc-Set' (λ w → set-Prop (function-Prop ((cardinality a) ≤-cardinality (cardinality b)) (function-Prop ((cardinality b) ≤-cardinality w) (leq-cardinality-Prop (cardinality a) w)))) (λ c a<b b<c → unit-leq-cardinality a c (transitive-mere-emb (inv-unit-leq-cardinality b c b<c) (inv-unit-leq-cardinality a b a<b))) Z) Y) X
Properties
For sets, the type # X = # Y
is equivalent to the type of mere equivalences from X
to Y
is-effective-cardinality : {l : Level} (X Y : Set l) → (cardinality X = cardinality Y) ≃ mere-equiv (type-Set X) (type-Set Y) is-effective-cardinality X Y = ( equiv-trunc-Prop (extensionality-Set X Y)) ∘e ( is-effective-unit-trunc-Set (Set _) X Y)
Assuming excluded middle we can show that leq-cardinality
is a partial order
Using the previous result and assuming excluded middle, we can show
leq-cardinality
is a partial order by showing that it is antisymmetric.
antisymmetric-leq-cardinality : {l1 : Level} (X Y : cardinal l1) → (LEM l1) → X ≤-cardinality Y → Y ≤-cardinality X → X = Y antisymmetric-leq-cardinality {l1} X Y lem = apply-dependent-universal-property-trunc-Set' (λ u → set-Prop (function-Prop (u ≤-cardinality Y) (function-Prop (Y ≤-cardinality u) (Id-Prop (cardinal-Set l1) u Y)))) (λ a → apply-dependent-universal-property-trunc-Set' (λ v → set-Prop (function-Prop ((cardinality a) ≤-cardinality v) (function-Prop (v ≤-cardinality (cardinality a)) (Id-Prop (cardinal-Set l1) (cardinality a) v)))) (λ b a<b b<a → map-inv-equiv (is-effective-cardinality a b) (antisymmetric-mere-emb lem (inv-unit-leq-cardinality _ _ a<b) (inv-unit-leq-cardinality _ _ b<a))) Y) X
Recent changes
- 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).