diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index f63911de8f8..ae18de7a2f2 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -306,6 +306,7 @@ open import foundation.maps-in-global-subuniverses public
 open import foundation.maps-in-subuniverses public
 open import foundation.maximum-truncation-levels public
 open import foundation.maybe public
+open import foundation.mere-decidable-embeddings public
 open import foundation.mere-embeddings public
 open import foundation.mere-equality public
 open import foundation.mere-equivalences public
diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md
index 70856d62e23..631d14a8f48 100644
--- a/src/foundation/decidable-embeddings.lagda.md
+++ b/src/foundation/decidable-embeddings.lagda.md
@@ -219,8 +219,8 @@ is-decidable-emb-id :
   {l : Level} {A : UU l} → is-decidable-emb (id {A = A})
 is-decidable-emb-id = (is-emb-id , is-decidable-map-id)
 
-decidable-emb-id : {l : Level} {A : UU l} → A ↪ᵈ A
-decidable-emb-id = (id , is-decidable-emb-id)
+id-decidable-emb : {l : Level} {A : UU l} → A ↪ᵈ A
+id-decidable-emb = (id , is-decidable-emb-id)
 
 is-decidable-prop-map-id :
   {l : Level} {A : UU l} → is-decidable-prop-map (id {A = A})
diff --git a/src/foundation/law-of-excluded-middle.lagda.md b/src/foundation/law-of-excluded-middle.lagda.md
index a633ea32d6a..ba4acd50cdd 100644
--- a/src/foundation/law-of-excluded-middle.lagda.md
+++ b/src/foundation/law-of-excluded-middle.lagda.md
@@ -33,6 +33,9 @@ asserts that any [proposition](foundation-core.propositions.md) `P` is
 LEM : (l : Level) → UU (lsuc l)
 LEM l = (P : Prop l) → is-decidable (type-Prop P)
 
+LEMω : UUω
+LEMω = {l : Level} → LEM l
+
 prop-LEM : (l : Level) → Prop (lsuc l)
 prop-LEM l = Π-Prop (Prop l) (is-decidable-Prop)
 ```
diff --git a/src/foundation/mere-decidable-embeddings.lagda.md b/src/foundation/mere-decidable-embeddings.lagda.md
new file mode 100644
index 00000000000..7153fe862d8
--- /dev/null
+++ b/src/foundation/mere-decidable-embeddings.lagda.md
@@ -0,0 +1,75 @@
+# Mere decidable embeddings
+
+```agda
+module foundation.mere-decidable-embeddings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cantor-schroder-bernstein-decidable-embeddings
+open import foundation.decidable-embeddings
+open import foundation.functoriality-propositional-truncation
+open import foundation.mere-equivalences
+open import foundation.propositional-truncations
+open import foundation.universe-levels
+open import foundation.weak-limited-principle-of-omniscience
+
+open import foundation-core.propositions
+
+open import order-theory.large-preorders
+```
+
+</details>
+
+## Idea
+
+A type `A` {{#concept "merely decidably embeds" Agda=mere-decidable-emb}} into a
+type `B` if there [merely exists](foundation.propositional-truncations.md) a
+[decidable embedding](foundation.decidable-embeddings.md) of `A` into `B`.
+
+## Definition
+
+```agda
+mere-decidable-emb-Prop : {l1 l2 : Level} → UU l1 → UU l2 → Prop (l1 ⊔ l2)
+mere-decidable-emb-Prop X Y = trunc-Prop (X ↪ᵈ Y)
+
+mere-decidable-emb : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
+mere-decidable-emb X Y = type-Prop (mere-decidable-emb-Prop X Y)
+
+is-prop-mere-decidable-emb :
+  {l1 l2 : Level} (X : UU l1) (Y : UU l2) → is-prop (mere-decidable-emb X Y)
+is-prop-mere-decidable-emb X Y = is-prop-type-Prop (mere-decidable-emb-Prop X Y)
+```
+
+## Properties
+
+### Types equipped with mere decidable embeddings form a preordering
+
+```agda
+refl-mere-decidable-emb : {l1 : Level} (X : UU l1) → mere-decidable-emb X X
+refl-mere-decidable-emb X = unit-trunc-Prop id-decidable-emb
+
+transitive-mere-decidable-emb :
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} →
+  mere-decidable-emb Y Z → mere-decidable-emb X Y → mere-decidable-emb X Z
+transitive-mere-decidable-emb = map-binary-trunc-Prop comp-decidable-emb
+
+mere-decidable-emb-Large-Preorder : Large-Preorder lsuc (_⊔_)
+mere-decidable-emb-Large-Preorder =
+  λ where
+  .type-Large-Preorder l → UU l
+  .leq-prop-Large-Preorder → mere-decidable-emb-Prop
+  .refl-leq-Large-Preorder → refl-mere-decidable-emb
+  .transitive-leq-Large-Preorder X Y Z → transitive-mere-decidable-emb
+```
+
+### Assuming WLPO, then types equipped with mere decidable embeddings form a partial ordering
+
+```agda
+antisymmetric-mere-decidable-emb :
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2} → level-WLPO (l1 ⊔ l2) →
+  mere-decidable-emb X Y → mere-decidable-emb Y X → mere-equiv X Y
+antisymmetric-mere-decidable-emb wlpo =
+  map-binary-trunc-Prop (Cantor-Schröder-Bernstein-WLPO wlpo)
+```
diff --git a/src/foundation/mere-embeddings.lagda.md b/src/foundation/mere-embeddings.lagda.md
index 4fbccc13d40..76a114ddc71 100644
--- a/src/foundation/mere-embeddings.lagda.md
+++ b/src/foundation/mere-embeddings.lagda.md
@@ -9,6 +9,7 @@ module foundation.mere-embeddings where
 ```agda
 open import foundation.cantor-schroder-bernstein-escardo
 open import foundation.embeddings
+open import foundation.functoriality-propositional-truncation
 open import foundation.law-of-excluded-middle
 open import foundation.mere-equivalences
 open import foundation.propositional-truncations
