Complemented inequality of cardinalities

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

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})

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)
 ```

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)
+```

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)
 ```

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

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