diff --git a/references.bib b/references.bib
index aced02fe79..9b40c4fe20 100644
--- a/references.bib
+++ b/references.bib
@@ -531,18 +531,24 @@ @online{Shu14UniversalProperties
 }
 
 @article{Shu17,
-  title     = {Idempotents in Intensional Type Theory},
-  author    = {Shulman, Michael},
-  date      = {2017-04-27},
-  year      = {2017},
-  month     = {04},
-  journal   = {Logical Methods in Computer Science},
-  volume    = {Volume 12, Issue 3},
-  publisher = {Episciences.org},
-  issn      = {1860-5974},
-  doi       = {10.2168/LMCS-12(3:9)2016},
-  url       = {https://lmcs.episciences.org/2027},
-  abstract  = {We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.}
+  title        = {Idempotents in Intensional Type Theory},
+  author       = {Shulman, Michael},
+  date         = {2017-04-27},
+  year         = {2017},
+  month        = {04},
+  eprint       = {1507.03634},
+  eprinttype   = {arxiv},
+  eprintclass  = {math},
+  primaryClass = {math.LO},
+  journal      = {Logical Methods in Computer Science},
+  volume       = {12},
+  issue        = {3},
+  pages        = {1--24},
+  publisher    = {Episciences.org},
+  issn         = {1860-5974},
+  doi          = {10.2168/LMCS-12(3:9)2016},
+  url          = {https://lmcs.episciences.org/2027},
+  abstract     = {We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.}
 }
 
 @article{Shu18,
diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
index d13637cdc8..4eda140f40 100644
--- a/src/foundation-core/functoriality-dependent-pair-types.lagda.md
+++ b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
@@ -19,6 +19,8 @@ open import foundation-core.fibers-of-maps
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.retractions
+open import foundation-core.retracts-of-types
 open import foundation-core.transport-along-identifications
 ```
 
@@ -234,6 +236,26 @@ module _
     is-equiv-tot-is-fiberwise-equiv (λ x → is-equiv-map-equiv (e x))
 ```
 
+### The action of `tot` on retracts
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  where
+
+  retraction-tot :
+    {f : (x : A) → B x → C x} →
+    ((x : A) → retraction (f x)) → retraction (tot f)
+  pr1 (retraction-tot {f} r) (x , z) =
+    ( x , map-retraction (f x) (r x) z)
+  pr2 (retraction-tot {f} r) (x , z) =
+    eq-pair-eq-fiber (is-retraction-map-retraction (f x) (r x) z)
+
+  retract-tot : ((x : A) → (B x) retract-of (C x)) → (Σ A B) retract-of (Σ A C)
+  pr1 (retract-tot r) = tot (λ x → inclusion-retract (r x))
+  pr2 (retract-tot r) = retraction-tot (λ x → retraction-retract (r x))
+```
+
 ### The fibers of `map-Σ-map-base`
 
 ```agda
diff --git a/src/foundation-core/sets.lagda.md b/src/foundation-core/sets.lagda.md
index 27390c8d90..d7a21248b0 100644
--- a/src/foundation-core/sets.lagda.md
+++ b/src/foundation-core/sets.lagda.md
@@ -25,7 +25,9 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A type is a set if its identity types are propositions.
+A type is a {{#concept "set" Agda=is-set}} if its
+[identity types](foundation-core.identity-types.md) are
+[propositions](foundation-core.propositions.md).
 
 ## Definition
 
@@ -86,6 +88,27 @@ module _
       ( contraction (is-proof-irrelevant-is-prop (H x x) refl) p)
 ```
 
+### A type is a set if and only if it satisfies uniqueness of identity proofs
+
+A type `A` is said to satisfy
+{{#concept "uniqueness of identity proofs" Agda=has-uip}} if for all elements
+`x y : A` all equality proofs `x ＝ y` are equal.
+
+```agda
+has-uip : {l : Level} → UU l → UU l
+has-uip A = (x y : A) → all-elements-equal (x ＝ y)
+
+module _
+  {l : Level} {A : UU l}
+  where
+
+  is-set-has-uip : is-set A → has-uip A
+  is-set-has-uip is-set-A x y = eq-is-prop' (is-set-A x y)
+
+  has-uip-is-set : has-uip A → is-set A
+  has-uip-is-set uip-A x y = is-prop-all-elements-equal (uip-A x y)
+```
+
 ### If a reflexive binary relation maps into the identity type of `A`, then `A` is a set
 
 ```agda
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index ad3b0ff8b8..760a6dda04 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -53,6 +53,7 @@ open import foundation.category-of-families-of-sets public
 open import foundation.category-of-sets public
 open import foundation.choice-of-representatives-equivalence-relation public
 open import foundation.codiagonal-maps-of-types public
+open import foundation.coherently-idempotent-maps public
 open import foundation.coherently-invertible-maps public
 open import foundation.coinhabited-pairs-of-types public
 open import foundation.commuting-cubes-of-maps public
diff --git a/src/foundation/coherently-idempotent-maps.lagda.md b/src/foundation/coherently-idempotent-maps.lagda.md
new file mode 100644
index 0000000000..d746a1ec6a
--- /dev/null
+++ b/src/foundation/coherently-idempotent-maps.lagda.md
@@ -0,0 +1,76 @@
+# Coherently idempotent maps
+
+```agda
+module foundation.coherently-idempotent-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.homotopy-algebra
+open import foundation.quasicoherently-idempotent-maps
+open import foundation.split-idempotent-maps
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.propositions
+open import foundation-core.retractions
+open import foundation-core.sets
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "coherently idempotent map" Disambiguation="of types" Agda=is-coherently-idempotent}}
+is an [idempotent](foundation.idempotent-maps.md) map `f : A → A`
+[equipped](foundation.structure.md) with an infinitely coherent hierarchy of
+[homotopies](foundation-core.homotopies.md) making it a "homotopy-correct"
+definition of an idempotent map in Homotopy Type Theory.
+
+The infinite coherence condition is given by taking the
+[sequential limit](foundation.sequential-limits.md) of iterated application of
+the splitting construction on
+[quasicoherently idempotent maps](foundation.quasicoherently-idempotent-maps.md)
+given in {{#cite Shu17}}:
+
+```text
+  is-coherently-idempotent f :=
+    Σ (a : ℕ → is-quasicoherently-idempotent f), (Π (n : ℕ), split(aₙ₊₁) ~ aₙ)
+```
+
+**Terminology.** Our definition of a _coherently idempotent map_ corresponds to
+the definition of a _(fully coherent) idempotent map_ in {{#reference Shu17}}
+and {{#reference Shu14SplittingIdempotents}}. Our definition of an _idempotent
+map_ corresponds in their terminology to a _pre-idempotent map_.
+
+## Definitions
+
+### The structure on a map of coherent idempotence
+
+```agda
+is-coherently-idempotent : {l : Level} {A : UU l} → (A → A) → UU l
+is-coherently-idempotent f =
+  Σ ( ℕ → is-quasicoherently-idempotent f)
+    ( λ a →
+      (n : ℕ) →
+      htpy-is-quasicoherently-idempotent
+        ( is-quasicoherently-idempotent-is-split-idempotent
+          ( is-split-idempotent-is-quasicoherently-idempotent
+            ( a (succ-ℕ n))))
+        ( a n))
+```
+
+## See also
+
+- [Split idempotent maps](foundation.split-idempotent-maps.md)
+
+## References
+
+{{#bibliography}} {{#reference Shu17}} {{#reference Shu14SplittingIdempotents}}
diff --git a/src/foundation/quasicoherently-idempotent-maps.lagda.md b/src/foundation/quasicoherently-idempotent-maps.lagda.md
index 6ab4964d05..bec945c76a 100644
--- a/src/foundation/quasicoherently-idempotent-maps.lagda.md
+++ b/src/foundation/quasicoherently-idempotent-maps.lagda.md
@@ -9,18 +9,24 @@ module foundation.quasicoherently-idempotent-maps where
 ```agda
 open import foundation.1-types
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-homotopies
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-algebra
+open import foundation.homotopy-induction
 open import foundation.idempotent-maps
 open import foundation.identity-types
 open import foundation.negated-equality
 open import foundation.negation
+open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 open import foundation.whiskering-higher-homotopies-composition
 open import foundation.whiskering-homotopies-composition
 
+open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.propositions
@@ -416,6 +422,88 @@ idempotence homotopy `f ∘ f ~ f` is quasicoherent. A counterexample can be
 constructed using the [cantor space](set-theory.cantor-space.md), see Section 4
 of {{#cite Shu17}} for more details.
 
+### Characterization of identity of quasicoherently idempotent maps
+
+A homotopy of quasicoherent idempotence witnesses `(I, Q) ~ (J, R)` consists of
+a homotopy of the underlying idempotence witnesses `H : I ~ J` and a
+[coherence](foundation-core.commuting-squares-of-homotopies.md)
+
+```text
+            fH
+  f ·l I -------- f ·l J
+     |              |
+   Q |              | R
+     |              |
+  I ·r f -------– J ·r f.
+            Hf
+```
+
+```agda
+module _
+  {l : Level} {A : UU l} {f : A → A}
+  where
+
+  coherence-htpy-is-quasicoherently-idempotent :
+    (p q : is-quasicoherently-idempotent f) →
+    ( is-idempotent-is-quasicoherently-idempotent p ~
+      is-idempotent-is-quasicoherently-idempotent q) →
+    UU l
+  coherence-htpy-is-quasicoherently-idempotent (I , Q) (J , R) H =
+    coherence-square-homotopies
+      ( left-whisker-comp² f H)
+      ( Q)
+      ( R)
+      ( right-whisker-comp² H f)
+
+  htpy-is-quasicoherently-idempotent :
+    (p q : is-quasicoherently-idempotent f) → UU l
+  htpy-is-quasicoherently-idempotent p q =
+    Σ ( is-idempotent-is-quasicoherently-idempotent p ~
+        is-idempotent-is-quasicoherently-idempotent q)
+      ( coherence-htpy-is-quasicoherently-idempotent p q)
+
+  refl-htpy-is-quasicoherently-idempotent :
+    (p : is-quasicoherently-idempotent f) →
+    htpy-is-quasicoherently-idempotent p p
+  refl-htpy-is-quasicoherently-idempotent p = (refl-htpy , right-unit-htpy)
+
+  htpy-eq-is-quasicoherently-idempotent :
+    (p q : is-quasicoherently-idempotent f) →
+    p ＝ q → htpy-is-quasicoherently-idempotent p q
+  htpy-eq-is-quasicoherently-idempotent p .p refl =
+    refl-htpy-is-quasicoherently-idempotent p
+
+  is-torsorial-htpy-is-quasicoherently-idempotent :
+    (p : is-quasicoherently-idempotent f) →
+    is-torsorial (htpy-is-quasicoherently-idempotent p)
+  is-torsorial-htpy-is-quasicoherently-idempotent p =
+    is-torsorial-Eq-structure
+      ( is-torsorial-htpy (is-idempotent-is-quasicoherently-idempotent p))
+      ( is-idempotent-is-quasicoherently-idempotent p , refl-htpy)
+      ( is-torsorial-htpy (coh-is-quasicoherently-idempotent p ∙h refl-htpy))
+
+  is-equiv-htpy-eq-is-quasicoherently-idempotent :
+    (p q : is-quasicoherently-idempotent f) →
+    is-equiv (htpy-eq-is-quasicoherently-idempotent p q)
+  is-equiv-htpy-eq-is-quasicoherently-idempotent p =
+    fundamental-theorem-id
+      ( is-torsorial-htpy-is-quasicoherently-idempotent p)
+      ( htpy-eq-is-quasicoherently-idempotent p)
+
+  extensionality-is-quasicoherently-idempotent :
+    (p q : is-quasicoherently-idempotent f) →
+    (p ＝ q) ≃ (htpy-is-quasicoherently-idempotent p q)
+  extensionality-is-quasicoherently-idempotent p q =
+    ( htpy-eq-is-quasicoherently-idempotent p q ,
+      is-equiv-htpy-eq-is-quasicoherently-idempotent p q)
+
+  eq-htpy-is-quasicoherently-idempotent :
+    (p q : is-quasicoherently-idempotent f) →
+    htpy-is-quasicoherently-idempotent p q → p ＝ q
+  eq-htpy-is-quasicoherently-idempotent p q =
+    map-inv-is-equiv (is-equiv-htpy-eq-is-quasicoherently-idempotent p q)
+```
+
 ## See also
 
 - In [`foundation.split-idempotent-maps`](foundation.split-idempotent-maps.md)
diff --git a/src/foundation/retracts-of-types.lagda.md b/src/foundation/retracts-of-types.lagda.md
index 12a25959b7..ce0fa62ff3 100644
--- a/src/foundation/retracts-of-types.lagda.md
+++ b/src/foundation/retracts-of-types.lagda.md
@@ -93,8 +93,8 @@ module _
   is-equiv-htpy-eq-retract R =
     fundamental-theorem-id (is-torsorial-htpy-retract R) (htpy-eq-retract R)
 
-  equiv-htpy-eq-retract : (R S : A retract-of B) → (R ＝ S) ≃ htpy-retract R S
-  equiv-htpy-eq-retract R S =
+  extensionality-retract : (R S : A retract-of B) → (R ＝ S) ≃ htpy-retract R S
+  extensionality-retract R S =
     ( htpy-eq-retract R S , is-equiv-htpy-eq-retract R S)
 
   eq-htpy-retract : (R S : A retract-of B) → htpy-retract R S → R ＝ S
@@ -158,8 +158,8 @@ module _
   is-equiv-equiv-eq-retracts R =
     fundamental-theorem-id (is-torsorial-equiv-retracts R) (equiv-eq-retracts R)
 
-  equiv-equiv-eq-retracts : (R S : retracts l2 A) → (R ＝ S) ≃ equiv-retracts R S
-  equiv-equiv-eq-retracts R S =
+  extensionality-retracts : (R S : retracts l2 A) → (R ＝ S) ≃ equiv-retracts R S
+  extensionality-retracts R S =
     ( equiv-eq-retracts R S , is-equiv-equiv-eq-retracts R S)
 
   eq-equiv-retracts : (R S : retracts l2 A) → equiv-retracts R S → R ＝ S
diff --git a/src/literature.lagda.md b/src/literature.lagda.md
index 82c74551c7..2731009799 100644
--- a/src/literature.lagda.md
+++ b/src/literature.lagda.md
@@ -1,13 +1,18 @@
 # Formalization of results from the literature
 
+> This page is a work in early progress. To see what's happening behind the
+> scenes, you can have a look at the associated GitHub issue
+> [#1055](https://github.com/UniMath/agda-unimath/issues/1055).
+
 ## References
 
-{{#bibliography}} {{#reference SvDR20}}
+{{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}}
 
 ## Files in the namespace
 
 ```agda
 module literature where
 
+open import literature.idempotents-in-intensional-type-theory public
 open import literature.sequential-colimits-in-homotopy-type-theory public
 ```
diff --git a/src/literature/idempotents-in-intensional-type-theory.lagda.md b/src/literature/idempotents-in-intensional-type-theory.lagda.md
new file mode 100644
index 0000000000..448cd6e695
--- /dev/null
+++ b/src/literature/idempotents-in-intensional-type-theory.lagda.md
@@ -0,0 +1,428 @@
+# Idempotents in Intensional Type Theory
+
+This file collects references to formalization of constructions and theorems
+from {{#cite Shu17}}.
+
+```agda
+module literature.idempotents-in-intensional-type-theory where
+```
+
+## 1 Introduction
+
+The introduction section gives an introduction to the problem at hand and
+motivates its study in univalent foundations.
+
+```agda
+open import group-theory.groups using
+  ( Group
+  )
+
+open import higher-group-theory.higher-groups using
+  ( ∞-Group
+  )
+```
+
+## 2 Some notation and terminology
+
+The second section introduces basic notions from homotopy type theory.
+
+```agda
+open import foundation.dependent-function-types -- "dependent products"
+
+open import foundation.dependent-pair-types -- "dependent sums"
+
+open import foundation.identity-types using
+  ( _＝_ -- "identity type, its elements are paths"
+  ; refl -- "the canonical elements of the identity types"
+  ; concat -- "transitivity of paths"
+  ; inv -- "symmetry of paths"
+  ; ind-Id -- "eliminator of the identity type"
+  )
+
+open import foundation.action-on-identifications-functions using
+  ( ap -- "action of functions on paths"
+  ; ap-comp -- "functoriality of `ap` with respect to function composition"
+  ; ap-concat -- "functoriality of `ap` with respect to transitivity of paths"
+  )
+```
+
+The preferred definition for propositions in the library, `is-prop`, are types
+whose identity types are [contractible](foundation-core.contractible-types.md).
+
+```agda
+open import foundation-core.propositions using
+  ( all-elements-equal -- "mere proposition"
+  ; is-prop -- all identity types are contractible
+  )
+```
+
+The preferred definition for sets in the library, `is-set` are types whose
+identity types are propositions in the preferred sense of the library. While the
+same relation holds for the definitions used in the article, we note that it
+does not extend one dimension lower to contractible types as our scheme does.
+
+```agda
+open import foundation-core.sets using
+  ( has-uip -- "satisfies uip"
+  ; is-set -- all identity types are propositions
+  )
+
+open import foundation.homotopies using
+  ( _~_ -- "homotopy"
+  ; nat-htpy -- "naturality of homotopies"
+  )
+```
+
+The preferred notion of equivalence in the library coincides with the example
+given in the article: an equivalence is a function equipped with a left inverse
+and a right inverse.
+
+```agda
+open import foundation.equivalences using
+  ( is-equiv -- "type of equivalence proofs"
+  ; equiv -- "type of equivalences"
+  ; is-property-is-equiv -- "the type of equivalence proofs is a mere proposition"
+  )
+
+open import foundation.function-extensionality using
+  ( funext -- "the function extensionality axiom"
+  )
+
+open import foundation.univalence using
+  ( equiv-eq -- "the canonical map `(A ＝ B) → (A ≃ B)`"
+  ; univalence -- "the univalence axiom"
+  )
+
+open import foundation.propositional-truncations using
+  ( ║_║₋₁ -- "propositional truncation"
+  ; unit-trunc-Prop -- "the map `A → ║ A ║₋₁`"
+  ; universal-property-trunc-Prop -- "the universal property of propositional truncation"
+  )
+
+open import foundation.mere-equivalences using
+  ( mere-equiv -- "merely equivalent"
+  )
+
+open import foundation.univalence-implies-function-extensionality using
+  ( funext-univalence -- "univalence implies function extensionality"
+  )
+
+-- MISSING: propositional truncations imply function extensionality
+
+open import foundation.equality-cartesian-product-types using
+  ( Eq-product -- observational equality on pairs
+  ; equiv-pair-eq -- "characterization of the identity types of cartesian product type formation"
+  )
+```
+
+## 3 Some pre-idempotents that split
+
+In this section, definitions of "pre-idempotents", "split idempotents" and
+"quasi-idempotents" are given, and basic relations between them are established.
+
+**Definition 3.1.** Pre-idempotents.
+
+The library's preferred terminology for "a pre-idempotent" is "an idempotent".
+We reserve the terminology "a coherent idempotent" for what in the article is
+referred to as "a (fully coherent) idempotent".
+
+```agda
+open import foundation.endomorphisms using
+  ( endo -- "endofunction"
+  )
+
+open import foundation.idempotent-maps using
+  ( is-idempotent -- "idempotency witness"
+  ; idempotent-map -- "pre-idempotent (map)"
+  )
+```
+
+**Definition 3.2.** Retracts and splittings.
+
+```agda
+open import foundation.retracts-of-types using
+  ( retracts -- "retracts of a type"
+  ; retract -- "type of retracts between two types"
+  )
+
+open import foundation.split-idempotent-maps using
+  ( is-split-idempotent -- "splitting of an endofunction"
+  )
+```
+
+**Lemma 3.3.** If $f$ has a splitting, then it is pre-idempotent.
+
+```agda
+open import foundation.split-idempotent-maps using
+  ( is-idempotent-is-split-idempotent
+  )
+```
+
+**Lemma 3.4.** The type associated to a splitting of a map is unique up to
+equivalence.
+
+```agda
+open import foundation.split-idempotent-maps using
+  ( essentially-unique-splitting-type-is-split-idempotent
+  )
+```
+
+**Definition 3.5.** Quasi-idempotents.
+
+The library's preferred terminology for "a quasi-idempotent" is "a quasicoherent
+idempotent".
+
+```agda
+open import foundation.quasicoherently-idempotent-maps using
+  ( is-quasicoherently-idempotent -- "the type of witnesses of quasi-idempotence"
+  ; quasicoherently-idempotent-map -- "the type of quasi-idempotents"
+  )
+```
+
+**Lemma 3.6.** If $f$ has a splitting, then it is a quasi-idempotent.
+
+```agda
+open import foundation.split-idempotent-maps using
+  ( is-quasicoherently-idempotent-is-split-idempotent
+  )
+```
+
+**Theorem 3.7.** If $X$ is a set, then any pre-idempotent on $X$ has a
+splitting.
+
+```agda
+open import foundation.split-idempotent-maps using
+  ( is-split-idempotent-is-idempotent-is-set
+  )
+```
+
+**Example 3.8.**
+
+> This example is not formalized.
+
+**Theorem 3.9.** If a pre-idempotent is weakly constant, then it has a
+splitting.
+
+```agda
+open import foundation.weakly-constant-maps using
+  ( is-weakly-constant -- "the type of witnesses that a map is weakly constant"
+  ; weakly-constant-map -- "the type of weakly constant maps"
+  )
+
+open import foundation.split-idempotent-maps using
+  ( is-split-idempotent-is-weakly-constant-is-idempotent
+  )
+```
+
+**Theorem 3.10.** An endofunction $f$ has a splitting in which the section $s$
+is an embedding if and only if it is pre-idempotent and the type $f(x) = x$
+admits a weakly constant endofunction for all $x$.
+
+```agda
+open import foundation.sections using
+  ( is-section -- "the type of witnesses that a map is a section to a map"
+  ; section -- "the type of sections of a map"
+  )
+
+open import foundation.embeddings using
+  ( is-emb -- "the type of witnesses that a map is an embedding"
+  ; _↪_ -- "the type of embeddings between two types"
+  )
+```
+
+> The proof remains to be formalized.
+> [#1103](https://github.com/UniMath/agda-unimath/issues/1103)
+
+## 4 A pre-idempotent that doesn't split
+
+In this section, assuming univalence and propositional truncations, an example
+is given of a pre-idempotent map that does not split or extend to a
+quasi-idempotent. Such a map is constructed on the
+[connected component of the universe](foundation.connected-components-universes.md)
+at the [cantor space](set-theory.cantor-space.md), i.e., its classifying space.
+
+> This section remains to be formalized.
+> [#1103](https://github.com/UniMath/agda-unimath/issues/1103)
+
+**Example 4.1.** An example of an idempotence witness that cannot be extended to
+a coherent system of idempotence data.
+
+```agda
+-- TODO
+```
+
+**Definition 4.2.** The Cantor space.
+
+```agda
+open import set-theory.cantor-space using
+  ( cantor-space -- "C"
+  )
+```
+
+**Lemma 4.3.** Assuming function extensionality, `C ≃ (C + C)`.
+
+```agda
+-- TODO
+```
+
+**Definition 4.5.** $B\operatorname{Aut}({-})$.
+
+```agda
+open import foundation.connected-components-universes using
+  ( component-UU -- "BAut(-)"
+  )
+```
+
+**Theorem 4.6.** There exists a pre-idempotent on $B\operatorname{Aut}(C)$ that
+does not split.
+
+```agda
+-- TODO
+```
+
+**Corollary 4.7.** It is impossible to prove in MLTT that all pre-idempotents
+split, or even that all pre-idempotents are quasi-idempotent.
+
+The previous theorem shows that in MLTT with univalence and propositional
+truncations the statement that all pre-idempotents split is false. Thus if it
+were provable in MLTT then MLTT with univalence and propositional truncations
+would be inconsistent, but it is not.
+
+## 5 All quasi-idempotents split
+
+In this section it is shown that, assuming function extensionality, every
+quasi-idempotent map splits.
+
+**Example 5.1.** A naïve attempt.
+
+> This example is not formalized.
+
+Sequential colimits of types.
+
+```agda
+open import synthetic-homotopy-theory.sequential-diagrams using
+  ( sequential-diagram
+  )
+
+open import synthetic-homotopy-theory.sequential-colimits using
+  ( standard-sequential-colimit
+  )
+```
+
+Sequential limits of types.
+
+```agda
+open import foundation.inverse-sequential-diagrams using
+  ( inverse-sequential-diagram
+  )
+
+open import foundation.sequential-limits using
+  ( standard-sequential-limit
+  )
+```
+
+**Lemma 5.2.** Characterization of the identity types of sequential limit
+formation.
+
+The formalization generalizes the result of the paper by considering general
+inverse sequential diagrams rather than those that are constantly $f$. Also note
+that compared to the paper, the coherences in the formalization are transposed.
+
+```agda
+open import foundation.sequential-limits using
+  ( Eq-standard-sequential-limit -- observational equality on standard sequential limits
+  ; extensionality-standard-sequential-limit
+  )
+```
+
+**Theorem 5.3.** Assuming function extensionality, any quasi-idempotent splits.
+
+```agda
+open import foundation.split-idempotent-maps using
+  ( is-split-idempotent-is-quasicoherently-idempotent
+  )
+```
+
+**Remark 5.4.** Components of the construction.
+
+```agda
+open import foundation.split-idempotent-maps using
+  ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent'
+  ; splitting-type-is-quasicoherently-idempotent'
+  ; inclusion-splitting-type-is-quasicoherently-idempotent'
+  ; map-retraction-splitting-type-is-quasicoherently-idempotent'
+  ; htpy-is-split-idempotent-is-quasicoherently-idempotent' -- "requires function extensionality"
+  )
+```
+
+## 6 Splitting is a retraction
+
+In this section it is shown, assuming the univalence axiom, that the type of
+splittings of a pre-idempotent map is a retract of the type of extensions to
+quasi-idempotence.
+
+> This section remains to be formalized.
+> [#1103](https://github.com/UniMath/agda-unimath/issues/1103)
+
+**Lemma 6.3.** Characterization of the identity types of retract formation.
+
+```agda
+open import foundation.retracts-of-types using
+  ( equiv-retracts -- observational equality on retracts
+  ; extensionality-retracts
+  )
+```
+
+## 7 Splitting is not an equivalence
+
+In this section, it is argued that there may be more quasi-idempotence witnesses
+than splittings of a map.
+
+> This section remains to be formalized.
+> [#1103](https://github.com/UniMath/agda-unimath/issues/1103)
+
+## 8 The double classifying space of 2
+
+In this section, an explicit example of a type with more quasi-idempotents than
+splittings are worked out using the univalence axiom and propositional
+truncations, proving Theorem 7.4 from the previous section.
+
+> This section remains to be formalized.
+> [#1103](https://github.com/UniMath/agda-unimath/issues/1103)
+
+## 9 Coherent idempotents
+
+In this section, assuming function extensionality, a "homotopy-correct"
+definition of coherently idempotent maps is given.
+
+**Definition 9.1.** (Fully coherent) idempotents.
+
+```agda
+open import foundation.coherently-idempotent-maps using
+  ( is-coherently-idempotent -- "type of (fully coherent) idempotence witnesses"
+  )
+```
+
+## 10 Conclusion
+
+This section of the article features a series of 5 open problems.
+
+> If a resolution to any of these open problems is formalized in the library,
+> then it should be recorded here.
+
+**Open Problem 10.1.** Can quasi-idempotents be split in MLTT without assuming
+function extensionality? In particular, is there a more "finite" way to
+construct such a splitting?
+
+**Open Problem 10.2.** Is the map
+$\operatorname{Idem}(X) → \operatorname{QIdem}(X)$ an embedding?
+
+**Open Problem 10.3.** Is the map
+$\operatorname{Idem}(X) → \operatorname{PIdem}(X)$ an embedding?
+
+**Open Problem 10.4.** Can $\operatorname{Idem}(X)$ be defined without assuming
+function extensionality?
+
+**Open Problem 10.5.** Are there examples of other fully-coherent higher
+homotopy structures that can be obtained from a finite amount of coherence by
+splitting an idempotent?