A constructive Cantor–Schröder–Bernstein theorem

references.bib

@@ -562,6 +562,17 @@ @article{KECA17
   keywords      = {Computer Science - Logic in Computer Science ; 03B15 ; F.4.1},
 }
 
+@article{König1906,
+  title         = {Sur la théorie des ensembles},
+  author        = {J. König},
+  year          = 1906,
+  journal       = {Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences},
+  volume        = 143,
+  pages         = {110--112},
+  url           = {https://gallica.bnf.fr/ark:/12148/bpt6k30977.image.f110.langEN},
+  language      = {french},
+}
+
 @inproceedings{Kraus15,
   title         = {{The General Universal Property of the Propositional Truncation}},
   author        = {Kraus, Nicolai},

src/foundation-core/contractible-maps.lagda.md

@@ -20,6 +20,7 @@ open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.retractions
 open import foundation-core.sections
+open import foundation-core.torsorial-type-families
 ```
 
 </details>
@@ -134,6 +135,18 @@ module _
       is-contr-map-is-coherently-invertible ∘ is-coherently-invertible-is-equiv
 ```
 
+### The identity function is contractible
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  abstract
+    is-contr-map-id : is-contr-map (id {A = A})
+    is-contr-map-id = is-torsorial-Id'
+```
+
 ## See also
 
 - For the notion of biinvertible maps see

src/foundation-core/injective-maps.lagda.md

@@ -179,7 +179,7 @@ module _
   where
 
   is-equiv-is-injective : {f : A → B} → section f → is-injective f → is-equiv f
-  is-equiv-is-injective {f} (pair g G) H =
+  is-equiv-is-injective {f} (g , G) H =
     is-equiv-is-invertible g G (λ x → H (G (f x)))
 ```
 

src/foundation-core/propositional-maps.lagda.md

@@ -15,6 +15,7 @@ open import foundation.universe-levels
 open import foundation-core.contractible-types
 open import foundation-core.embeddings
 open import foundation-core.fibers-of-maps
+open import foundation-core.function-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
 ```
@@ -129,3 +130,10 @@ module _
   pr1 (fiber-emb-Prop' f y) = fiber' (map-emb f) y
   pr2 (fiber-emb-Prop' f y) = is-prop-map-emb' f y
 ```
+
+### The identity function is propositional
+
+```agda
+is-prop-map-id : {l : Level} {X : UU l} → is-prop-map (id' X)
+is-prop-map-id = is-prop-map-is-emb is-emb-id
+```

src/foundation-core/truncated-maps.lagda.md

@@ -97,6 +97,13 @@ module _
   is-trunc-map-equiv e = is-trunc-map-is-equiv (is-equiv-map-equiv e)
 ```
 
+### The identity function is `k`-truncated
+
+```agda
+is-trunc-map-id : {l : Level} (k : 𝕋) {X : UU l} → is-trunc-map k (id' X)
+is-trunc-map-id k = is-trunc-map-is-equiv k is-equiv-id
+```
+
 ### A map is `k+1`-truncated if and only if its action on identifications is `k`-truncated
 
 ```agda

src/foundation.lagda.md

@@ -48,6 +48,7 @@ open import foundation.binary-relations-with-lifts public
 open import foundation.binary-transport public
 open import foundation.binary-type-duality public
 open import foundation.booleans public
+open import foundation.cantor-schroder-bernstein-decidable-embeddings public
 open import foundation.cantor-schroder-bernstein-escardo public
 open import foundation.cantors-theorem public
 open import foundation.cartesian-morphisms-arrows public

src/foundation/0-connected-types.lagda.md

@@ -41,8 +41,11 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A type is said to be connected if its type of connected components, i.e., its
-set truncation, is contractible.
+A type is said to be
+{{#concept "0-connected" Disambiguation="type" Agda=is-0-connected}} if its type
+of [connected components](foundation.connected-components.md), i.e., its
+[set truncation](foundation.set-truncations.md), is
+[contractible](foundation-core.contractible-types.md).
 
 ```agda
 is-0-connected-Prop : {l : Level} → UU l → Prop l
@@ -65,7 +68,7 @@ abstract
 
 abstract
   mere-eq-is-0-connected :
-    {l : Level} {A : UU l} → is-0-connected A → (x y : A) → mere-eq x y
+    {l : Level} {A : UU l} → is-0-connected A → all-elements-merely-equal A
   mere-eq-is-0-connected {A = A} H x y =
     apply-effectiveness-unit-trunc-Set (eq-is-contr H)
 
@@ -83,7 +86,7 @@ abstract
 abstract
   is-0-connected-mere-eq-is-inhabited :
     {l : Level} {A : UU l} →
-    is-inhabited A → ((x y : A) → mere-eq x y) → is-0-connected A
+    is-inhabited A → all-elements-merely-equal A → is-0-connected A
   is-0-connected-mere-eq-is-inhabited H K =
     apply-universal-property-trunc-Prop H
       ( is-0-connected-Prop _)