@@ -21,6 +22,12 @@ open import order-theory.large-preorders
 
 </details>
 
+## Idea
+
+A type `A` {{#concept "merely embeds" Agda=mere-emb}} into a type `B` if there
+[merely exists](foundation.propositional-truncations.md) an
+[embedding](foundation-core.embeddings.md) of `A` into `B`.
+
 ## Definition
 
 ```agda
@@ -46,20 +53,15 @@ refl-mere-emb X = unit-trunc-Prop id-emb
 transitive-mere-emb :
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3} →
   mere-emb Y Z → mere-emb X Y → mere-emb X Z
-transitive-mere-emb g f =
-  apply-universal-property-trunc-Prop g
-    ( mere-emb-Prop _ _)
-    ( λ g' →
-      apply-universal-property-trunc-Prop f
-        ( mere-emb-Prop _ _)
-        ( λ f' → unit-trunc-Prop (comp-emb g' f')))
+transitive-mere-emb = map-binary-trunc-Prop comp-emb
 
 mere-emb-Large-Preorder : Large-Preorder lsuc (_⊔_)
-type-Large-Preorder mere-emb-Large-Preorder l = UU l
-leq-prop-Large-Preorder mere-emb-Large-Preorder = mere-emb-Prop
-refl-leq-Large-Preorder mere-emb-Large-Preorder = refl-mere-emb
-transitive-leq-Large-Preorder mere-emb-Large-Preorder X Y Z =
-  transitive-mere-emb
+mere-emb-Large-Preorder =
+  λ where
+  .type-Large-Preorder l → UU l
+  .leq-prop-Large-Preorder → mere-emb-Prop
+  .refl-leq-Large-Preorder → refl-mere-emb
+  .transitive-leq-Large-Preorder X Y Z → transitive-mere-emb
 ```
 
 ### Assuming excluded middle, if there are mere embeddings between `A` and `B` in both directions, then there is a mere equivalence between them
@@ -68,11 +70,6 @@ transitive-leq-Large-Preorder mere-emb-Large-Preorder X Y Z =
 antisymmetric-mere-emb :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} →
   LEM (l1 ⊔ l2) → mere-emb X Y → mere-emb Y X → mere-equiv X Y
-antisymmetric-mere-emb lem f g =
-  apply-universal-property-trunc-Prop f
-    ( mere-equiv-Prop _ _)
-    ( λ f' →
-      apply-universal-property-trunc-Prop g
-        ( mere-equiv-Prop _ _)
-        ( λ g' → unit-trunc-Prop (Cantor-Schröder-Bernstein-Escardó lem f' g')))
+antisymmetric-mere-emb lem =
+  map-binary-trunc-Prop (Cantor-Schröder-Bernstein-Escardó lem)
 ```
diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md
index 154cc2d2b55..30598163594 100644
--- a/src/foundation/set-truncations.lagda.md
+++ b/src/foundation/set-truncations.lagda.md
@@ -122,6 +122,50 @@ module _
     (x : type-trunc-Set A) → type-Set (B x)
   apply-dependent-universal-property-trunc-Set' =
     map-inv-equiv (equiv-dependent-universal-property-trunc-Set B) f
+
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : type-trunc-Set A → UU l2}
+  (C : (a : type-trunc-Set A) → type-trunc-Set (B a) → Set l3)
+  (f :
+    (x : A) (y : B (unit-trunc-Set x)) →
+    type-Set (C (unit-trunc-Set x) (unit-trunc-Set y)))
+  where
+
+  apply-twice-dependent-universal-property-trunc-Set' :
+    (a : type-trunc-Set A) (b : type-trunc-Set (B a)) → type-Set (C a b)
+  apply-twice-dependent-universal-property-trunc-Set' =
+    apply-dependent-universal-property-trunc-Set'
+    ( λ x → Π-Set (trunc-Set (B x)) (C x))
+    ( λ x →
+      apply-dependent-universal-property-trunc-Set'
+        ( C (unit-trunc-Set x))
+        ( f x))
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : type-trunc-Set A → UU l2}
+  {C : (a : type-trunc-Set A) → type-trunc-Set (B a) → UU l3}
+  (D :
+    (a : type-trunc-Set A) (b : type-trunc-Set (B a)) → type-trunc-Set (C a b) →
+    Set l4)
+  (f :
+    (x : A)
+    (y : B (unit-trunc-Set x))
+    (z : C (unit-trunc-Set x) (unit-trunc-Set y)) →
+    type-Set (D (unit-trunc-Set x) (unit-trunc-Set y) (unit-trunc-Set z)))
+  where
+
+  apply-thrice-dependent-universal-property-trunc-Set' :
+    (a : type-trunc-Set A)
+    (b : type-trunc-Set (B a))
+    (c : type-trunc-Set (C a b)) →
+    type-Set (D a b c)
+  apply-thrice-dependent-universal-property-trunc-Set' =
+    apply-twice-dependent-universal-property-trunc-Set'
+      ( λ x y → Π-Set (trunc-Set (C x y)) (D x y))
+      ( λ x y →
+        apply-dependent-universal-property-trunc-Set'
+          ( D (unit-trunc-Set x) (unit-trunc-Set y))
+          ( f x y))
 ```
 
 ### The universal property of set truncations
diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index 6ce59643c86..391f523884b 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -38,7 +38,7 @@ set-level structure. In fact, assuming univalence, it is a proper
 In this module, we consider ideas historically related to the study of set
 theories both as foundations of set-level mathematics, but also as a study of
 hierarchies in mathematics. This includes ideas such as
-[cardinality](set-theory.cardinalities.md) and
+[cardinality](set-theory.cardinals.md) and
 [infinity](set-theory.infinite-sets.md), the
 [cumulative hierarchy](set-theory.cumulative-hierarchy.md) as a model of set
 theory, and [Russell's paradox](set-theory.russells-paradox.md).
@@ -52,12 +52,15 @@ open import set-theory.baire-space public
 open import set-theory.bounded-increasing-binary-sequences public
 open import set-theory.cantor-space public
 open import set-theory.cantors-diagonal-argument public
-open import set-theory.cardinalities public
+open import set-theory.cardinals public
+open import set-theory.complemented-inequality-cardinals public
 open import set-theory.countable-sets public
 open import set-theory.cumulative-hierarchy public
+open import set-theory.equality-cardinals public
 open import set-theory.finite-elements-increasing-binary-sequences public
 open import set-theory.inclusion-natural-numbers-increasing-binary-sequences public
 open import set-theory.increasing-binary-sequences public
+open import set-theory.inequality-cardinals public
 open import set-theory.inequality-increasing-binary-sequences public
 open import set-theory.infinite-sets public
 open import set-theory.positive-elements-increasing-binary-sequences public
diff --git a/src/set-theory/cardinalities.lagda.md b/src/set-theory/cardinalities.lagda.md
deleted file mode 100644
index 26956dc000c..00000000000
--- a/src/set-theory/cardinalities.lagda.md
+++ /dev/null
@@ -1,225 +0,0 @@
-# Cardinalities of sets
-
-```agda
-module set-theory.cardinalities where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-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.large-binary-relations
-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
-```
-
-</details>
-
-## Idea
-
-The
-{{#concept "cardinality" Disambiguation="of a set" Agda=cardinality WD="cardinality" WDID=Q4049983}}
-of a [set](foundation-core.sets.md) is its
-[isomorphism](category-theory.isomorphisms-in-categories.md) class. We take
-isomorphism classes of sets by [set truncating](foundation.set-truncations.md)
-the universe of sets of any given
-[universe level](foundation.universe-levels.md). Note that this definition takes
-advantage of the [univalence axiom](foundation.univalence.md): By the univalence
-axiom [isomorphic sets](foundation.isomorphisms-of-sets.md) are
-[equal](foundation-core.identity-types.md), and will be mapped to the same
-element in the set truncation of the universe of all sets.
-
-## Definition
-
-### Cardinalities
-
-```agda
-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
-
-```agda
-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) →
-  ( 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-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)
-
-is-prop-leq-cardinality :
-  {l1 l2 : Level} {X : cardinal l1} {Y : cardinal l2} →
-  is-prop (leq-cardinality X 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) →
-  ( leq-cardinality (cardinality X) (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-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) →
-  leq-cardinality (cardinality X) (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) →
-  leq-cardinality (cardinality X) (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 : is-reflexive-Large-Relation cardinal leq-cardinality
-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) →
-  leq-cardinality X Y →
-  leq-cardinality Y Z →
-  leq-cardinality X Z
-transitive-leq-cardinality X Y Z =
-  apply-dependent-universal-property-trunc-Set'
-  ( λ u →
-    set-Prop
-      ( function-Prop
-        ( leq-cardinality u Y)
-        ( function-Prop (leq-cardinality Y Z)
-          ( leq-cardinality-Prop u Z))))
-  ( λ a →
-    apply-dependent-universal-property-trunc-Set'
-    ( λ v →
-      set-Prop
-        (function-Prop
-          (leq-cardinality (cardinality a) v)
-          (function-Prop (leq-cardinality v Z)
-            (leq-cardinality-Prop (cardinality a) Z))))
-    ( λ b →
-      apply-dependent-universal-property-trunc-Set'
-      ( λ w →
-        set-Prop
-          (function-Prop
-            (leq-cardinality (cardinality a) (cardinality b))
-            (function-Prop (leq-cardinality (cardinality b) 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`
-
-```agda
-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)
-
-eq-mere-equiv-cardinality :
-  {l : Level} (X Y : Set l) →
-  mere-equiv (type-Set X) (type-Set Y) → cardinality X ＝ cardinality Y
-eq-mere-equiv-cardinality X Y = map-inv-equiv (is-effective-cardinality 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 conclude
-`leq-cardinality` is a partial order by showing that it is antisymmetric.
-
-```agda
-antisymmetric-leq-cardinality :
-  {l1 : Level} (X Y : cardinal l1) → (LEM l1) →
-  leq-cardinality X Y → leq-cardinality Y X → X ＝ Y
-antisymmetric-leq-cardinality {l1} X Y lem =
-  apply-dependent-universal-property-trunc-Set'
-  ( λ u →
-    set-Prop
-      ( function-Prop
-        ( leq-cardinality u Y)
-        ( function-Prop
-          ( leq-cardinality Y u)
-          ( Id-Prop (cardinal-Set l1) u Y))))
-  ( λ a →
-    apply-dependent-universal-property-trunc-Set'
-    ( λ v →
-      set-Prop
-        ( function-Prop
-          ( leq-cardinality (cardinality a) v)
-          ( function-Prop
-            ( leq-cardinality v (cardinality a))
-            ( Id-Prop (cardinal-Set l1) (cardinality a) v))))
-    ( λ b a<b b<a →
-      eq-mere-equiv-cardinality a b
-        ( antisymmetric-mere-emb lem
-          ( inv-unit-leq-cardinality _ _ a<b)
-          ( inv-unit-leq-cardinality _ _ b<a)))
-    ( Y))
-  ( X)
-```
-
-## External links
-
-- [Cardinality](https://en.wikipedia.org/wiki/Cardinality) at Wikipedia
-- [cardinal number](https://ncatlab.org/nlab/show/cardinal+number) at $n$Lab
diff --git a/src/set-theory/cardinals.lagda.md b/src/set-theory/cardinals.lagda.md
new file mode 100644
index 00000000000..33fc3b3f054
--- /dev/null
+++ b/src/set-theory/cardinals.lagda.md
@@ -0,0 +1,64 @@
+# Cardinals
+
+```agda
+module set-theory.cardinals where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "cardinality" Disambiguation="of a set" Agda=cardinality WD="cardinality" WDID=Q4049983}}
+of a [set](foundation-core.sets.md) is its
+[isomorphism](category-theory.isomorphisms-in-categories.md) class. We take
+isomorphism classes of sets by [set truncating](foundation.set-truncations.md)
+the universe of sets of any given
+[universe level](foundation.universe-levels.md), and such an isomorphism class
+is called a
+{{#concept "cardinal" Disambiguation="sets" WD="cardinal number" WDID=Q163875}}.
+
+Note that this definition takes advantage of the
+[univalence axiom](foundation.univalence.md): By the univalence axiom
+[isomorphic sets](foundation.isomorphisms-of-sets.md) are
+[equal](foundation-core.identity-types.md), and will be mapped to the same
+element in the set truncation of the universe of all sets. S
+
+## Definition
+
+### Cardinals
+
+```agda
+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
+
+```agda
+cardinality : {l : Level} → Set l → Cardinal l
+cardinality A = unit-trunc-Set A
+```
+
+## External links
+
+- [Cardinality](https://en.wikipedia.org/wiki/Cardinality) at Wikipedia
+- [cardinal number](https://ncatlab.org/nlab/show/cardinal+number) at $n$Lab
diff --git a/src/set-theory/complemented-inequality-cardinals.lagda.md b/src/set-theory/complemented-inequality-cardinals.lagda.md
new file mode 100644
index 00000000000..cc4bfe3abaf
--- /dev/null
+++ b/src/set-theory/complemented-inequality-cardinals.lagda.md
@@ -0,0 +1,262 @@
+# Complemented inequality on cardinals
+
+```agda
+module set-theory.complemented-inequality-cardinals where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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.mere-decidable-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 foundation.weak-limited-principle-of-omniscience
+
+open import order-theory.large-posets
+open import order-theory.large-preorders
+
+open import set-theory.cardinals
+open import set-theory.equality-cardinals
+```
+
+</details>
+
+## Idea
+
+We may say a [cardinal](set-theory.cardinals.md) `X` is
+{{#concept "less than or equal to" Agda=leq-complemented-Cardinal}} a cardinal
+`Y` if any [set](foundation-core.sets.md) in the isomorphism class represented
+by `X` [embeds](foundation-core.embeddings.md) as a
+[complemented subtype](foundation.decidable-subtypes.md) into any set in the
+isomorphism class represented by `Y`. In other words, if there is a
+[decidable embedding](foundation.decidable-embeddings.md) from the first to the
+second. This defines the
+{{#concept "complemented ordering" Disambiguation="on cardinalities of sets"}}
+on cardinalities of sets.
+
+Under the assumption of the
+[weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md),
+this relation is antisymmetric and hence defines a
+[partial order](order-theory.posets.md) on cardinals.
+
+## Definition
+
+### Complemented boundedness of the cardinality of a set
+
+```agda
+module _
+  {l1 l2 : Level} (X : Set l1)
+  where
+
+  leq-complemented-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2)
+  leq-complemented-prop-Cardinal' =
+    map-universal-property-trunc-Set
+      ( Prop-Set (l1 ⊔ l2))
+      ( λ Y' → mere-decidable-emb-Prop (type-Set X) (type-Set Y'))
+
+  compute-leq-complemented-prop-Cardinal' :
+    (Y : Set l2) →
+    leq-complemented-prop-Cardinal' (cardinality Y) ＝
+    mere-decidable-emb-Prop (type-Set X) (type-Set Y)
+  compute-leq-complemented-prop-Cardinal' =
+    triangle-universal-property-trunc-Set
+      ( Prop-Set (l1 ⊔ l2))
+      ( λ Y' → mere-decidable-emb-Prop (type-Set X) (type-Set Y'))
+```
+
+### Complemented inequality of cardinals
+
+```agda
+module _
+  {l1 l2 : Level}
+  where
+
+  leq-complemented-prop-Cardinal :
+    Cardinal l1 → Cardinal l2 → Prop (l1 ⊔ l2)
+  leq-complemented-prop-Cardinal =
+    map-universal-property-trunc-Set
+      ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
+      ( leq-complemented-prop-Cardinal')
+
+  leq-complemented-Cardinal :
+    Cardinal l1 → Cardinal l2 → UU (l1 ⊔ l2)
+  leq-complemented-Cardinal X Y =
+    type-Prop (leq-complemented-prop-Cardinal X Y)
+
+  is-prop-leq-complemented-Cardinal :
+    {X : Cardinal l1} {Y : Cardinal l2} →
+    is-prop (leq-complemented-Cardinal X Y)
+  is-prop-leq-complemented-Cardinal {X} {Y} =
+    is-prop-type-Prop (leq-complemented-prop-Cardinal X Y)
+```
+
+### Complemented inequality of cardinalities
+
+```agda
+module _
+  {l1 l2 : Level} (X : Set l1) (Y : Set l2)
+  where
+
+  leq-complemented-prop-cardinality : Prop (l1 ⊔ l2)
+  leq-complemented-prop-cardinality =
+    leq-complemented-prop-Cardinal (cardinality X) (cardinality Y)
+
+  leq-complemented-cardinality : UU (l1 ⊔ l2)
+  leq-complemented-cardinality =
+    leq-complemented-Cardinal (cardinality X) (cardinality Y)
+
+  is-prop-leq-complemented-cardinality :
+    is-prop leq-complemented-cardinality
+  is-prop-leq-complemented-cardinality =
+    is-prop-leq-complemented-Cardinal
+
+  compute-leq-complemented-prop-cardinality' :
+    leq-complemented-prop-cardinality ＝
+    mere-decidable-emb-Prop (type-Set X) (type-Set Y)
+  compute-leq-complemented-prop-cardinality' =
+    ( htpy-eq
+      ( triangle-universal-property-trunc-Set
+        ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
+        ( leq-complemented-prop-Cardinal') X) (cardinality Y)) ∙
+    ( compute-leq-complemented-prop-Cardinal' X Y)
+
+  compute-leq-complemented-cardinality' :
+    leq-complemented-cardinality ＝
+    mere-decidable-emb (type-Set X) (type-Set Y)
+  compute-leq-complemented-cardinality' =
+    ap type-Prop compute-leq-complemented-prop-cardinality'
+
+  compute-leq-complemented-cardinality :
+    leq-complemented-cardinality ≃
+    mere-decidable-emb (type-Set X) (type-Set Y)
+  compute-leq-complemented-cardinality =
+    equiv-eq compute-leq-complemented-cardinality'
+
+  unit-leq-complemented-cardinality :
+    mere-decidable-emb (type-Set X) (type-Set Y) →
+    leq-complemented-cardinality
+  unit-leq-complemented-cardinality =
+    map-inv-equiv compute-leq-complemented-cardinality
+
+  inv-unit-leq-complemented-cardinality :
+    leq-complemented-cardinality →
+    mere-decidable-emb (type-Set X) (type-Set Y)
+  inv-unit-leq-complemented-cardinality =
+    pr1 compute-leq-complemented-cardinality
+```
+
+### Complemented inequality on cardinals is reflexive
+
+```agda
+refl-leq-complemented-cardinality :
+  is-reflexive-Large-Relation Set leq-complemented-cardinality
+refl-leq-complemented-cardinality A =
+  unit-leq-complemented-cardinality A A
+    ( refl-mere-decidable-emb (type-Set A))
+
+refl-leq-complemented-Cardinal :
+  is-reflexive-Large-Relation Cardinal leq-complemented-Cardinal
+refl-leq-complemented-Cardinal =
+  apply-dependent-universal-property-trunc-Set'
+    ( λ X → set-Prop (leq-complemented-prop-Cardinal X X))
+    ( refl-leq-complemented-cardinality)
+```
+
+### Complemented inequality on cardinals is transitive
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  where
+
+  transitive-leq-complemented-cardinality :
+    (X : Set l1) (Y : Set l2) (Z : Set l3) →
+    leq-complemented-cardinality Y Z →
+    leq-complemented-cardinality X Y →
+    leq-complemented-cardinality X Z
+  transitive-leq-complemented-cardinality X Y Z Y≤Z X≤Y =
+    unit-leq-complemented-cardinality X Z
+      ( transitive-mere-decidable-emb
+        ( inv-unit-leq-complemented-cardinality Y Z Y≤Z)
+        ( inv-unit-leq-complemented-cardinality X Y X≤Y))
+
+  transitive-leq-complemented-Cardinal :
+    (X : Cardinal l1) (Y : Cardinal l2) (Z : Cardinal l3) →
+    leq-complemented-Cardinal Y Z →
+    leq-complemented-Cardinal X Y →
+    leq-complemented-Cardinal X Z
+  transitive-leq-complemented-Cardinal =
+    apply-thrice-dependent-universal-property-trunc-Set'
+      ( λ X Y Z →
+        ( leq-complemented-Cardinal Y Z →
+          leq-complemented-Cardinal X Y →
+          leq-complemented-Cardinal X Z) ,
+        ( is-set-function-type
+          ( is-set-function-type
+            ( is-set-is-prop is-prop-leq-complemented-Cardinal))))
+      ( transitive-leq-complemented-cardinality)
+```
+
+## Properties
+
+### Assuming the weak limited principle of omniscience, then complemented inequality forms a partial order
+
+```agda
+module _
+  {l : Level} (wlpo : level-WLPO l)
+  where
+
+  antisymmetric-leq-complemented-cardinality :
+    (X Y : Set l) →
+    leq-complemented-cardinality X Y →
+    leq-complemented-cardinality Y X →
+    cardinality X ＝ cardinality Y
+  antisymmetric-leq-complemented-cardinality X Y X≤Y Y≤X =
+    eq-mere-equiv-cardinality X Y
+      ( antisymmetric-mere-decidable-emb
+        ( wlpo)
+        ( inv-unit-leq-complemented-cardinality X Y X≤Y)
+        ( inv-unit-leq-complemented-cardinality Y X Y≤X))
+
+  antisymmetric-leq-complemented-Cardinal :
+    (X Y : Cardinal l) →
+    leq-complemented-Cardinal X Y → leq-complemented-Cardinal Y X → X ＝ Y
+  antisymmetric-leq-complemented-Cardinal =
+    apply-twice-dependent-universal-property-trunc-Set'
+      ( λ X Y →
+        set-Prop
+          ( function-Prop
+            ( leq-complemented-Cardinal X Y)
+            ( function-Prop
+              ( leq-complemented-Cardinal Y X)
+              ( Id-Prop (Cardinal-Set l) X Y))))
+      ( antisymmetric-leq-complemented-cardinality)
+```
+
+### The large poset of cardinals under complemented inequality
+
+```agda
+large-preorder-complemented-Cardinal : Large-Preorder lsuc (_⊔_)
+large-preorder-complemented-Cardinal =
+  λ where
+  .type-Large-Preorder → Cardinal
+  .leq-prop-Large-Preorder → leq-complemented-prop-Cardinal
+  .refl-leq-Large-Preorder → refl-leq-complemented-Cardinal
+  .transitive-leq-Large-Preorder → transitive-leq-complemented-Cardinal
+
+large-poset-complemented-Cardinal : WLPO → Large-Poset lsuc (_⊔_)
+large-poset-complemented-Cardinal wlpo =
+  λ where
+  .large-preorder-Large-Poset → large-preorder-complemented-Cardinal
+  .antisymmetric-leq-Large-Poset → antisymmetric-leq-complemented-Cardinal wlpo
+```
diff --git a/src/set-theory/equality-cardinals.lagda.md b/src/set-theory/equality-cardinals.lagda.md
new file mode 100644
index 00000000000..8eea5937e59
--- /dev/null
+++ b/src/set-theory/equality-cardinals.lagda.md
@@ -0,0 +1,318 @@
+# Equality of cardinals
+
+```agda
+module set-theory.equality-cardinals where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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.functoriality-propositional-truncation
+open import foundation.identity-types
+open import foundation.large-equivalence-relations
+open import foundation.large-similarity-relations
+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.univalence
+open import foundation.universe-levels
+
+open import set-theory.cardinals
+```
+
+</details>
+
+## Idea
+
+Two [cardinals of sets](set-theory.cardinals.md) `X` and `Y` are
+{{#concept "similar" Disambiguation="cardinals" Agda=sim-Cardinal}} if there
+[merely](foundation.inhabited-types.md) is an
+[equivalence](foundation-core.equivalences.md) between any two representing two
+types. This characterizes [equality](foundation-core.identity-types.md) of
+cardinals.
+
+## Definition
+
+### The underlying similarity of cardinalities
+
+```agda
+module _
+  {l1 l2 : Level} (X : Set l1) (Y : Set l2)
+  where
+
+  sim-prop-cardinality' : Prop (l1 ⊔ l2)
+  sim-prop-cardinality' = mere-equiv-Prop (type-Set X) (type-Set Y)
+
+  sim-cardinality' : UU (l1 ⊔ l2)
+  sim-cardinality' = mere-equiv (type-Set X) (type-Set Y)
+
+  is-prop-sim-sim-cardinality' : is-prop sim-cardinality'
+  is-prop-sim-sim-cardinality' = is-prop-mere-equiv (type-Set X) (type-Set Y)
+
+refl-sim-cardinality' : {l : Level} (X : Set l) → sim-cardinality' X X
+refl-sim-cardinality' X = refl-mere-equiv (type-Set X)
+
+transitive-sim-cardinality' :
+  {l1 l2 l3 : Level} (X : Set l1) (Y : Set l2) (Z : Set l3) →
+  sim-cardinality' Y Z → sim-cardinality' X Y → sim-cardinality' X Z
+transitive-sim-cardinality' X Y Z =
+  transitive-mere-equiv (type-Set X) (type-Set Y) (type-Set Z)
+
+symmetric-sim-cardinality' :
+  {l1 l2 : Level} (X : Set l1) (Y : Set l2) →
+  sim-cardinality' X Y → sim-cardinality' Y X
+symmetric-sim-cardinality' X Y =
+  symmetric-mere-equiv (type-Set X) (type-Set Y)
+```
+
+### Similarity of cardinalities with a cardinal
+
+```agda
+module _
+  {l1 l2 : Level} (X : Set l1)
+  where
+
+  sim-prop-Cardinal' : Cardinal l2 → Prop (l1 ⊔ l2)
+  sim-prop-Cardinal' =
+    map-universal-property-trunc-Set
+      ( Prop-Set (l1 ⊔ l2))
+      ( sim-prop-cardinality' X)
+
+  sim-Cardinal' : Cardinal l2 → UU (l1 ⊔ l2)
+  sim-Cardinal' Y = type-Prop (sim-prop-Cardinal' Y)
+
+  is-prop-sim-sim-Cardinal' : (Y : Cardinal l2) → is-prop (sim-Cardinal' Y)
+  is-prop-sim-sim-Cardinal' Y = is-prop-type-Prop (sim-prop-Cardinal' Y)
+
+  eq-compute-sim-prop-Cardinal' :
+    (Y : Set l2) →
+    sim-prop-Cardinal' (cardinality Y) ＝ sim-prop-cardinality' X Y
+  eq-compute-sim-prop-Cardinal' =
+    triangle-universal-property-trunc-Set
+      ( Prop-Set (l1 ⊔ l2))
+      ( sim-prop-cardinality' X)
+
+  eq-compute-sim-Cardinal' :
+    (Y : Set l2) →
+    sim-Cardinal' (cardinality Y) ＝ sim-cardinality' X Y
+  eq-compute-sim-Cardinal' Y =
+    ap type-Prop (eq-compute-sim-prop-Cardinal' Y)
+```
+
+### Similarity of cardinals
+
+```agda
+module _
+  {l1 l2 : Level} (X : Cardinal l1) (Y : Cardinal l2)
+  where
+
+  sim-prop-Cardinal : Prop (l1 ⊔ l2)
+  sim-prop-Cardinal =
+    map-universal-property-trunc-Set
+      ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
+      ( sim-prop-Cardinal')
+      ( X)
+      ( Y)
+
+  sim-Cardinal : UU (l1 ⊔ l2)
+  sim-Cardinal = type-Prop sim-prop-Cardinal
+
+  is-prop-sim-sim-Cardinal : is-prop sim-Cardinal
+  is-prop-sim-sim-Cardinal = is-prop-type-Prop sim-prop-Cardinal
+
+  sim-set-Cardinal : Set (l1 ⊔ l2)
+  sim-set-Cardinal = set-Prop sim-prop-Cardinal
+```
+
+### Similarity of cardinalities
+
+```agda
+module _
+  {l1 l2 : Level} (X : Set l1) (Y : Set l2)
+  where
+
+  sim-prop-cardinality : Prop (l1 ⊔ l2)
+  sim-prop-cardinality = sim-prop-Cardinal (cardinality X) (cardinality Y)
+
+  sim-cardinality : UU (l1 ⊔ l2)
+  sim-cardinality = type-Prop sim-prop-cardinality
+
+  is-prop-sim-sim-cardinality : is-prop sim-cardinality
+  is-prop-sim-sim-cardinality = is-prop-type-Prop sim-prop-cardinality
+
+  eq-compute-sim-prop-cardinality :
+    sim-prop-cardinality ＝ mere-equiv-Prop (type-Set X) (type-Set Y)
+  eq-compute-sim-prop-cardinality =
+    ( htpy-eq
+      ( triangle-universal-property-trunc-Set
+        ( hom-set-Set (Cardinal-Set l2) (Prop-Set (l1 ⊔ l2)))
+        ( sim-prop-Cardinal')
+        ( X))
+      ( cardinality Y)) ∙
+    ( eq-compute-sim-prop-Cardinal' X Y)
+
+  eq-compute-sim-cardinality :
+    sim-cardinality ＝ mere-equiv (type-Set X) (type-Set Y)
+  eq-compute-sim-cardinality =
+    ap type-Prop eq-compute-sim-prop-cardinality
+
+  compute-sim-cardinality :
+    sim-cardinality ≃ mere-equiv (type-Set X) (type-Set Y)
+  compute-sim-cardinality = equiv-eq eq-compute-sim-cardinality
+
+  unit-sim-cardinality :
+    mere-equiv (type-Set X) (type-Set Y) → sim-cardinality
+  unit-sim-cardinality = map-inv-equiv compute-sim-cardinality
+
+  inv-unit-sim-cardinality :
+    sim-cardinality → mere-equiv (type-Set X) (type-Set Y)
+  inv-unit-sim-cardinality = pr1 compute-sim-cardinality
+```
+
+## Properties
+
+### Equality of cardinalities is equivalent to mere equivalence
+
+```agda
+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)
+
+eq-mere-equiv-cardinality :
+  {l : Level} (X Y : Set l) →
+  mere-equiv (type-Set X) (type-Set Y) → cardinality X ＝ cardinality Y
+eq-mere-equiv-cardinality X Y = map-inv-equiv (is-effective-cardinality X Y)
+```
+
+### Similarity of cardinals is reflexive
+
+```agda
+refl-sim-cardinality : {l : Level} (X : Set l) → sim-cardinality X X
+refl-sim-cardinality X = unit-sim-cardinality X X (refl-mere-equiv (type-Set X))
+
+refl-sim-Cardinal : {l : Level} (X : Cardinal l) → sim-Cardinal X X
+refl-sim-Cardinal =
+  apply-dependent-universal-property-trunc-Set'
+    ( λ X → sim-set-Cardinal X X)
+    ( refl-sim-cardinality)
+```
+
+### Similarity of cardinals is symmetric
+
+```agda
+symmetric-sim-cardinality :
+  {l1 l2 : Level}
+  (X : Set l1) (Y : Set l2) →
+  sim-cardinality X Y → sim-cardinality Y X
+symmetric-sim-cardinality X Y p =
+  unit-sim-cardinality Y X
+    ( symmetric-sim-cardinality' X Y (inv-unit-sim-cardinality X Y p))
+
+abstract
+  symmetric-sim-Cardinal :
+    {l1 l2 : Level}
+    (X : Cardinal l1) (Y : Cardinal l2) →
+    sim-Cardinal X Y → sim-Cardinal Y X
+  symmetric-sim-Cardinal =
+    apply-twice-dependent-universal-property-trunc-Set'
+      ( λ X Y → hom-set-Set (sim-set-Cardinal X Y) (sim-set-Cardinal Y X))
+      ( symmetric-sim-cardinality)
+```
+
+### Similarity of cardinals is transitive
+
+```agda
+transitive-sim-cardinality :
+  {l1 l2 l3 : Level}
+  (X : Set l1) (Y : Set l2) (Z : Set l3) →
+  sim-cardinality Y Z → sim-cardinality X Y → sim-cardinality X Z
+transitive-sim-cardinality X Y Z p q =
+  unit-sim-cardinality X Z
+    ( transitive-sim-cardinality' X Y Z
+      ( inv-unit-sim-cardinality Y Z p)
+      ( inv-unit-sim-cardinality X Y q))
+
+abstract
+  transitive-sim-Cardinal :
+    {l1 l2 l3 : Level}
+    (X : Cardinal l1) (Y : Cardinal l2) (Z : Cardinal l3) →
+    sim-Cardinal Y Z → sim-Cardinal X Y → sim-Cardinal X Z
+  transitive-sim-Cardinal =
+    apply-thrice-dependent-universal-property-trunc-Set'
+      ( λ X Y Z →
+        hom-set-Set
+          ( sim-set-Cardinal Y Z)
+          ( hom-set-Set (sim-set-Cardinal X Y) (sim-set-Cardinal X Z)))
+      ( transitive-sim-cardinality)
+```
+
+### Similarity of cardinals is extensional
+
+```agda
+module _
+  {l : Level}
+  where
+
+  sim-eq-Cardinal :
+      (X Y : Cardinal l) → X ＝ Y → sim-Cardinal X Y
+  sim-eq-Cardinal X .X refl = refl-sim-Cardinal X
+
+  sim-eq-cardinality :
+      (X Y : Set l) → cardinality X ＝ cardinality Y → sim-cardinality X Y
+  sim-eq-cardinality X Y = sim-eq-Cardinal (cardinality X) (cardinality Y)
+
+  eq-sim-cardinality :
+    (X Y : Set l) → sim-cardinality X Y → cardinality X ＝ cardinality Y
+  eq-sim-cardinality X Y p =
+    eq-mere-equiv-cardinality X Y (inv-unit-sim-cardinality X Y p)
+
+  abstract
+    eq-sim-Cardinal :
+      (X Y : Cardinal l) → sim-Cardinal X Y → X ＝ Y
+    eq-sim-Cardinal =
+      apply-twice-dependent-universal-property-trunc-Set'
+        ( λ X Y →
+          hom-set-Set
+            ( sim-set-Cardinal X Y)
+            ( set-Prop (Id-Prop (Cardinal-Set l) X Y)))
+        ( eq-sim-cardinality)
+
+  abstract
+    antisymmetric-sim-Cardinal :
+      (X Y : Cardinal l) → sim-Cardinal X Y → sim-Cardinal Y X → X ＝ Y
+    antisymmetric-sim-Cardinal X Y p _ = eq-sim-Cardinal X Y p
+```
+
+### Similarity of cardinals is a large similarity relation
+
+```agda
+large-equivalence-relation-Cardinal : Large-Equivalence-Relation (_⊔_) Cardinal
+large-equivalence-relation-Cardinal =
+  λ where
+    .sim-prop-Large-Equivalence-Relation → sim-prop-Cardinal
+    .refl-sim-Large-Equivalence-Relation → refl-sim-Cardinal
+    .symmetric-sim-Large-Equivalence-Relation → symmetric-sim-Cardinal
+    .transitive-sim-Large-Equivalence-Relation → transitive-sim-Cardinal
+
+large-similarity-relation-Cardinal : Large-Similarity-Relation (_⊔_) Cardinal
+large-similarity-relation-Cardinal =
+  λ where
+    .large-equivalence-relation-Large-Similarity-Relation →
+      large-equivalence-relation-Cardinal
+    .eq-sim-Large-Similarity-Relation →
+      eq-sim-Cardinal
+```
+
+## External links
+
+- [Cardinality](https://en.wikipedia.org/wiki/Cardinality) at Wikipedia
+- [cardinal number](https://ncatlab.org/nlab/show/cardinal+number) at $n$Lab
diff --git a/src/set-theory/inequality-cardinals.lagda.md b/src/set-theory/inequality-cardinals.lagda.md
new file mode 100644
index 00000000000..a12e340c19a
--- /dev/null
+++ b/src/set-theory/inequality-cardinals.lagda.md
@@ -0,0 +1,242 @@
+# Inequality on cardinals
+
+```agda
+module set-theory.inequality-cardinals where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+We say a [cardinal of sets](set-theory.cardinals.md) `X` is
+{{#concept "less than or equal to" Agda=leq-Cardinal}} a cardinal `Y` if any
+[set](foundation-core.sets.md) in the isomorphism class represented by `X`
+embeds into any set in the isomorphism class represented by `Y`. This defines
+the {{#concept "standard ordering" Disambiguation="on cardinalities of sets"}}
+on cardinalities of sets.
+
+Under the assumption of the
+[law of excluded middle](foundation.law-of-excluded-middle.md), this relation is
+antisymmetric and hence defines a [partial order](order-theory.posets.md) on
+cardinalites.
+
+## Definition
+
+### Boundedness of the cardinality of a set
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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.
+
+```agda
+module _
+  {l : Level} (lem : 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
+
+```agda
+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
+
+- [Complemented inequality of cardinals](set-theory.complemented-inequality-cardinals.md)
+
+## External links
+
+- [Cardinality](https://en.wikipedia.org/wiki/Cardinality) at Wikipedia
+- [cardinal number](https://ncatlab.org/nlab/show/cardinal+number) at $n$Lab
diff --git a/src/set-theory/infinite-sets.lagda.md b/src/set-theory/infinite-sets.lagda.md
index d94e6be82f9..0016b645382 100644
--- a/src/set-theory/infinite-sets.lagda.md
+++ b/src/set-theory/infinite-sets.lagda.md
@@ -24,7 +24,7 @@ open import univalent-combinatorics.standard-finite-types
 
 A [set](foundation-core.sets.md) `A` is said to be
 {{#concept "infinite" Disambiguation="set" WD="infinite set" WDID=Q205140}} if
-it contains arbitrarily [large](set-theory.cardinalities.md)
+it contains arbitrarily [large](set-theory.cardinals.md)
 [finite](univalent-combinatorics.finite-types.md)
 [subsets](foundation-core.subtypes.md).
 
diff --git a/src/univalent-combinatorics/complements-isolated-elements.lagda.md b/src/univalent-combinatorics/complements-isolated-elements.lagda.md
index c993815344f..2a12c8eb1fb 100644
--- a/src/univalent-combinatorics/complements-isolated-elements.lagda.md
+++ b/src/univalent-combinatorics/complements-isolated-elements.lagda.md
@@ -27,7 +27,7 @@ open import univalent-combinatorics.finite-types
 ## Idea
 
 For any element `x` in a [finite type](univalent-combinatorics.finite-types.md)
-`X` of [cardinality](set-theory.cardinalities.md) `n+1`, we can construct its
+`X` of [cardinality](set-theory.cardinals.md) `n+1`, we can construct its
 **complement**, which is a type of cardinality `n`.
 
 ## Definition
diff --git a/src/univalent-combinatorics/ferrers-diagrams.lagda.md b/src/univalent-combinatorics/ferrers-diagrams.lagda.md
index 57d99eae92a..4d2809e13ea 100644
--- a/src/univalent-combinatorics/ferrers-diagrams.lagda.md
+++ b/src/univalent-combinatorics/ferrers-diagrams.lagda.md
@@ -40,7 +40,7 @@ ferrers diagram of a [finite type](univalent-combinatorics.finite-types.md) `A`
 consists of a finite type `X` and a family `Y` of inhabited finite types over
 `X` such that `Σ X Y` is merely equivalent to `A`. The number of finite Ferrers
 diagrams of `A` is the [partition number](univalent-combinatorics.partitions.md)
-of the [cardinality](set-theory.cardinalities.md) of `A`.
+of the [cardinality](set-theory.cardinals.md) of `A`.
 
 ## Definition
 
diff --git a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md
index 7e7423d0377..d8e33ac8d4e 100644
--- a/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md
+++ b/src/univalent-combinatorics/kuratowski-finite-sets.lagda.md
@@ -22,7 +22,9 @@ open import foundation.sets
 open import foundation.surjective-maps
 open import foundation.universe-levels
 
-open import set-theory.cardinalities
+open import set-theory.cardinals
+open import set-theory.equality-cardinals
+open import set-theory.inequality-cardinals
 
 open import univalent-combinatorics.dedekind-finite-sets
 open import univalent-combinatorics.dedekind-finite-types
@@ -167,7 +169,7 @@ module _
 
 ```agda
 cardinality-Kuratowski-Finite-Set :
-  {l : Level} → Kuratowski-Finite-Set l → cardinal l
+  {l : Level} → Kuratowski-Finite-Set l → Cardinal l
 cardinality-Kuratowski-Finite-Set X =
   cardinality (set-Kuratowski-Finite-Set X)
 
@@ -177,11 +179,11 @@ module _
 
   antisymmetric-leq-cardinality-Kuratowski-Finite-Set :
     leq-cardinality
-      ( cardinality-Kuratowski-Finite-Set X)
-      ( cardinality-Kuratowski-Finite-Set Y) →
+      ( set-Kuratowski-Finite-Set X)
+      ( set-Kuratowski-Finite-Set Y) →
     leq-cardinality
-      ( cardinality-Kuratowski-Finite-Set Y)
-      ( cardinality-Kuratowski-Finite-Set X) →
+      ( set-Kuratowski-Finite-Set Y)
+      ( set-Kuratowski-Finite-Set X) →
     cardinality-Kuratowski-Finite-Set X ＝
     cardinality-Kuratowski-Finite-Set Y
   antisymmetric-leq-cardinality-Kuratowski-Finite-Set p q =