diff --git a/references.bib b/references.bib
index fac2c5e383..ac1ee65322 100644
--- a/references.bib
+++ b/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},
diff --git a/src/foundation-core/contractible-maps.lagda.md b/src/foundation-core/contractible-maps.lagda.md
index 2c2d1e9c41..898e0b2f67 100644
--- a/src/foundation-core/contractible-maps.lagda.md
+++ b/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
diff --git a/src/foundation-core/injective-maps.lagda.md b/src/foundation-core/injective-maps.lagda.md
index 508ff7325c..f1e6ffe6a0 100644
--- a/src/foundation-core/injective-maps.lagda.md
+++ b/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)))
 ```
 
diff --git a/src/foundation-core/propositional-maps.lagda.md b/src/foundation-core/propositional-maps.lagda.md
index 3c00a25216..65f367adc5 100644
--- a/src/foundation-core/propositional-maps.lagda.md
+++ b/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
+```
diff --git a/src/foundation-core/truncated-maps.lagda.md b/src/foundation-core/truncated-maps.lagda.md
index 6c68755acc..068c7c04d2 100644
--- a/src/foundation-core/truncated-maps.lagda.md
+++ b/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
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index cd01e10694..f63911de8f 100644
--- a/src/foundation.lagda.md
+++ b/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
diff --git a/src/foundation/0-connected-types.lagda.md b/src/foundation/0-connected-types.lagda.md
index d2bdc9203d..756f782225 100644
--- a/src/foundation/0-connected-types.lagda.md
+++ b/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 _)
diff --git a/src/foundation/cantor-schroder-bernstein-decidable-embeddings.lagda.md b/src/foundation/cantor-schroder-bernstein-decidable-embeddings.lagda.md
new file mode 100644
index 0000000000..f7004e76e7
--- /dev/null
+++ b/src/foundation/cantor-schroder-bernstein-decidable-embeddings.lagda.md
@@ -0,0 +1,351 @@
+# The Cantor–Schröder–Bernstein theorem for decidable embeddings
+
+```agda
+module foundation.cantor-schroder-bernstein-decidable-embeddings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.decidable-embeddings
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.double-negation-dense-equality-maps
+open import foundation.double-negation-images
+open import foundation.function-types
+open import foundation.injective-maps
+open import foundation.perfect-images
+open import foundation.retracts-of-types
+open import foundation.sections
+open import foundation.universe-levels
+open import foundation.weak-limited-principle-of-omniscience
+
+open import foundation-core.coproduct-types
+open import foundation-core.empty-types
+open import foundation-core.equivalences
+open import foundation-core.identity-types
+open import foundation-core.negation
+
+open import logic.double-negation-eliminating-maps
+open import logic.double-negation-stable-embeddings
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "Cantor–Schröder–Bernstein theorem" Disambiguation="for decidable embeddings" Agda=Cantor-Schröder-Bernstein-WLPO}}
+for [decidable embeddings](foundation.decidable-embeddings.md) states that,
+assuming the
+[weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md)
+(WLPO), then if two types `A` and `B` mutually embed via
+[embeddings](foundation-core.embeddings.md) whose
+[fibers](foundation.fibers-of-maps.md) are
+[decidable](foundation.decidable-types.md), then `A` and `B` are
+[equivalent](foundation-core.equivalences.md) types.
+
+Classically, i.e., under the assumption of the
+[law of excluded middle](foundation.law-of-excluded-middle.md), the
+Cantor–Schröder–Bernstein theorem asserts that from any pair of
+[injective maps](foundation-core.injective-maps.md) between
+[sets](foundation-core.sets.md) `f : A → B` and `g : B → A` we can construct a
+bijection between `A` and `B`. In a recent generalization, Martín Escardó proved
+that the Cantor–Schröder–Bernstein theorem also holds for ∞-groupoids
+{{#cite Esc21}}. His generalization asserts that given two types that
+[embed](foundation-core.embeddings.md) into each other, then the types are
+[equivalent](foundation-core.equivalences.md).
+
+In this file we give a fine-grained deconstruction of the construction used in
+the proof of this
+[Cantor–Schröder–Bernstein-Escardó theorem](foundation.cantor-schroder-bernstein-escardo.md),
+originally due to König {{#cite König1906}}, and use this to give the
+generalization of the theorem for
+[decidable embeddings](foundation.decidable-embeddings.md) under the assumption
+of the weak limited principle of omniscience.
+
+## Construction
+
+Given a pair of mutually converse maps `f : A → B` and `g : B → A` such that
+
+1. the maps `f` and `g` satisfy double negation elimination on their fibers
+2. `f` has double negation dense equality
+3. `g` is injective
+4. the [perfect image](foundation.perfect-images.md) of `g` relative to `f` is
+   decidable
+
+then `B` is a retract of `A`. If `f` moreover is injective, then this retract is
+an equivalence.
+
+This can be understood as an entirely constructive formulation of the
+Cantor–Schröder–Bernstein theorem.
+
+The reader may also note that under the additional assumption of
+[function extensionality](foundation.function-extensionality.md), double
+negation eliminating injections are double negation stable embeddings.
+
+The underlying map `A → B` of the construction.
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  where
+
+  map-construction-Cantor-Schröder-Bernstein' :
+    (x : A) → is-decidable (is-perfect-image f g x) → B
+  map-construction-Cantor-Schröder-Bernstein' x (inl γ) =
+    inverse-of-perfect-image x γ
+  map-construction-Cantor-Schröder-Bernstein' x (inr nγ) =
+    f x
+
+  map-construction-Cantor-Schröder-Bernstein :
+    (D : (x : A) → is-decidable (is-perfect-image f g x)) → A → B
+  map-construction-Cantor-Schröder-Bernstein D x =
+    map-construction-Cantor-Schröder-Bernstein' x (D x)
+```
+
+Computing the underlying map `A → B` of the construction.
+
+```agda
+  compute-map-construction-Cantor-Schröder-Bernstein' :
+    (G' : is-injective g) →
+    (y : B) →
+    (γ : is-perfect-image f g (g y)) →
+    (d : is-decidable (is-perfect-image f g (g y))) →
+    map-construction-Cantor-Schröder-Bernstein'
+      ( g y) d ＝
+    y
+  compute-map-construction-Cantor-Schröder-Bernstein' G' y γ (inl v') =
+    is-retraction-inverse-of-perfect-image G' y v'
+  compute-map-construction-Cantor-Schröder-Bernstein' G' y γ (inr v) =
+    ex-falso (v γ)
+
+  compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein :
+    (G : is-double-negation-eliminating-map g)
+    (G' : is-injective g)
+    (F : is-double-negation-eliminating-map f)
+    (F' : has-double-negation-dense-equality-map f) →
+    (y : B) →
+    (nγ : ¬ (is-perfect-image f g (g y))) →
+    (d :
+      is-decidable
+        ( is-perfect-image f g
+          ( element-has-not-perfect-fiber-is-not-perfect-image
+              G G' F F' y nγ))) →
+    map-construction-Cantor-Schröder-Bernstein'
+      ( element-has-not-perfect-fiber-is-not-perfect-image G G' F F' y nγ)
+      ( d) ＝
+    y
+  compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein
+    G G' F F' y nγ (inl v) =
+    ex-falso
+      ( is-not-perfect-image-has-not-perfect-fiber-is-not-perfect-image
+          G G' F F' y nγ v)
+  compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein
+    G G' F F' y nγ (inr _) =
+    is-in-fiber-element-has-not-perfect-fiber-is-not-perfect-image
+      G G' F F' y nγ
+```
+
+The underlying section `B → A` of the construction.
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  (G : is-double-negation-eliminating-map g)
+  (G' : is-injective g)
+  (F : is-double-negation-eliminating-map f)
+  (F' : has-double-negation-dense-equality-map f)
+  where
+
+  map-section-construction-Cantor-Schröder-Bernstein' :
+    (y : B) → is-decidable (is-perfect-image f g (g y)) → A
+  map-section-construction-Cantor-Schröder-Bernstein' y (inl _) =
+    g y
+  map-section-construction-Cantor-Schröder-Bernstein' y (inr nγ) =
+    element-has-not-perfect-fiber-is-not-perfect-image G G' F F' y nγ
+
+  map-section-construction-Cantor-Schröder-Bernstein :
+    (D : (y : B) → is-decidable (is-perfect-image f g (g y))) →
+    B → A
+  map-section-construction-Cantor-Schröder-Bernstein D y =
+    map-section-construction-Cantor-Schröder-Bernstein' y (D y)
+
+  is-section-map-section-construction-Cantor-Schröder-Bernstein' :
+    (y : B)
+    (d : is-decidable (is-perfect-image f g (g y))) →
+    (d' :
+      is-decidable
+        ( is-perfect-image f g
+          ( map-section-construction-Cantor-Schröder-Bernstein' y d))) →
+    map-construction-Cantor-Schröder-Bernstein'
+      ( map-section-construction-Cantor-Schröder-Bernstein' y d)
+      ( d') ＝
+    y
+  is-section-map-section-construction-Cantor-Schröder-Bernstein' y (inl γ) =
+    compute-map-construction-Cantor-Schröder-Bernstein' G' y γ
+  is-section-map-section-construction-Cantor-Schröder-Bernstein' y (inr nγ) =
+    compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein
+      G G' F F' y nγ
+
+  is-section-map-section-construction-Cantor-Schröder-Bernstein :
+    (D : (x : A) → is-decidable (is-perfect-image f g x)) →
+    is-section
+      ( map-construction-Cantor-Schröder-Bernstein D)
+      ( map-section-construction-Cantor-Schröder-Bernstein (D ∘ g))
+  is-section-map-section-construction-Cantor-Schröder-Bernstein D y =
+    is-section-map-section-construction-Cantor-Schröder-Bernstein' y
+      ( D (g y))
+      ( D (map-section-construction-Cantor-Schröder-Bernstein (D ∘ g) y))
+
+  section-construction-Cantor-Schröder-Bernstein :
+    (D : (x : A) → is-decidable (is-perfect-image f g x)) →
+    section (map-construction-Cantor-Schröder-Bernstein D)
+  section-construction-Cantor-Schröder-Bernstein D =
+    ( map-section-construction-Cantor-Schröder-Bernstein (D ∘ g) ,
+      is-section-map-section-construction-Cantor-Schröder-Bernstein D)
+
+  retract-construction-Cantor-Schröder-Bernstein :
+    (D : (x : A) → is-decidable (is-perfect-image f g x)) →
+    B retract-of A
+  retract-construction-Cantor-Schröder-Bernstein D =
+    retract-section
+      ( map-construction-Cantor-Schröder-Bernstein D)
+      ( section-construction-Cantor-Schröder-Bernstein D)
+```
+
+Injectivity of the constructed map.
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  (F' : is-injective f)
+  where
+
+  is-injective-map-construction-Cantor-Schröder-Bernstein' :
+    {x x' : A}
+    (d : is-decidable (is-perfect-image f g x))
+    (d' : is-decidable (is-perfect-image f g x')) →
+    map-construction-Cantor-Schröder-Bernstein' x d ＝
+    map-construction-Cantor-Schröder-Bernstein' x' d' →
+    x ＝ x'
+  is-injective-map-construction-Cantor-Schröder-Bernstein'
+    {x} {x'} (inl ρ) (inl ρ') p =
+    ( inv (is-section-inverse-of-perfect-image x ρ)) ∙
+    ( ap g p) ∙
+    ( is-section-inverse-of-perfect-image x' ρ')
+  is-injective-map-construction-Cantor-Schröder-Bernstein'
+    {x} {x'} (inl ρ) (inr nρ') p =
+    ex-falso (perfect-image-has-distinct-image x' x nρ' ρ (inv p))
+  is-injective-map-construction-Cantor-Schröder-Bernstein'
+    {x} {x'} (inr nρ) (inl ρ') p =
+    ex-falso (perfect-image-has-distinct-image x x' nρ ρ' p)
+  is-injective-map-construction-Cantor-Schröder-Bernstein'
+    {x} {x'} (inr nρ) (inr nρ') p =
+    F' p
+```
+
+Piecing it all together.
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  (G : is-double-negation-eliminating-map g)
+  (G' : is-injective g)
+  (F : is-double-negation-eliminating-map f)
+  (F'' : is-injective f)
+  (D : (x : A) → is-decidable (is-perfect-image f g x))
+  where
+
+  is-equiv-map-construction-Cantor-Schröder-Bernstein :
+    is-equiv (map-construction-Cantor-Schröder-Bernstein D)
+  is-equiv-map-construction-Cantor-Schröder-Bernstein =
+    is-equiv-is-injective
+      ( section-construction-Cantor-Schröder-Bernstein G G' F
+        ( has-double-negation-dense-equality-map-is-emb
+          ( is-emb-is-injective-is-double-negation-eliminating-map F F''))
+        ( D))
+      ( λ {x} {x'} →
+        is-injective-map-construction-Cantor-Schröder-Bernstein' F''
+          ( D x)
+          ( D x'))
+
+  equiv-construction-Cantor-Schröder-Bernstein : A ≃ B
+  equiv-construction-Cantor-Schröder-Bernstein =
+    ( map-construction-Cantor-Schröder-Bernstein D ,
+      is-equiv-map-construction-Cantor-Schröder-Bernstein)
+```
+
+## Theorem
+
+It follows from the weak limited principle of omniscience that, for every pair
+of mutual decidable embeddings `f : A ↪ B` and `g : B ↪ A`, it is decidable
+for every element `x : A` whether `x` is a perfect image of `g` relative to `f`.
+Applying this fact to the Cantor-Schröder-Bernstein construction, we conclude
+with the main result.
+
+```agda
+module _
+  {l1 l2 : Level} (wlpo : level-WLPO (l1 ⊔ l2))
+  {A : UU l1} {B : UU l2}
+  where
+
+  abstract
+    Cantor-Schröder-Bernstein-WLPO' :
+      {f : A → B} {g : B → A} →
+      is-decidable-emb g →
+      is-decidable-emb f →
+      A ≃ B
+    Cantor-Schröder-Bernstein-WLPO' G F =
+      equiv-construction-Cantor-Schröder-Bernstein
+        ( is-double-negation-eliminating-map-is-decidable-emb G)
+        ( is-injective-is-decidable-emb G)
+        ( is-double-negation-eliminating-map-is-decidable-emb F)
+        ( is-injective-is-decidable-emb F)
+        ( is-decidable-is-perfect-image-WLPO wlpo
+          ( G)
+          ( is-decidable-map-is-decidable-emb F)
+          ( has-double-negation-dense-equality-map-is-emb
+            ( is-emb-is-decidable-emb F)))
+
+    Cantor-Schröder-Bernstein-WLPO : (A ↪ᵈ B) → (B ↪ᵈ A) → A ≃ B
+    Cantor-Schröder-Bernstein-WLPO (f , F) (g , G) =
+      Cantor-Schröder-Bernstein-WLPO' G F
+```
+
+## References
+
+- Escardó's formalizations of this theorem can be found at
+  <https://www.cs.bham.ac.uk/~mhe/TypeTopology/CantorSchroederBernstein.index.html>.
+  {{#cite TypeTopology}}
+
+{{#bibliography}}
+
+## See also
+
+The Cantor–Schröder–Bernstein theorem holds constructively for many notions of
+finite type, including
+
+- [Dedekind finite types](univalent-combinatorics.dedekind-finite-types.md)
+- [Finite types](univalent-combinatorics.finite-types.md) (unformalized)
+- [Finitely enumerable types](univalent-combinatorics.finitely-enumerable-types.md)
+- [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md)
+- [Subfinite types](univalent-combinatorics.subfinite-types.md)
+- [Subfinitely enumerable types](univalent-combinatorics.subfinitely-enumerable-types.md)
+
+## External links
+
+- See also the twin formalization in TypeTopology at
+  [`CantorSchroederBernstein.CSB-WLPO`](https://martinescardo.github.io/TypeTopology/CantorSchroederBernstein.CSB-WLPO.html).
+  There it is verified that the construction does not depend on any other axioms
+  than WLPO, and the assumption that `f` has double negation dense equality on
+  fibers is somewhat further weakened.
+
+- The Cantor–Schröder–Bernstein theorem is the 25th theorem on
+  [Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+  [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
index 0c4e86cd9b..e5e25491a8 100644
--- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
+++ b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
@@ -7,22 +7,21 @@ module foundation.cantor-schroder-bernstein-escardo where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
-open import foundation.decidable-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.cantor-schroder-bernstein-decidable-embeddings
+open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.injective-maps
 open import foundation.law-of-excluded-middle
-open import foundation.perfect-images
-open import foundation.split-surjective-maps
+open import foundation.propositions
 open import foundation.universe-levels
 
-open import foundation-core.coproduct-types
 open import foundation-core.embeddings
-open import foundation-core.empty-types
 open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
-open import foundation-core.identity-types
-open import foundation-core.negation
+open import foundation-core.propositional-maps
 open import foundation-core.sets
 ```
 
@@ -38,144 +37,29 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for
 [embed](foundation-core.embeddings.md) into each other, then the types are
 [equivalent](foundation-core.equivalences.md). {{#cite Esc21}}
 
-The Cantor–Schröder–Bernstein theorem is the
-[25th](literature.100-theorems.md#25) theorem on
-[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
-[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+## Theorem
 
-## Statement
-
-```agda
-type-Cantor-Schröder-Bernstein-Escardó : (l1 l2 : Level) → UU (lsuc (l1 ⊔ l2))
-type-Cantor-Schröder-Bernstein-Escardó l1 l2 =
-  {X : UU l1} {Y : UU l2} → (X ↪ Y) → (Y ↪ X) → X ≃ Y
-```
-
-## Proof
-
-### The law of excluded middle implies Cantor-Schröder-Bernstein-Escardó
+### The Cantor-Schröder-Bernstein-Escardó theorem
 
 ```agda
 module _
   {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
-  where
-
-  module _
-    {X : UU l1} {Y : UU l2} (f : X ↪ Y) (g : Y ↪ X)
-    where
-
-    map-Cantor-Schröder-Bernstein-Escardó' :
-      (x : X) → is-decidable (is-perfect-image (map-emb f) (map-emb g) x) → Y
-    map-Cantor-Schröder-Bernstein-Escardó' x (inl y) =
-      inverse-of-perfect-image x y
-    map-Cantor-Schröder-Bernstein-Escardó' x (inr y) =
-      map-emb f x
-
-    map-Cantor-Schröder-Bernstein-Escardó :
-      X → Y
-    map-Cantor-Schröder-Bernstein-Escardó x =
-      map-Cantor-Schröder-Bernstein-Escardó' x
-        ( is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x)
-
-    is-injective-map-Cantor-Schröder-Bernstein-Escardó :
-      is-injective map-Cantor-Schröder-Bernstein-Escardó
-    is-injective-map-Cantor-Schröder-Bernstein-Escardó {x} {x'} =
-      l (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x)
-      (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x')
-      where
-      l :
-        (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x))
-        (d' : is-decidable (is-perfect-image (map-emb f) (map-emb g) x')) →
-        ( map-Cantor-Schröder-Bernstein-Escardó' x d) ＝
-        ( map-Cantor-Schröder-Bernstein-Escardó' x' d') →
-        x ＝ x'
-      l (inl ρ) (inl ρ') p =
-        inv (is-section-inverse-of-perfect-image x ρ) ∙
-          (ap (map-emb g) p ∙ is-section-inverse-of-perfect-image x' ρ')
-      l (inl ρ) (inr nρ') p =
-        ex-falso (perfect-image-has-distinct-image x' x nρ' ρ (inv p))
-      l (inr nρ) (inl ρ') p =
-        ex-falso (perfect-image-has-distinct-image x x' nρ ρ' p)
-      l (inr nρ) (inr nρ') p =
-        is-injective-is-emb (is-emb-map-emb f) p
-
-    is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó :
-      is-split-surjective map-Cantor-Schröder-Bernstein-Escardó
-    is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó y =
-      pair x p
-      where
-      a :
-        is-decidable
-          ( is-perfect-image (map-emb f) (map-emb g) (map-emb g y)) →
-        Σ ( X)
-          ( λ x →
-            ( (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) →
-              map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y))
-      a (inl γ) =
-        pair (map-emb g y) ψ
-        where
-        ψ :
-          ( d :
-            is-decidable
-              ( is-perfect-image (map-emb f) (map-emb g) (map-emb g y))) →
-          map-Cantor-Schröder-Bernstein-Escardó' (map-emb g y) d ＝ y
-        ψ (inl v') =
-          is-retraction-inverse-of-perfect-image
-            { is-emb-g = is-emb-map-emb g}
-            ( y)
-            ( v')
-        ψ (inr v) = ex-falso (v γ)
-      a (inr γ) =
-        pair x ψ
-        where
-        w :
-          Σ ( fiber (map-emb f) y)
-            ( λ s → ¬ (is-perfect-image (map-emb f) (map-emb g) (pr1 s)))
-        w =
-          not-perfect-image-has-not-perfect-fiber
-            ( is-emb-map-emb f)
-            ( is-emb-map-emb g)
-            ( lem)
-            ( y)
-            ( γ)
-        x : X
-        x = pr1 (pr1 w)
-        p : map-emb f x ＝ y
-        p = pr2 (pr1 w)
-        ψ :
-          ( d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) →
-          map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y
-        ψ (inl v) = ex-falso ((pr2 w) v)
-        ψ (inr v) = p
-      b :
-        Σ ( X)
-          ( λ x →
-            ( (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) →
-              map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y))
-      b =
-        a ( is-decidable-is-perfect-image-is-emb
-            ( is-emb-map-emb g)
-            ( lem)
-            ( map-emb g y))
-      x : X
-      x = pr1 b
-      p : map-Cantor-Schröder-Bernstein-Escardó x ＝ y
-      p = pr2 b (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x)
-
-    is-equiv-map-Cantor-Schröder-Bernstein-Escardó :
-      is-equiv map-Cantor-Schröder-Bernstein-Escardó
-    is-equiv-map-Cantor-Schröder-Bernstein-Escardó =
-      is-equiv-is-split-surjective-is-injective
-        map-Cantor-Schröder-Bernstein-Escardó
-        is-injective-map-Cantor-Schröder-Bernstein-Escardó
-        is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó
+  {A : UU l1} {B : UU l2}
+  where abstract
+
+  Cantor-Schröder-Bernstein-Escardó' :
+    {f : A → B} {g : B → A} →
+    is-emb g → is-emb f → A ≃ B
+  Cantor-Schröder-Bernstein-Escardó' {f} {g} G F =
+    Cantor-Schröder-Bernstein-WLPO'
+      ( λ P → lem (Π-Prop ℕ (prop-Decidable-Prop ∘ P)))
+      ( G , λ y → lem (fiber g y , is-prop-map-is-emb G y))
+      ( F , λ y → lem (fiber f y , is-prop-map-is-emb F y))
 
   Cantor-Schröder-Bernstein-Escardó :
-    type-Cantor-Schröder-Bernstein-Escardó l1 l2
-  pr1 (Cantor-Schröder-Bernstein-Escardó f g) =
-    map-Cantor-Schröder-Bernstein-Escardó f g
-  pr2 (Cantor-Schröder-Bernstein-Escardó f g) =
-    is-equiv-map-Cantor-Schröder-Bernstein-Escardó f g
+    A ↪ B → B ↪ A → A ≃ B
+  Cantor-Schröder-Bernstein-Escardó (f , F) (g , G) =
+    Cantor-Schröder-Bernstein-Escardó' G F
 ```
 
 ## Corollaries
@@ -183,19 +67,24 @@ module _
 ### The Cantor–Schröder–Bernstein theorem
 
 ```agda
-Cantor-Schröder-Bernstein :
+module _
   {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
-  (A : Set l1) (B : Set l2) →
-  injection (type-Set A) (type-Set B) →
-  injection (type-Set B) (type-Set A) →
-  (type-Set A) ≃ (type-Set B)
-Cantor-Schröder-Bernstein lem A B f g =
-  Cantor-Schröder-Bernstein-Escardó lem (emb-injection B f) (emb-injection A g)
+  (A : Set l1) (B : Set l2)
+  where abstract
+
+  Cantor-Schröder-Bernstein :
+    injection (type-Set A) (type-Set B) →
+    injection (type-Set B) (type-Set A) →
+    (type-Set A) ≃ (type-Set B)
+  Cantor-Schröder-Bernstein f g =
+    Cantor-Schröder-Bernstein-Escardó lem
+      ( emb-injection B f)
+      ( emb-injection A g)
 ```
 
 ## References
 
-- Escardó's formalizations regarding this theorem can be found at
+- Escardó's formalizations of this theorem can be found at
   <https://www.cs.bham.ac.uk/~mhe/TypeTopology/CantorSchroederBernstein.index.html>.
   {{#cite TypeTopology}}
 
@@ -206,8 +95,15 @@ Cantor-Schröder-Bernstein lem A B f g =
 The Cantor–Schröder–Bernstein–Escardó theorem holds constructively for many
 notions of finite type, including
 
+- [Dedekind finite types](univalent-combinatorics.dedekind-finite-types.md)
 - [Finite types](univalent-combinatorics.finite-types.md) (unformalized)
-- [Subfinite types](univalent-combinatorics.subfinite-types.md)
+- [Finitely enumerable types](univalent-combinatorics.finitely-enumerable-types.md)
 - [Kuratowski finite sets](univalent-combinatorics.kuratowski-finite-sets.md)
+- [Subfinite types](univalent-combinatorics.subfinite-types.md)
 - [Subfinitely enumerable types](univalent-combinatorics.subfinitely-enumerable-types.md)
-- [Dedekind finite types](univalent-combinatorics.dedekind-finite-types.md)
+
+## External links
+
+- The Cantor–Schröder–Bernstein theorem is the 25th theorem on
+  [Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+  [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
diff --git a/src/foundation/decidable-dependent-pair-types.lagda.md b/src/foundation/decidable-dependent-pair-types.lagda.md
index 14a85748f4..445c747101 100644
--- a/src/foundation/decidable-dependent-pair-types.lagda.md
+++ b/src/foundation/decidable-dependent-pair-types.lagda.md
@@ -53,7 +53,7 @@ module _
   is-decidable-Σ-equiv' = is-decidable-equiv (equiv-Σ D e f)
 ```
 
-### Dependent sums of a uniformly decidable family of types
+### Dependent sums of uniformly decidable families of types
 
 ```agda
 is-decidable-Σ-uniformly-decidable-family :
diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md
index a58beedcbb..70856d62e2 100644
--- a/src/foundation/decidable-embeddings.lagda.md
+++ b/src/foundation/decidable-embeddings.lagda.md
@@ -55,7 +55,7 @@ if it is an [embedding](foundation-core.embeddings.md) and its
 Equivalently, a decidable embedding is a map whose fibers are
 [decidable propositions](foundation-core.decidable-propositions.md). We refer to
 this condition as being a
-{{#concept "decidably propositional map" Disambiguation="of types" Agda=is-decidable-prop-map}}.
+{{#concept "decidable propositional map" Disambiguation="of types" Agda=is-decidable-prop-map}}.
 
 ## Definitions
 
@@ -82,7 +82,7 @@ is-injective-is-decidable-emb :
 is-injective-is-decidable-emb = is-injective-is-emb ∘ is-emb-is-decidable-emb
 ```
 
-### Decidably propositional maps
+### Decidable propositional maps
 
 ```agda
 module _
@@ -141,6 +141,11 @@ module _
   is-decidable-map-map-decidable-emb =
     is-decidable-map-is-decidable-emb is-decidable-emb-map-decidable-emb
 
+  is-injective-map-decidable-emb :
+    is-injective map-decidable-emb
+  is-injective-map-decidable-emb =
+    is-injective-is-decidable-emb is-decidable-emb-map-decidable-emb
+
   emb-decidable-emb : X ↪ Y
   emb-decidable-emb = map-decidable-emb , is-emb-map-decidable-emb
 ```
diff --git a/src/foundation/decidable-maps.lagda.md b/src/foundation/decidable-maps.lagda.md
index aae4c0c21e..89cb4cd718 100644
--- a/src/foundation/decidable-maps.lagda.md
+++ b/src/foundation/decidable-maps.lagda.md
@@ -7,18 +7,24 @@ module foundation.decidable-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-morphisms-arrows
 open import foundation.coproduct-types
 open import foundation.decidable-equality
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
+open import foundation.double-negation-dense-equality-maps
 open import foundation.embeddings
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-coproduct-types
 open import foundation.hilbert-epsilon-operators-maps
 open import foundation.identity-types
+open import foundation.iterating-functions
+open import foundation.propositional-truncations
 open import foundation.retracts-of-maps
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import foundation-core.contractible-maps
@@ -43,7 +49,7 @@ A [map](foundation-core.function-types.md) is said to be
 its [fibers](foundation-core.fibers-of-maps.md) are
 [decidable types](foundation.decidable-types.md).
 
-## Definition
+## Definitions
 
 ### The structure on a map of decidability
 
@@ -93,9 +99,46 @@ opaque
       ( K b)
 ```
 
+### Maps with sections are decidable
+
+```agda
+is-decidable-map-section :
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+  (i : A → B) → section i → is-decidable-map i
+is-decidable-map-section i (s , S) b = inl (s b , S b)
+```
+
+### Any map out of the empty type is decidable
+
+```agda
+abstract
+  is-decidable-map-ex-falso :
+    {l : Level} {X : UU l} → is-decidable-map (ex-falso {l} {X})
+  is-decidable-map-ex-falso x = inr pr1
+```
+
+### The identity map is decidable
+
+```agda
+abstract
+  is-decidable-map-id :
+    {l : Level} {X : UU l} → is-decidable-map (id {l} {X})
+  is-decidable-map-id y = inl (y , refl)
+```
+
+### Equivalences are decidable maps
+
+```agda
+abstract
+  is-decidable-map-is-equiv :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
+    is-equiv f → is-decidable-map f
+  is-decidable-map-is-equiv H x = inl (center (is-contr-map-is-equiv H x))
+```
+
 ### Composition of decidable maps
 
-The composite `g ∘ f` of two decidable maps is decidable if `g` is injective.
+The composite of two decidable maps `g ∘ f` is decidable if `g` is injective.
 
 ```agda
 module _
@@ -120,6 +163,46 @@ module _
         ( G x)
 ```
 
+The composite of two decidable maps `g ∘ f` is decidable if `g` has double
+negation dense equality on fibers.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {g : B → C} {f : A → B}
+  where
+
+  abstract
+    is-decidable-map-comp-has-double-negation-dense-equality-map :
+      has-double-negation-dense-equality-map g →
+      is-decidable-map g →
+      is-decidable-map f →
+      is-decidable-map (g ∘ f)
+    is-decidable-map-comp-has-double-negation-dense-equality-map H G F x =
+      is-decidable-equiv
+        ( compute-fiber-comp g f x)
+        ( is-decidable-Σ-has-double-negation-dense-equality-base
+          ( H x)
+          ( G x)
+          ( F ∘ pr1))
+
+module _
+  {l1 : Level} {A : UU l1} {f : A → A}
+  (is-decidable-f : is-decidable-map f)
+  (H : has-double-negation-dense-equality-map f)
+  where
+
+  is-decidable-map-iterate-has-double-negation-dense-equality-map :
+    (n : ℕ) → is-decidable-map (iterate n f)
+  is-decidable-map-iterate-has-double-negation-dense-equality-map zero-ℕ =
+    is-decidable-map-id
+  is-decidable-map-iterate-has-double-negation-dense-equality-map (succ-ℕ n) =
+    is-decidable-map-comp-has-double-negation-dense-equality-map
+      ( H)
+      ( is-decidable-f)
+      ( is-decidable-map-iterate-has-double-negation-dense-equality-map n)
+```
+
 ### Left cancellation for decidable maps
 
 If a composite `g ∘ f` is decidable and `g` is injective then `f` is decidable.
@@ -135,7 +218,7 @@ module _
     is-decidable-map-right-factor' GF G y =
       rec-coproduct
         ( λ q → inl (pr1 q , G (pr2 q)))
-        ( λ q → inr (λ x → q ((pr1 x) , ap g (pr2 x))))
+        ( λ q → inr (λ x → q (pr1 x , ap g (pr2 x))))
         ( GF (g y))
 ```
 
@@ -152,43 +235,6 @@ is-decidable-map-retraction d i (r , R) b =
     ( d (i (r b)) b)
 ```
 
-### Maps with sections are decidable
-
-```agda
-is-decidable-map-section :
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
-  (i : A → B) → section i → is-decidable-map i
-is-decidable-map-section i (s , S) b = inl (s b , S b)
-```
-
-### Any map out of the empty type is decidable
-
-```agda
-abstract
-  is-decidable-map-ex-falso :
-    {l : Level} {X : UU l} → is-decidable-map (ex-falso {l} {X})
-  is-decidable-map-ex-falso x = inr pr1
-```
-
-### The identity map is decidable
-
-```agda
-abstract
-  is-decidable-map-id :
-    {l : Level} {X : UU l} → is-decidable-map (id {l} {X})
-  is-decidable-map-id y = inl (y , refl)
-```
-
-### Equivalences are decidable maps
-
-```agda
-abstract
-  is-decidable-map-is-equiv :
-    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
-    is-equiv f → is-decidable-map f
-  is-decidable-map-is-equiv H x = inl (center (is-contr-map-is-equiv H x))
-```
-
 ### The map on total spaces induced by a family of decidable maps is decidable
 
 ```agda
diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md
index 24c1b8f0c4..9cebc2d58f 100644
--- a/src/foundation/decidable-propositions.lagda.md
+++ b/src/foundation/decidable-propositions.lagda.md
@@ -9,6 +9,7 @@ open import foundation-core.decidable-propositions public
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.0-connected-types
 open import foundation.action-on-identifications-functions
 open import foundation.booleans
 open import foundation.decidable-equality
diff --git a/src/foundation/double-negation-dense-equality-maps.lagda.md b/src/foundation/double-negation-dense-equality-maps.lagda.md
index 0fa5ddaa97..29ff9ee50f 100644
--- a/src/foundation/double-negation-dense-equality-maps.lagda.md
+++ b/src/foundation/double-negation-dense-equality-maps.lagda.md
@@ -7,11 +7,19 @@ module foundation.double-negation-dense-equality-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
 open import foundation.double-negation-dense-equality
+open import foundation.embeddings
+open import foundation.function-types
 open import foundation.irrefutable-equality
+open import foundation.iterating-functions
+open import foundation.propositional-maps
 open import foundation.universe-levels
 
 open import foundation-core.fibers-of-maps
+open import foundation-core.propositions
 ```
 
 </details>
@@ -34,3 +42,65 @@ has-double-negation-dense-equality-map :
 has-double-negation-dense-equality-map {B = B} f =
   (y : B) → has-double-negation-dense-equality (fiber f y)
 ```
+
+## Properties
+
+### Embeddings have double negation dense equality
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
+  where
+
+  abstract
+    has-double-negation-dense-equality-map-is-prop-map :
+      is-prop-map f → has-double-negation-dense-equality-map f
+    has-double-negation-dense-equality-map-is-prop-map H b x y =
+      irrefutable-eq-eq (eq-is-prop (H b))
+
+  abstract
+    has-double-negation-dense-equality-map-is-emb :
+      is-emb f → has-double-negation-dense-equality-map f
+    has-double-negation-dense-equality-map-is-emb H =
+      has-double-negation-dense-equality-map-is-prop-map
+        ( is-prop-map-is-emb H)
+
+has-double-negation-dense-equality-map-id :
+  {l : Level} {A : UU l} →
+  has-double-negation-dense-equality-map (id {A = A})
+has-double-negation-dense-equality-map-id =
+  has-double-negation-dense-equality-map-is-emb is-emb-id
+```
+
+### Composition of maps with double negation dense equality
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {g : B → C} {f : A → B}
+  where
+
+  abstract
+    has-double-negation-dense-equality-map-comp :
+      has-double-negation-dense-equality-map g →
+      has-double-negation-dense-equality-map f →
+      has-double-negation-dense-equality-map (g ∘ f)
+    has-double-negation-dense-equality-map-comp G F y =
+      has-double-negation-dense-equality-equiv
+        ( compute-fiber-comp g f y)
+        ( has-double-negation-dense-equality-Σ (G y) (F ∘ pr1))
+
+module _
+  {l1 : Level} {A : UU l1} {f : A → A}
+  (F : has-double-negation-dense-equality-map f)
+  where
+
+  abstract
+    has-double-negation-dense-equality-map-iterate :
+      (n : ℕ) → has-double-negation-dense-equality-map (iterate n f)
+    has-double-negation-dense-equality-map-iterate zero-ℕ =
+      has-double-negation-dense-equality-map-id
+    has-double-negation-dense-equality-map-iterate (succ-ℕ n) =
+      has-double-negation-dense-equality-map-comp F
+        ( has-double-negation-dense-equality-map-iterate n)
+```
diff --git a/src/foundation/functoriality-truncation.lagda.md b/src/foundation/functoriality-truncation.lagda.md
index 92e1760616..3708abf21b 100644
--- a/src/foundation/functoriality-truncation.lagda.md
+++ b/src/foundation/functoriality-truncation.lagda.md
@@ -131,7 +131,7 @@ module _
         ( preserves-comp-map-trunc k (map-inv-equiv e) (map-equiv e)) ∙h
         ( htpy-trunc (is-retraction-map-inv-equiv e) ∙h id-map-trunc k))
 
-  equiv-trunc : (type-trunc k A ≃ type-trunc k B)
+  equiv-trunc : type-trunc k A ≃ type-trunc k B
   pr1 equiv-trunc = map-equiv-trunc
   pr2 equiv-trunc = is-equiv-map-equiv-trunc
 ```
diff --git a/src/foundation/iterating-functions.lagda.md b/src/foundation/iterating-functions.lagda.md
index 47def9e9b1..1196af4981 100644
--- a/src/foundation/iterating-functions.lagda.md
+++ b/src/foundation/iterating-functions.lagda.md
@@ -18,12 +18,17 @@ open import elementary-number-theory.natural-numbers
 open import foundation.action-on-higher-identifications-functions
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.embeddings
 open import foundation.function-extensionality
 open import foundation.function-types
+open import foundation.propositional-maps
 open import foundation.subtypes
+open import foundation.truncated-maps
+open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import foundation-core.endomorphisms
+open import foundation-core.equivalences
 open import foundation-core.identity-types
 open import foundation-core.sets
 
@@ -113,31 +118,72 @@ module _
 ```agda
 module _
   {l1 l2 : Level} {X : UU l1} {f : X → X}
-  (P : subtype l2 (X → X))
+  {P : (X → X) → UU l2}
   where
 
-  is-in-subtype-iterate-succ-ℕ :
-    (F : is-in-subtype P f) →
-    ( (h g : X → X) →
-      is-in-subtype P h →
-      is-in-subtype P g →
-      is-in-subtype P (h ∘ g)) →
-    (n : ℕ) → is-in-subtype P (iterate (succ-ℕ n) f)
-  is-in-subtype-iterate-succ-ℕ F H zero-ℕ = F
-  is-in-subtype-iterate-succ-ℕ F H (succ-ℕ n) =
-    H f (iterate (succ-ℕ n) f) F (is-in-subtype-iterate-succ-ℕ F H n)
-
-  is-in-subtype-iterate :
-    (I : is-in-subtype P (id {A = X})) →
-    (F : is-in-subtype P f) →
-    ( (h g : X → X) →
-      is-in-subtype P h →
-      is-in-subtype P g →
-      is-in-subtype P (h ∘ g)) →
-    (n : ℕ) → is-in-subtype P (iterate n f)
-  is-in-subtype-iterate I F H zero-ℕ = I
-  is-in-subtype-iterate I F H (succ-ℕ n) =
-    H f (iterate n f) F (is-in-subtype-iterate I F H n)
+  is-in-function-class-iterate-succ-ℕ :
+    ( (h g : X → X) → P h → P g → P (h ∘ g)) →
+    (n : ℕ) → (F : P f) → P (iterate (succ-ℕ n) f)
+  is-in-function-class-iterate-succ-ℕ H zero-ℕ F = F
+  is-in-function-class-iterate-succ-ℕ H (succ-ℕ n) F =
+    H f (iterate (succ-ℕ n) f) F (is-in-function-class-iterate-succ-ℕ H n F)
+
+  is-in-function-class-iterate :
+    (I : P (id {A = X})) →
+    ((h g : X → X) → P h → P g → P (h ∘ g)) →
+    (n : ℕ) → (F : P f) → P (iterate n f)
+  is-in-function-class-iterate I H zero-ℕ F = I
+  is-in-function-class-iterate I H (succ-ℕ n) F =
+    H f (iterate n f) F (is-in-function-class-iterate I H n F)
+```
+
+### Iterates of equivalences are equivalences
+
+```agda
+module _
+  {l : Level} {X : UU l} {f : X → X}
+  where abstract
+
+  is-equiv-iterate : (n : ℕ) → is-equiv f → is-equiv (iterate n f)
+  is-equiv-iterate =
+    is-in-function-class-iterate is-equiv-id (λ h g H G → is-equiv-comp h g G H)
+```
+
+### Iterates of embeddings are embeddings
+
+```agda
+module _
+  {l : Level} {X : UU l} {f : X → X}
+  where abstract
+
+  is-emb-iterate : (n : ℕ) → is-emb f → is-emb (iterate n f)
+  is-emb-iterate = is-in-function-class-iterate is-emb-id is-emb-comp
+```
+
+### Iterates of truncated maps are truncated
+
+```agda
+module _
+  {l : Level} (k : 𝕋) {X : UU l} {f : X → X}
+  where abstract
+
+  is-trunc-map-iterate :
+    (n : ℕ) → is-trunc-map k f → is-trunc-map k (iterate n f)
+  is-trunc-map-iterate =
+    is-in-function-class-iterate (is-trunc-map-id k) (is-trunc-map-comp k)
+```
+
+### Iterates of propositional maps are propositional
+
+```agda
+module _
+  {l : Level} (k : 𝕋) {X : UU l} {f : X → X}
+  where abstract
+
+  is-prop-map-iterate :
+    (n : ℕ) → is-prop-map f → is-prop-map (iterate n f)
+  is-prop-map-iterate =
+    is-in-function-class-iterate is-prop-map-id is-prop-map-comp
 ```
 
 ## External links
diff --git a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
index 322774e407..975166b68e 100644
--- a/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
+++ b/src/foundation/lesser-limited-principle-of-omniscience.lagda.md
@@ -37,7 +37,7 @@ open import foundation-core.propositions
 
 </details>
 
-## Statement
+## Idea
 
 The {{#concept "lesser limited principle of omniscience" Agda=LLPO}} (LLPO)
 asserts that if two [decidable subtypes](foundation.decidable-subtypes.md) of
@@ -46,6 +46,10 @@ the [natural numbers](elementary-number-theory.natural-numbers.md) are not
 then merely one [or](foundation.disjunction.md) the other are
 [empty](foundation.empty-types.md).
 
+## Definitions
+
+### The small lesser limited principle of omniscience
+
 ```agda
 level-prop-LLPO : (l : Level) → Prop (lsuc l)
 level-prop-LLPO l =
diff --git a/src/foundation/perfect-images.lagda.md b/src/foundation/perfect-images.lagda.md
index 823a24a157..024cfd372e 100644
--- a/src/foundation/perfect-images.lagda.md
+++ b/src/foundation/perfect-images.lagda.md
@@ -10,20 +10,27 @@ module foundation.perfect-images where
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.decidable-dependent-function-types
+open import foundation.decidable-embeddings
+open import foundation.decidable-maps
+open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.double-negation
-open import foundation.iterated-dependent-product-types
+open import foundation.double-negation-dense-equality-maps
+open import foundation.functoriality-dependent-function-types
 open import foundation.iterating-functions
-open import foundation.law-of-excluded-middle
 open import foundation.negated-equality
 open import foundation.negation
+open import foundation.type-arithmetic-dependent-function-types
+open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
+open import foundation.weak-limited-principle-of-omniscience
 
 open import foundation-core.cartesian-product-types
-open import foundation-core.coproduct-types
 open import foundation-core.embeddings
 open import foundation-core.empty-types
+open import foundation-core.equivalences
 open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.identity-types
@@ -31,25 +38,38 @@ open import foundation-core.injective-maps
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
 open import foundation-core.transport-along-identifications
+
+open import logic.double-negation-eliminating-maps
+open import logic.double-negation-elimination
+open import logic.propositionally-decidable-maps
 ```
 
 </details>
 
 ## Idea
 
-Consider two maps `f : A → B` and `g : B → A`. For `(g ◦ f)ⁿ(a₀) ＝ a`, consider
-also the following chain
+Given two maps `f : A → B` and `g : B → A`, then if `(g ◦ f)ⁿ(a₀) ＝ a` for some
+[natural number](elementary-number-theory.natural-numbers.md) `n : ℕ`, we have a
+chain of elements
 
 ```text
       f          g            f               g       g
-  a₀ --> f (a₀) --> g(f(a₀)) --> f(g(f(a₀))) --> ... --> (g ◦ f)ⁿ(a₀) ＝ a
+  a₀ --> f (a₀) --> g(f(a₀)) --> f(g(f(a₀))) --> ... --> (g ◦ f)ⁿ(a₀) ＝ a.
 ```
 
-We say `a₀` is an {{#concept "origin"}} for `a`, and `a` is a
-{{#concept "perfect image" Agda=is-perfect-image}} for `g` if any origin of `a`
-is in the [image](foundation.images.md) of `g`.
+We say `a₀` is an {{#concept "origin" Disambiguation="perfect image"}} for `a`,
+and `a` is a {{#concept "perfect image" Agda=is-perfect-image}} for `g`
+_relative to `f`_ if any origin of `a` is in the [image](foundation.images.md)
+of `g`.
+
+This concept is used in the
+[Cantor–Schröder–Bernstein construction](foundation.cantor-schroder-bernstein-decidable-embeddings.md)
+to construct an equivalence of types `A ≃ B` given mutual embeddings
+`f : A ↪ B` and `g : B ↪ A`.
 
-## Definition
+## Definitions
+
+### Perfect images
 
 ```agda
 module _
@@ -58,88 +78,184 @@ module _
 
   is-perfect-image : (a : A) → UU (l1 ⊔ l2)
   is-perfect-image a =
-    (a₀ : A) (n : ℕ) → (iterate n (g ∘ f)) a₀ ＝ a → fiber g a₀
+    (a₀ : A) (n : ℕ) → iterate n (g ∘ f) a₀ ＝ a → fiber g a₀
+```
+
+An alternative but equivalent definition.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
+  where
+
+  is-perfect-image-at' : A → ℕ → UU (l1 ⊔ l2)
+  is-perfect-image-at' a n = (p : fiber (iterate n (g ∘ f)) a) → fiber g (pr1 p)
+
+  is-perfect-image' : (a : A) → UU (l1 ⊔ l2)
+  is-perfect-image' a = (n : ℕ) → is-perfect-image-at' a n
+
+  compute-is-perfect-image :
+    (a : A) → is-perfect-image' a ≃ is-perfect-image f g a
+  compute-is-perfect-image a =
+    equivalence-reasoning
+      ((n : ℕ) (p : fiber (iterate n (g ∘ f)) a) → fiber g (pr1 p))
+      ≃ ((n : ℕ) (a₀ : A) → iterate n (g ∘ f) a₀ ＝ a → fiber g a₀)
+        by equiv-Π-equiv-family (λ n → equiv-ev-pair)
+      ≃ ((a₀ : A) (n : ℕ) → iterate n (g ∘ f) a₀ ＝ a → fiber g a₀)
+        by equiv-swap-Π
+```
+
+### Nonperfect images
+
+We say an origin of `a` is a
+{{#concept "nonperfect image" Disambiguation="of pair of mutually converse maps" Agda=is-nonperfect-image}}
+if we have an `a₀ : A` and a natural number `n : ℕ` such that
+`(g ∘ f)ⁿ(a₀) = a`, but the fiber of `g` above `a₀` is
+[empty](foundation.empty-types.md).
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
+  where
+
+  is-nonperfect-image : (a : A) → UU (l1 ⊔ l2)
+  is-nonperfect-image a =
+    Σ ℕ (λ n → Σ A (λ a₀ → (iterate n (g ∘ f) a₀ ＝ a) × ¬ (fiber g a₀)))
+```
+
+**Comment.** Notice that, while being a nonperfect image is not always a
+proposition when `f` and `g` are embeddings, if we in addition require that `n`
+be minimal this would make it propositional.
+
+### Nonperfect fibers
+
+We say `f` has a
+{{#concept "nonperfect fiber" Disambiguation="of pair of mutually converse maps" Agda=has-nonperfect-fiber}}
+over an element `b` if there is a nonperfect image in its fiber.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A)
+  where
+
+  has-not-perfect-fiber : B → UU (l1 ⊔ l2)
+  has-not-perfect-fiber b =
+    Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
+
+  has-nonperfect-fiber : B → UU (l1 ⊔ l2)
+  has-nonperfect-fiber b =
+    Σ (fiber f b) (λ s → is-nonperfect-image f g (pr1 s))
 ```
 
 ## Properties
 
-If `g` is an [embedding](foundation-core.embeddings.md), then
-`is-perfect-image a` is a [proposition](foundation-core.propositions.md). In
-this case, if we assume the
-[law of excluded middle](foundation.law-of-excluded-middle.md), we can show
-`is-perfect-image a` is a [decidable type](foundation.decidable-types.md) for
-any `a : A`.
+### If `g` is an embedding then being a perfect image of `g` is a property
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A} (is-emb-g : is-emb g)
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
-  is-prop-is-perfect-image-is-emb :
-    (a : A) → is-prop (is-perfect-image f g a)
-  is-prop-is-perfect-image-is-emb a =
-    is-prop-iterated-Π 3 (λ a₀ n p → is-prop-map-is-emb is-emb-g a₀)
+  is-prop-is-perfect-image-at'' :
+    is-prop-map g → (a : A) (n : ℕ) →
+    is-prop (is-perfect-image-at' f g a n)
+  is-prop-is-perfect-image-at'' G a n =
+    is-prop-Π (λ p → G (pr1 p))
+
+  is-prop-is-perfect-image' :
+    is-prop-map g → (a : A) → is-prop (is-perfect-image f g a)
+  is-prop-is-perfect-image' G a =
+    is-prop-Π (λ a₀ → is-prop-Π (λ n → is-prop-Π (λ p → G a₀)))
+
+  is-perfect-image-Prop' : is-prop-map g → A → Prop (l1 ⊔ l2)
+  is-perfect-image-Prop' G a =
+    ( is-perfect-image f g a , is-prop-is-perfect-image' G a)
+
+  is-prop-is-perfect-image :
+    is-emb g → (a : A) → is-prop (is-perfect-image f g a)
+  is-prop-is-perfect-image G =
+    is-prop-is-perfect-image' (is-prop-map-is-emb G)
+
+  is-perfect-image-Prop : is-emb g → A → Prop (l1 ⊔ l2)
+  is-perfect-image-Prop G a =
+    ( is-perfect-image f g a , is-prop-is-perfect-image G a)
+```
 
-  is-perfect-image-Prop : A → Prop (l1 ⊔ l2)
-  pr1 (is-perfect-image-Prop a) = is-perfect-image f g a
-  pr2 (is-perfect-image-Prop a) = is-prop-is-perfect-image-is-emb a
+### If `f` is an embedding then having a not perfect fiber is a proposition
 
-  is-decidable-is-perfect-image-is-emb :
-    LEM (l1 ⊔ l2) → (a : A) → is-decidable (is-perfect-image f g a)
-  is-decidable-is-perfect-image-is-emb lem a =
-    lem (is-perfect-image-Prop a)
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  where
+
+  is-prop-has-not-perfect-fiber' :
+    is-prop-map f → (b : B) → is-prop (has-not-perfect-fiber f g b)
+  is-prop-has-not-perfect-fiber' F b = is-prop-Σ (F b) (λ _ → is-prop-neg)
+
+  is-prop-has-not-perfect-fiber :
+    is-emb f → (b : B) → is-prop (has-not-perfect-fiber f g b)
+  is-prop-has-not-perfect-fiber F =
+    is-prop-has-not-perfect-fiber' (is-prop-map-is-emb F)
+
+  has-not-perfect-fiber-Prop' :
+    is-prop-map f → B → Prop (l1 ⊔ l2)
+  has-not-perfect-fiber-Prop' F b =
+    ( has-not-perfect-fiber f g b , is-prop-has-not-perfect-fiber' F b)
+
+  has-not-perfect-fiber-Prop :
+    is-emb f → B → Prop (l1 ⊔ l2)
+  has-not-perfect-fiber-Prop F b =
+    ( has-not-perfect-fiber f g b , is-prop-has-not-perfect-fiber F b)
 ```
 
+### Fibers over perfect images
+
 If `a` is a perfect image for `g`, then `a` has a preimage under `g`. Just take
 `n = zero` in the definition.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
-  is-perfect-image-is-fiber :
-    {f : A → B} {g : B → A} → (a : A) →
-    is-perfect-image f g a → fiber g a
-  is-perfect-image-is-fiber a ρ = ρ a 0 refl
+  fiber-is-perfect-image : (a : A) → is-perfect-image f g a → fiber g a
+  fiber-is-perfect-image a ρ = ρ a 0 refl
 ```
 
 One can define a map from `A` to `B` restricting the domain to the perfect
-images of `g`. This gives a kind of [section](foundation-core.sections.md) of g.
-When g is also an embedding, the map gives a kind of
-[retraction](foundation-core.retractions.md) of g.
+images of `g`. This gives a kind of [section](foundation-core.sections.md) of
+`g`. When `g` is also an embedding, the map gives a kind of
+[retraction](foundation-core.retractions.md) of `g`.
 
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
-  inverse-of-perfect-image :
-    (a : A) → (is-perfect-image f g a) → B
-  inverse-of-perfect-image a ρ =
-    pr1 (is-perfect-image-is-fiber a ρ)
+  inverse-of-perfect-image : (a : A) → is-perfect-image f g a → B
+  inverse-of-perfect-image a ρ = pr1 (fiber-is-perfect-image a ρ)
 
   is-section-inverse-of-perfect-image :
     (a : A) (ρ : is-perfect-image f g a) →
     g (inverse-of-perfect-image a ρ) ＝ a
   is-section-inverse-of-perfect-image a ρ =
-    pr2 (is-perfect-image-is-fiber a ρ)
+    pr2 (fiber-is-perfect-image a ρ)
 ```
 
+When `g` is also injective, the map gives a kind of
+[retraction](foundation-core.retractions.md) of `g`.
+
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A} {is-emb-g : is-emb g}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
   is-retraction-inverse-of-perfect-image :
+    is-injective g →
     (b : B) (ρ : is-perfect-image f g (g b)) →
     inverse-of-perfect-image (g b) ρ ＝ b
-  is-retraction-inverse-of-perfect-image b ρ =
-    is-injective-is-emb
-      is-emb-g
-      (is-section-inverse-of-perfect-image (g b) ρ)
+  is-retraction-inverse-of-perfect-image G b ρ =
+    G (is-section-inverse-of-perfect-image (g b) ρ)
 ```
 
 If `g(f(a))` is a perfect image for `g`, so is `a`.
@@ -149,15 +265,30 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
+  previous-perfect-image-at' :
+    (a : A) (n : ℕ) →
+    is-perfect-image-at' f g (g (f a)) (succ-ℕ n) →
+    is-perfect-image-at' f g a n
+  previous-perfect-image-at' a n γ (a₀ , p) =
+    γ (a₀ , ap (g ∘ f) p)
+
+  previous-perfect-image' :
+    (a : A) →
+    is-perfect-image' f g (g (f a)) →
+    is-perfect-image' f g a
+  previous-perfect-image' a γ n =
+    previous-perfect-image-at' a n (γ (succ-ℕ n))
+
   previous-perfect-image :
     (a : A) →
-    is-perfect-image f g (g (f (a))) →
+    is-perfect-image f g (g (f a)) →
     is-perfect-image f g a
-  previous-perfect-image a γ a₀ n p = γ a₀ (succ-ℕ n) (ap (g ∘ f) p)
+  previous-perfect-image a γ a₀ n p =
+    γ a₀ (succ-ℕ n) (ap (g ∘ f) p)
 ```
 
-Perfect images goes to a disjoint place under `inverse-of-perfect-image` than
-`f`
+Perfect images of `g` relative to `f` not mapped to the image of `f` under
+`inverse-of-perfect-image`.
 
 ```agda
 module _
@@ -165,7 +296,9 @@ module _
   where
 
   perfect-image-has-distinct-image :
-    (a a₀ : A) → ¬ (is-perfect-image f g a) → (ρ : is-perfect-image f g a₀) →
+    (a a₀ : A) →
+    ¬ (is-perfect-image f g a) →
+    (ρ : is-perfect-image f g a₀) →
     f a ≠ inverse-of-perfect-image a₀ ρ
   perfect-image-has-distinct-image a a₀ nρ ρ p =
     v ρ
@@ -177,88 +310,209 @@ module _
     s = λ η → nρ (previous-perfect-image a η)
 
     v : ¬ (is-perfect-image f g a₀)
-    v = tr (λ _ → ¬ (is-perfect-image f g _)) q s
+    v = tr (λ a' → ¬ (is-perfect-image f g a')) q s
 ```
 
-Using the property above, we can talk about origins of `a` which are not images
-of `g`.
+### Double negation elimination on not perfect fibers
+
+If we assume that `g` is a double negation eliminating map, we can prove that if
+`is-nonperfect-image a` does not hold, then we have `is-perfect-image a`.
 
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
-  is-not-perfect-image : (a : A) → UU (l1 ⊔ l2)
-  is-not-perfect-image a =
-    Σ A (λ a₀ → (Σ ℕ (λ n → ((iterate n (g ∘ f)) a₀ ＝ a) × ¬ (fiber g a₀))))
+  double-negation-elim-is-perfect-image :
+    is-double-negation-eliminating-map g →
+    (a : A) → ¬ (is-nonperfect-image f g a) → is-perfect-image f g a
+  double-negation-elim-is-perfect-image G a nρ a₀ n p =
+    G a₀ (λ a₁ → nρ (n , a₀ , p , a₁))
 ```
 
-If we assume the law of excluded middle and `g` is an embedding, we can prove
-that if `is-not-perfect-image a` does not hold, we have `is-perfect-image a`.
+If `g(b)` is not a perfect image, then there is an `a ∈ fiber f b` that is not a
+perfect image of `g`.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A} (is-emb-g : is-emb g)
-  (lem : LEM (l1 ⊔ l2))
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
-  is-perfect-not-not-is-perfect-image :
-    (a : A) → ¬ (is-not-perfect-image a) → is-perfect-image f g a
-  is-perfect-not-not-is-perfect-image a nρ a₀ n p =
-    rec-coproduct
-      ( id)
-      ( λ a₁ → ex-falso (nρ (a₀ , n , p , a₁)))
-      ( lem (fiber g a₀ , is-prop-map-is-emb is-emb-g a₀))
+  is-irrefutable-is-nonperfect-image-is-not-perfect-image :
+    (G : is-double-negation-eliminating-map g)
+    (b : B) (nρ : ¬ (is-perfect-image f g (g b))) →
+    ¬¬ (is-nonperfect-image f g (g b))
+  is-irrefutable-is-nonperfect-image-is-not-perfect-image G b nρ nμ =
+    nρ (double-negation-elim-is-perfect-image G (g b) nμ)
+
+  has-not-perfect-fiber-is-nonperfect-image :
+    is-injective g →
+    (b : B) →
+    is-nonperfect-image f g (g b) →
+    has-not-perfect-fiber f g b
+  has-not-perfect-fiber-is-nonperfect-image G b (zero-ℕ , x₀ , u) =
+    ex-falso (pr2 u (b , inv (pr1 u)))
+  has-not-perfect-fiber-is-nonperfect-image G b (succ-ℕ n , x₀ , u) =
+    ( iterate n (g ∘ f) x₀ , G (pr1 u)) ,
+    ( λ s → pr2 u (s x₀ n refl))
+
+  is-irrefutable-has-not-perfect-fiber-is-not-perfect-image :
+    is-double-negation-eliminating-map g →
+    is-injective g →
+    (b : B) (nρ : ¬ (is-perfect-image f g (g b))) →
+    ¬¬ (has-not-perfect-fiber f g b)
+  is-irrefutable-has-not-perfect-fiber-is-not-perfect-image G G' b nρ t =
+    is-irrefutable-is-nonperfect-image-is-not-perfect-image G b nρ
+      ( λ s → t (has-not-perfect-fiber-is-nonperfect-image G' b s))
 ```
 
-The following property states that if `g (b)` is not a perfect image, then `b`
-has an `f` fiber `a` that is not a perfect image for `g`. Again, we need to
-assume law of excluded middle and that both `g` and `f` are embedding.
+If `f` has double negation dense equality and double negation elimination, then
+`has-not-perfect-fiber f g b` has double negation elimination.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  {f : A → B} {g : B → A}
-  (is-emb-f : is-emb f) (is-emb-g : is-emb g)
-  (lem : LEM (l1 ⊔ l2))
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
   where
 
-  not-perfect-image-has-not-perfect-fiber :
-      (b : B) →
-      ¬ (is-perfect-image f g (g b)) →
-      Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
-  not-perfect-image-has-not-perfect-fiber b nρ = v
-      where
-      i : ¬¬ (is-not-perfect-image {f = f} (g b))
-      i = λ nμ → nρ (is-perfect-not-not-is-perfect-image is-emb-g lem (g b) nμ)
-
-      ii :
-        is-not-perfect-image (g b) →
-        Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
-      ii (x₀ , 0 , u) =
-        ex-falso (pr2 u (b , inv (pr1 u)))
-      ii (x₀ , succ-ℕ n , u) =
-        a , w
-        where
-        q : f (iterate n (g ∘ f) x₀) ＝ b
-        q = is-injective-is-emb is-emb-g (pr1 u)
-
-        a : fiber f b
-        a = iterate n (g ∘ f) x₀ , q
-
-        w : ¬ (is-perfect-image f g ((iterate n (g ∘ f)) x₀))
-        w = λ s → pr2 u (s x₀ n refl)
-
-      iii : ¬¬ (Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))))
-      iii = λ t → i (λ s → t (ii s))
-
-      iv : is-prop (Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s))))
-      iv =
-        is-prop-Σ
-          (is-prop-map-is-emb is-emb-f b)
-          (λ s → is-prop-neg {A = is-perfect-image f g (pr1 s)})
-
-      v : Σ (fiber f b) (λ s → ¬ (is-perfect-image f g (pr1 s)))
-      v = double-negation-elim-is-decidable (lem (_ , iv)) iii
+  double-negation-elim-has-not-perfect-fiber :
+    is-double-negation-eliminating-map f →
+    has-double-negation-dense-equality-map f →
+    (b : B) →
+    has-double-negation-elim (has-not-perfect-fiber f g b)
+  double-negation-elim-has-not-perfect-fiber F F' b =
+    double-negation-elim-Σ-has-double-negation-dense-equality-base
+      ( F' b)
+      ( F b)
+      ( λ p → double-negation-elim-neg (is-perfect-image f g (pr1 p)))
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  (G : is-double-negation-eliminating-map g)
+  (G' : is-injective g)
+  (F : is-double-negation-eliminating-map f)
+  (F' : has-double-negation-dense-equality-map f)
+  (b : B) (nρ : ¬ (is-perfect-image f g (g b)))
+  where
+
+  has-not-perfect-fiber-is-not-perfect-image :
+    has-not-perfect-fiber f g b
+  has-not-perfect-fiber-is-not-perfect-image =
+    double-negation-elim-has-not-perfect-fiber F F' b
+      ( is-irrefutable-has-not-perfect-fiber-is-not-perfect-image G G' b nρ)
+
+  fiber-has-not-perfect-fiber-is-not-perfect-image : fiber f b
+  fiber-has-not-perfect-fiber-is-not-perfect-image =
+    pr1 has-not-perfect-fiber-is-not-perfect-image
+
+  element-has-not-perfect-fiber-is-not-perfect-image : A
+  element-has-not-perfect-fiber-is-not-perfect-image =
+    pr1 fiber-has-not-perfect-fiber-is-not-perfect-image
+
+  is-in-fiber-element-has-not-perfect-fiber-is-not-perfect-image :
+    f element-has-not-perfect-fiber-is-not-perfect-image ＝ b
+  is-in-fiber-element-has-not-perfect-fiber-is-not-perfect-image =
+    pr2 fiber-has-not-perfect-fiber-is-not-perfect-image
+
+  is-not-perfect-image-has-not-perfect-fiber-is-not-perfect-image :
+    ¬ (is-perfect-image f g element-has-not-perfect-fiber-is-not-perfect-image)
+  is-not-perfect-image-has-not-perfect-fiber-is-not-perfect-image =
+    pr2 has-not-perfect-fiber-is-not-perfect-image
+```
+
+### Decidability of perfect images
+
+Assuming `g` and `f` are decidable embedding, then for every natural number
+`n : ℕ` and every element `a : A` it is decidable whether `a` is a perfect image
+of `g` relative to `f` after `n` iterations. In fact, the map `f` need only be
+propositionally decidable and have double negation dense equality on fibers.
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  where abstract
+
+  is-decidable-prop-is-perfect-image-at'' :
+    is-decidable-emb g →
+    is-inhabited-or-empty-map f →
+    has-double-negation-dense-equality-map f →
+    (a : A) (n : ℕ) →
+    is-decidable-prop (is-perfect-image-at' f g a n)
+  is-decidable-prop-is-perfect-image-at'' G F F' a n =
+    is-decidable-prop-Π-has-double-negation-dense-equality-base'
+      ( λ x →
+        fiber g (pr1 x) ,
+        is-decidable-prop-map-is-decidable-emb G (pr1 x))
+      ( has-double-negation-dense-equality-map-iterate
+        ( has-double-negation-dense-equality-map-comp
+          ( has-double-negation-dense-equality-map-is-emb
+            ( is-emb-is-decidable-emb G))
+          ( F'))
+        ( n)
+        ( a))
+      ( is-inhabited-or-empty-map-iterate-has-double-negation-dense-equality-map
+        ( is-inhabited-or-empty-map-comp-has-double-negation-dense-equality-map
+          ( has-double-negation-dense-equality-map-is-emb
+            ( is-emb-is-decidable-emb G))
+          ( is-inhabited-or-empty-map-is-decidable-map
+            ( is-decidable-map-is-decidable-emb G))
+          ( F))
+        ( has-double-negation-dense-equality-map-comp
+          ( has-double-negation-dense-equality-map-is-emb
+            ( is-emb-is-decidable-emb G))
+          ( F'))
+        ( n)
+        ( a))
+
+  is-decidable-prop-is-perfect-image-at' :
+    is-decidable-emb g →
+    is-decidable-map f →
+    has-double-negation-dense-equality-map f →
+    (a : A) (n : ℕ) →
+    is-decidable-prop (is-perfect-image-at' f g a n)
+  is-decidable-prop-is-perfect-image-at' G F =
+    is-decidable-prop-is-perfect-image-at'' G
+      ( is-inhabited-or-empty-map-is-decidable-map F)
+```
+
+### Decidability of perfect images under WLPO
+
+It follows from the
+[weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md)
+that, for every pair of mutual decidable embeddings `f : A ↪ B` and
+`g : B ↪ A`, it is decidable for every element `x : A` whether `x` is a perfect
+image of `g` relative to `f`.
+
+```agda
+module _
+  {l1 l2 : Level} (wlpo : level-WLPO (l1 ⊔ l2))
+  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
+  where abstract
+
+  is-decidable-is-perfect-image'-WLPO :
+    is-decidable-emb g →
+    is-decidable-map f →
+    has-double-negation-dense-equality-map f →
+    (a : A) →
+    is-decidable (is-perfect-image' f g a)
+  is-decidable-is-perfect-image'-WLPO G F F' a =
+    wlpo
+      ( λ n →
+        is-perfect-image-at' f g a n ,
+        is-decidable-prop-is-perfect-image-at' G F F' a n)
+
+  is-decidable-is-perfect-image-WLPO :
+    is-decidable-emb g →
+    is-decidable-map f →
+    has-double-negation-dense-equality-map f →
+    (a : A) →
+    is-decidable (is-perfect-image f g a)
+  is-decidable-is-perfect-image-WLPO G F F' a =
+    is-decidable-equiv'
+      ( compute-is-perfect-image f g a)
+      ( is-decidable-is-perfect-image'-WLPO G F F' a)
 ```
+
+## External links
+
+- See also the twin formalization in TypeTopology at
+  [`CantorSchroederBernstein.PerfectImages`](https://martinescardo.github.io/TypeTopology/CantorSchroederBernstein.PerfectImages.html).
diff --git a/src/foundation/truncations.lagda.md b/src/foundation/truncations.lagda.md
index da13d2b08d..ed07abee14 100644
--- a/src/foundation/truncations.lagda.md
+++ b/src/foundation/truncations.lagda.md
@@ -357,6 +357,10 @@ module _
   is-equiv-unit-trunc-is-contr : is-contr A → is-equiv unit-trunc
   is-equiv-unit-trunc-is-contr c =
     is-equiv-unit-trunc (A , is-trunc-is-contr k c)
+
+  is-contr-type-trunc : is-contr A → is-contr (type-trunc k A)
+  is-contr-type-trunc H =
+    is-contr-is-equiv' A unit-trunc (is-equiv-unit-trunc-is-contr H) H
 ```
 
 ### Truncation is idempotent
diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
index b855eca865..9d2ce56416 100644
--- a/src/literature/100-theorems.lagda.md
+++ b/src/literature/100-theorems.lagda.md
@@ -33,18 +33,19 @@ open import elementary-number-theory.infinitude-of-primes using
 
 **Author:** [Elif Uskuplu](https://elifuskuplu.github.io)
 
-**Note:** The formalization of the Cantor-Schröder-Bernstein theorem in
-agda-unimath is a generalization of the statement to all types, i.e., it is not
-restricted to sets. This generalization is originally due to Martin-Escardó,
-hence we refer to the generalization as the Cantor-Schröder-Bernstein-Escardó
-theorem.
-
 ```agda
 open import foundation.cantor-schroder-bernstein-escardo using
   ( Cantor-Schröder-Bernstein-Escardó ;
     Cantor-Schröder-Bernstein)
 ```
 
+**Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke)
+
+```agda
+open import foundation.cantor-schroder-bernstein-decidable-embeddings using
+  ( Cantor-Schröder-Bernstein-WLPO)
+```
+
 ### 44. The binomial theorem {#44}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
@@ -159,7 +160,6 @@ open import real-numbers.metric-space-of-real-numbers using
 ```agda
 open import real-numbers.absolute-value-real-numbers using
   ( triangle-inequality-abs-ℝ)
-
 open import real-numbers.distance-real-numbers using
   ( triangle-inequality-dist-ℝ)
 ```
diff --git a/src/literature/wikipedia-list-of-theorems.lagda.md b/src/literature/wikipedia-list-of-theorems.lagda.md
index 3677061e2a..0c7846e7b9 100644
--- a/src/literature/wikipedia-list-of-theorems.lagda.md
+++ b/src/literature/wikipedia-list-of-theorems.lagda.md
@@ -50,18 +50,19 @@ open import elementary-number-theory.binomial-theorem-natural-numbers using
 
 **Author:** [Elif Uskuplu](https://elifuskuplu.github.io)
 
-**Note:** The formalization of the Cantor-Schröder-Bernstein theorem in
-agda-unimath is a generalization of the statement to all types, i.e., it is not
-restricted to sets. This generalization is originally due to Martin-Escardó,
-hence we refer to the generalization as the Cantor-Schröder-Bernstein-Escardó
-theorem.
-
 ```agda
 open import foundation.cantor-schroder-bernstein-escardo using
   ( Cantor-Schröder-Bernstein-Escardó ;
     Cantor-Schröder-Bernstein)
 ```
 
+**Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke)
+
+```agda
+open import foundation.cantor-schroder-bernstein-decidable-embeddings using
+  ( Cantor-Schröder-Bernstein-WLPO)
+```
+
 ### Cantor's theorem {#Q474881}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
diff --git a/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md b/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md
index eb2cbcdba9..f173a260c6 100644
--- a/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md
+++ b/src/orthogonal-factorization-systems/double-negation-sheaves.lagda.md
@@ -83,7 +83,7 @@ is-double-negation-sheaf-is-contr is-contr-A P =
 module _
   {l : Level} {A : UU l}
   (is-prop-A : is-prop A)
-  (is-¬¬sheaf-A : is-double-negation-sheaf l A)
+  (is-¬¬-sheaf-A : is-double-negation-sheaf l A)
   where
 
   compute-is-double-negation-sheaf-is-prop : A ≃ (¬ A → A)
@@ -91,12 +91,12 @@ module _
     ( left-unit-law-product-is-contr
       ( is-proof-irrelevant-is-prop (is-prop-function-type is-prop-A) id)) ∘e
     ( equiv-universal-property-coproduct A) ∘e
-    ( _ , is-¬¬sheaf-A (is-decidable-prop-Irrefutable-Prop (A , is-prop-A)))
+    ( _ , is-¬¬-sheaf-A (is-decidable-prop-Irrefutable-Prop (A , is-prop-A)))
 
   is-double-negation-stable-is-double-negation-sheaf-is-prop :
     is-double-negation-stable (A , is-prop-A)
   is-double-negation-stable-is-double-negation-sheaf-is-prop ¬¬a =
-    map-inv-is-equiv (is-¬¬sheaf-A (A , is-prop-A , ¬¬a)) id
+    map-inv-is-equiv (is-¬¬-sheaf-A (A , is-prop-A , ¬¬a)) id
 ```
 
 ### Double negation stable propositions are double negation sheaves
diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md
index 5242c08e65..5db561660b 100644
--- a/src/synthetic-homotopy-theory/pushouts.lagda.md
+++ b/src/synthetic-homotopy-theory/pushouts.lagda.md
@@ -176,7 +176,20 @@ module _
         ( c)
         ( compute-inl-dependent-cogap)
         ( compute-inr-dependent-cogap)
+```
+
+For reference, the unfolded type signature for `compute-glue-dependent-cogap` is
+as follows:
+
+```text
+  (s : S) →
+  ( apd dependent-cogap (glue-pushout f g s) ∙
+    compute-inr-dependent-cogap (g s)) ＝
+  ( ap (tr P (glue-pushout f g s)) (compute-inl-dependent-cogap (f s)) ∙
+    coherence-square-dependent-cocone f g (cocone-pushout f g) P c s)
+```
 
+```agda
   htpy-compute-dependent-cogap :
     htpy-dependent-cocone f g
       ( cocone-pushout f g)