Inequality on cardinals

Content created by Fredrik Bakke.

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

module set-theory.inequality-cardinals where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.large-binary-relations
open import foundation.law-of-excluded-middle
open import foundation.mere-embeddings
open import foundation.propositional-extensionality
open import foundation.propositions
open import foundation.set-truncations
open import foundation.sets
open import foundation.univalence
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-preorders

open import set-theory.cardinals
open import set-theory.equality-cardinals

Idea

We say a cardinal X is less than or equal to a cardinal Y if any set in the isomorphism class of X embeds into any set in the isomorphism class of Y. This defines the standard ordering on cardinals.

Under the assumption of the law of excluded middle this relation is antisymmetric and hence defines a partial order, due to the Cantor–Schröder–Bernstein theorem.

Definition

Boundedness of the cardinality of a set

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

  leq-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2)
  leq-prop-Cardinal' =
    map-universal-property-trunc-Set
      ( Prop-Set (l1 ⊔ l2))
      ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y'))

  compute-leq-prop-Cardinal' :
    (Y : Set l2) →
    leq-prop-Cardinal' (cardinality Y) ＝
    mere-emb-Prop (type-Set X) (type-Set Y)
  compute-leq-prop-Cardinal' =
    triangle-universal-property-trunc-Set
      ( Prop-Set (l1 ⊔ l2))
      ( λ Y' → mere-emb-Prop (type-Set X) (type-Set Y'))

Inequality of cardinals

module _
  {l1 l2 : Level}
  where

  leq-prop-Cardinal : Cardinal l1 → Cardinal l2 → Prop (l1 ⊔ l2)
  leq-prop-Cardinal =
    map-universal-property-trunc-Set
      ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
      ( leq-prop-Cardinal')

  leq-Cardinal : Cardinal l1 → Cardinal l2 → UU (l1 ⊔ l2)
  leq-Cardinal X Y = type-Prop (leq-prop-Cardinal X Y)

  is-prop-leq-Cardinal :
    {X : Cardinal l1} {Y : Cardinal l2} → is-prop (leq-Cardinal X Y)
  is-prop-leq-Cardinal {X} {Y} = is-prop-type-Prop (leq-prop-Cardinal X Y)

Inequality of cardinalities

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

  leq-prop-cardinality : Prop (l1 ⊔ l2)
  leq-prop-cardinality = leq-prop-Cardinal (cardinality X) (cardinality Y)

  leq-cardinality : UU (l1 ⊔ l2)
  leq-cardinality = leq-Cardinal (cardinality X) (cardinality Y)

  is-prop-leq-cardinality : is-prop leq-cardinality
  is-prop-leq-cardinality = is-prop-leq-Cardinal

  eq-compute-leq-prop-cardinality :
    leq-prop-cardinality ＝ mere-emb-Prop (type-Set X) (type-Set Y)
  eq-compute-leq-prop-cardinality =
    ( htpy-eq
      ( triangle-universal-property-trunc-Set
        ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
        ( leq-prop-Cardinal') X) (cardinality Y)) ∙
    ( compute-leq-prop-Cardinal' X Y)

  eq-compute-leq-cardinality :
    leq-cardinality ＝ mere-emb (type-Set X) (type-Set Y)
  eq-compute-leq-cardinality =
    ap type-Prop eq-compute-leq-prop-cardinality

  compute-leq-cardinality :
    leq-cardinality ≃ mere-emb (type-Set X) (type-Set Y)
  compute-leq-cardinality = equiv-eq eq-compute-leq-cardinality

  unit-leq-cardinality :
    mere-emb (type-Set X) (type-Set Y) → leq-cardinality
  unit-leq-cardinality = map-inv-equiv compute-leq-cardinality

  inv-unit-leq-cardinality :
    leq-cardinality → mere-emb (type-Set X) (type-Set Y)
  inv-unit-leq-cardinality = pr1 compute-leq-cardinality

Inequality on cardinals is reflexive

refl-leq-cardinality : is-reflexive-Large-Relation Set leq-cardinality
refl-leq-cardinality A = unit-leq-cardinality A A (refl-mere-emb (type-Set A))

refl-leq-Cardinal : is-reflexive-Large-Relation Cardinal leq-Cardinal
refl-leq-Cardinal =
  apply-dependent-universal-property-trunc-Set'
    ( λ X → set-Prop (leq-prop-Cardinal X X))
    ( refl-leq-cardinality)

Inequality on cardinals is transitive

module _
  {l1 l2 l3 : Level}
  where

  transitive-leq-cardinality :
    (X : Set l1) (Y : Set l2) (Z : Set l3) →
    leq-cardinality Y Z → leq-cardinality X Y → leq-cardinality X Z
  transitive-leq-cardinality X Y Z Y≤Z X≤Y =
    unit-leq-cardinality X Z
      ( transitive-mere-emb
        ( inv-unit-leq-cardinality Y Z Y≤Z)
        ( inv-unit-leq-cardinality X Y X≤Y))

  transitive-leq-Cardinal :
    (X : Cardinal l1) (Y : Cardinal l2) (Z : Cardinal l3) →
    leq-Cardinal Y Z → leq-Cardinal X Y → leq-Cardinal X Z
  transitive-leq-Cardinal =
    apply-thrice-dependent-universal-property-trunc-Set'
      ( λ X Y Z →
        ( leq-Cardinal Y Z → leq-Cardinal X Y → leq-Cardinal X Z) ,
        ( is-set-function-type
          ( is-set-function-type
            ( is-set-is-prop is-prop-leq-Cardinal))))
      ( transitive-leq-cardinality)

Properties

Assuming excluded middle, then inequality is antisymmetric

Using that mere equivalence characterizes equality of cardinals we can conclude by the Cantor–Schröder–Bernstein theorem, assuming the law of excluded middle, that leq-Cardinal is antisymmetric and hence a partial order.

module _
  {l : Level} (lem : level-LEM l)
  where

  antisymmetric-leq-cardinality :
    (X Y : Set l) →
    leq-cardinality X Y →
    leq-cardinality Y X →
    cardinality X ＝ cardinality Y
  antisymmetric-leq-cardinality X Y X≤Y Y≤X =
    eq-mere-equiv-cardinality X Y
      ( antisymmetric-mere-emb
        ( lem)
        ( inv-unit-leq-cardinality X Y X≤Y)
        ( inv-unit-leq-cardinality Y X Y≤X))

  antisymmetric-leq-Cardinal :
    (X Y : Cardinal l) →
    leq-Cardinal X Y → leq-Cardinal Y X → X ＝ Y
  antisymmetric-leq-Cardinal =
    apply-twice-dependent-universal-property-trunc-Set'
      ( λ X Y →
        set-Prop
          ( function-Prop
            ( leq-Cardinal X Y)
            ( function-Prop (leq-Cardinal Y X) (Id-Prop (Cardinal-Set l) X Y))))
      ( antisymmetric-leq-cardinality)

The large poset of cardinals

large-preorder-Cardinal : Large-Preorder lsuc (_⊔_)
large-preorder-Cardinal =
  λ where
  .type-Large-Preorder → Cardinal
  .leq-prop-Large-Preorder → leq-prop-Cardinal
  .refl-leq-Large-Preorder → refl-leq-Cardinal
  .transitive-leq-Large-Preorder → transitive-leq-Cardinal

large-poset-Cardinal : LEM → Large-Poset lsuc (_⊔_)
large-poset-Cardinal lem =
  λ where
  .large-preorder-Large-Poset → large-preorder-Cardinal
  .antisymmetric-leq-Large-Poset → antisymmetric-leq-Cardinal lem

See also

Recent changes