Inhabited cardinals

Content created by Fredrik Bakke.

Created on 2026-02-16.
Last modified on 2026-02-16.

module set-theory.inhabited-cardinals where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.propositional-extensionality
open import foundation.propositions
open import foundation.set-truncations
open import foundation.sets
open import foundation.subtypes
open import foundation.univalence
open import foundation.universe-levels

open import set-theory.cardinals

Idea

A cardinal of sets κ is inhabited, if any set in its isomorphism class is inhabited.

Definitions

The predicate on cardinals of being inhabited

module _
  {l : Level} (κ : Cardinal l)
  where

  is-inhabited-prop-Cardinal : Prop l
  is-inhabited-prop-Cardinal =
    apply-universal-property-trunc-Set' κ
      ( Prop-Set l)
      ( is-inhabited-Prop ∘ type-Set)

  is-inhabited-Cardinal : UU l
  is-inhabited-Cardinal = type-Prop is-inhabited-prop-Cardinal

  is-prop-is-inhabited-Cardinal : is-prop is-inhabited-Cardinal
  is-prop-is-inhabited-Cardinal =
    is-prop-type-Prop is-inhabited-prop-Cardinal

Inhabited cardinalities

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

  is-inhabited-prop-cardinality : Prop l
  is-inhabited-prop-cardinality = is-inhabited-prop-Cardinal (cardinality X)

  is-inhabited-cardinality : UU l
  is-inhabited-cardinality = is-inhabited-Cardinal (cardinality X)

  is-prop-is-inhabited-cardinality : is-prop is-inhabited-cardinality
  is-prop-is-inhabited-cardinality =
    is-prop-is-inhabited-Cardinal (cardinality X)

  eq-compute-is-inhabited-prop-cardinality :
    is-inhabited-prop-cardinality ＝ is-inhabited-Prop (type-Set X)
  eq-compute-is-inhabited-prop-cardinality =
    triangle-universal-property-trunc-Set
      ( Prop-Set l)
      ( is-inhabited-Prop ∘ type-Set)
      ( X)

  eq-compute-is-inhabited-cardinality :
    is-inhabited-cardinality ＝ is-inhabited (type-Set X)
  eq-compute-is-inhabited-cardinality =
    ap type-Prop eq-compute-is-inhabited-prop-cardinality

  compute-is-inhabited-cardinality :
    is-inhabited-cardinality ≃ is-inhabited (type-Set X)
  compute-is-inhabited-cardinality =
    equiv-eq eq-compute-is-inhabited-cardinality

  unit-is-inhabited-cardinality :
    is-inhabited (type-Set X) → is-inhabited-cardinality
  unit-is-inhabited-cardinality =
    map-inv-equiv compute-is-inhabited-cardinality

  inv-unit-is-inhabited-cardinality :
    is-inhabited-cardinality → is-inhabited (type-Set X)
  inv-unit-is-inhabited-cardinality =
    map-equiv compute-is-inhabited-cardinality

The universe of inhabited cardinals

Inhabited-Cardinal : (l : Level) → UU (lsuc l)
Inhabited-Cardinal l = Σ (Cardinal l) is-inhabited-Cardinal

is-set-Inhabited-Cardinal : {l : Level} → is-set (Inhabited-Cardinal l)
is-set-Inhabited-Cardinal =
  is-set-type-subtype is-inhabited-prop-Cardinal is-set-Cardinal

Inhabited-Cardinal-Set : (l : Level) → Set (lsuc l)
Inhabited-Cardinal-Set l = (Inhabited-Cardinal l , is-set-Inhabited-Cardinal)

module _
  {l : Level} (κ : Inhabited-Cardinal l)
  where

  cardinal-Inhabited-Cardinal : Cardinal l
  cardinal-Inhabited-Cardinal = pr1 κ

  is-inhabited-Inhabited-Cardinal :
    is-inhabited-Cardinal cardinal-Inhabited-Cardinal
  is-inhabited-Inhabited-Cardinal = pr2 κ

Recent changes