Splitting idempotents (#1105)

### Summary
- Retracts of a type
  - Define retracts of a type 
  - Characterize equality of retracts
- Weakly constant maps
  - The type of fixed points of weakly constant maps is a proposition
- Idempotent maps
- Rename "preidempotent maps" to "idempotent maps". This mirrors how we
treat "invertible maps" vs "coherently invertible maps", although there
is an essential difference between the two concepts: idempotent maps are
not "coherentifiable" like invertible maps. That role is taken by
"quasicoherently idempotent maps" instead.
- Quasicoherently idempotent maps (called "quasiidempotent maps" in
[Shu17])
  - Define quasicoherently idempotent maps
- Quasicoherently idempotent maps are closed under homotopy (without
funext)
- Split idempotent maps
  - Define split idempotent maps
  - Split idempotent maps are quasicoherently idempotent
  - Idempotent maps on sets split
  - Weakly constant idempotent maps split
  - Quasicoherently idempotent maps split
- Retracts of small types are small

Work towards #1103.

references.bib

@@ -23,7 +23,6 @@ @online{BCDE21
   url    = {https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.Free.html}
 }
 
-
 @online{BCFR23,
   title       = {Central {{H-spaces}} and Banded Types},
   author      = {Buchholtz, Ulrik and Christensen, J. Daniel and Flaten, Jarl G. Taxerås and Rijke, Egbert},
@@ -38,6 +37,21 @@ @online{BCFR23
   keywords    = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic}
 }
 
+@online{BdJR24,
+  title       = {Epimorphisms and {{Acyclic Types}} in {{Univalent Mathematics}}},
+  author      = {Buchholtz, Ulrik and {{de}} Jong, Tom and Rijke, Egbert},
+  citeas      = {BdJR24},
+  date        = {2024-01-25},
+  year        = {2024},
+  month       = {01},
+  eprint      = {2401.14106},
+  eprinttype  = {arxiv},
+  eprintclass = {cs, math},
+  abstract    = {We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.},
+  pubstate    = {preprint},
+  keywords    = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory}
+}
+
 @online{BDR18,
   title       = {Higher {{Groups}} in {{Homotopy Type Theory}}},
   author      = {Buchholtz, Ulrik and {{van}} Doorn, Floris and Rijke, Egbert},
@@ -53,21 +67,6 @@ @online{BDR18
   keywords    = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic}
 }
 
-@online{BJR24,
-  title       = {Epimorphisms and {{Acyclic Types}} in {{Univalent Mathematics}}},
-  author      = {Buchholtz, Ulrik and {{de}} Jong, Tom and Rijke, Egbert},
-  citeas      = {BJR24},
-  date        = {2024-01-25},
-  year        = {2024},
-  month       = {01},
-  eprint      = {2401.14106},
-  eprinttype  = {arxiv},
-  eprintclass = {cs, math},
-  abstract    = {We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.},
-  pubstate    = {preprint},
-  keywords    = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory}
-}
-
 @book{BSCS05,
   title     = {Absztrakt algebrai feladatok},
   author    = {Bálintné Szendrei, Mária and Czédli, Gábor and Szendrei, Ágnes},
@@ -139,6 +138,40 @@ @article{CR21
   keywords    = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory}
 }
 
+@article{dJE23,
+  title       = {{On Small Types in Univalent Foundations}},
+  author      = {{{de}} Jong, Tom and  Escardó, Martín Hötzel},
+  url         = {https://lmcs.episciences.org/11270},
+  doi         = {10.46298/lmcs-19(2:8)2023},
+  journal     = {{Logical Methods in Computer Science}},
+  volume      = {19},
+  issue       = {2},
+  year        = {2023},
+  month       = {05},
+  keywords    = {Computer Science - Logic in Computer Science ; Mathematics - Logic},
+  eprint      = {2111.00482},
+  eprinttype  = {arxiv},
+  eprintclass = {cs},
+  citeas      = {dJE23}
+}
+
+@inproceedings{dJKFC23,
+  title       = {Set-{{Theoretic}} and {{Type-Theoretic Ordinals Coincide}}},
+  booktitle   = {2023 38th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})},
+  author      = {{{de}} Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie},
+  citeas      = {dJKFC23},
+  date        = {2023-06-26},
+  year        = {2023},
+  month       = {06},
+  eprint      = {2301.10696},
+  eprinttype  = {arxiv},
+  eprintclass = {cs, math},
+  pages       = {1--13},
+  doi         = {10.1109/LICS56636.2023.10175762},
+  abstract    = {In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.},
+  keywords    = {Computer Science - Logic in Computer Science,Mathematics - Logic}
+}
+
 @online{Dlicata335/Cohesion-Agda,
   title        = {Dlicata335/Cohesion-Agda},
   author       = {Licata, Dan},
@@ -218,21 +251,20 @@ @online{GGMS24
   keywords    = {Computer Science - Logic in Computer Science,Mathematics - Logic}
 }
 
-@inproceedings{JKFC23,
-  title       = {Set-{{Theoretic}} and {{Type-Theoretic Ordinals Coincide}}},
-  booktitle   = {2023 38th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})},
-  author      = {{{de}} Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie},
-  citeas      = {JKFC23},
-  date        = {2023-06-26},
-  year        = {2023},
-  month       = {06},
-  eprint      = {2301.10696},
+@article{KECA17,
+  title       = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}},
+  author      = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch},
+  url         = {https://lmcs.episciences.org/3217},
+  doi         = {10.23638/LMCS-13(1:15)2017},
+  journal     = {{Logical Methods in Computer Science}},
+  volume      = {13},
+  issue       = {1},
+  year        = {2017},
+  month       = {03},
+  keywords    = {Computer Science - Logic in Computer Science ; 03B15 ; F.4.1},
+  eprint      = {1610.03346},
   eprinttype  = {arxiv},
-  eprintclass = {cs, math},
-  pages       = {1--13},
-  doi         = {10.1109/LICS56636.2023.10175762},
-  abstract    = {In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.},
-  keywords    = {Computer Science - Logic in Computer Science,Mathematics - Logic}
+  eprintclass = {cs}
 }
 
 @book{May12,

src/elementary-number-theory/natural-numbers.lagda.md

@@ -11,6 +11,7 @@ open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.empty-types
+open import foundation-core.function-types
 open import foundation-core.identity-types
 open import foundation-core.injective-maps
 open import foundation-core.negation
@@ -34,6 +35,15 @@ data ℕ : UU lzero where
   succ-ℕ : ℕ → ℕ
 
 {-# BUILTIN NATURAL ℕ #-}
+
+second-succ-ℕ : ℕ → ℕ
+second-succ-ℕ = succ-ℕ ∘ succ-ℕ
+
+third-succ-ℕ : ℕ → ℕ
+third-succ-ℕ = succ-ℕ ∘ second-succ-ℕ
+
+fourth-succ-ℕ : ℕ → ℕ
+fourth-succ-ℕ = succ-ℕ ∘ third-succ-ℕ
 ```
 
 ### Useful predicates on the natural numbers

src/foundation-core.lagda.md

@@ -48,6 +48,7 @@ open import foundation-core.propositional-maps public
 open import foundation-core.propositions public
 open import foundation-core.pullbacks public
 open import foundation-core.retractions public
+open import foundation-core.retracts-of-types public
 open import foundation-core.sections public
 open import foundation-core.sets public
 open import foundation-core.small-types public

src/foundation-core/coherently-invertible-maps.lagda.md

@@ -31,7 +31,7 @@ open import foundation-core.whiskering-homotopies-concatenation
 
 A [(two-sided) inverse](foundation-core.invertible-maps.md) for a map
 `f : A → B` is a map `g : B → A` equipped with
-[homotopies](foundation-core.homotopies.md) ` S : f ∘ g ~ id` and
+[homotopies](foundation-core.homotopies.md) `S : f ∘ g ~ id` and
 `R : g ∘ f ~ id`. Such data, however is [structure](foundation.structure.md) on
 the map `f`, and not generally a [property](foundation-core.propositions.md).
 One way to make the type of inverses into a property is by adding a single

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

@@ -12,14 +12,14 @@ open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-extensionality
 open import foundation.implicit-function-types
-open import foundation.retracts-of-types
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
 open import foundation-core.homotopies
 open import foundation-core.identity-types
+open import foundation-core.retracts-of-types
 open import foundation-core.transport-along-identifications
 ```
 

src/foundation-core/homotopies.lagda.md

@@ -227,6 +227,18 @@ module _
   inv-htpy-right-inv-htpy = inv-htpy right-inv-htpy
 ```
 
+### Inverting homotopies is an involution
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  {f g : (x : A) → B x} (H : f ~ g)
+  where
+
+  inv-inv-htpy : inv-htpy (inv-htpy H) ~ H
+  inv-inv-htpy = inv-inv ∘ H
+```
+
 ### Distributivity of `inv` over `concat` for homotopies
 
 ```agda
@@ -328,6 +340,46 @@ module _
   ap-inv-htpy K x = ap inv (K x)
 ```
 
+### Concatenating with an inverse homotopy is inverse to concatenating
+
+We show that the operation `K ↦ inv-htpy H ∙h K` is inverse to the operation
+`K ↦ H ∙h K` by constructing homotopies
+
+```text
+  inv-htpy H ∙h (H ∙h K) ~ K
+  H ∙h (inv H ∙h K) ~ K.
+```
+
+Similarly, we show that the operation `H ↦ H ∙h inv-htpy K` is inverse to the
+operation `H ↦ H ∙h K` by constructing homotopies
+
+```text
+  (H ∙h K) ∙h inv-htpy K ~ H
+  (H ∙h inv-htpy K) ∙h K ~ H.
+```
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
+  where
+
+  is-retraction-inv-concat-htpy :
+    (H : f ~ g) (K : g ~ h) → inv-htpy H ∙h (H ∙h K) ~ K
+  is-retraction-inv-concat-htpy H K x = is-retraction-inv-concat (H x) (K x)
+
+  is-section-inv-concat-htpy :
+    (H : f ~ g) (L : f ~ h) → H ∙h (inv-htpy H ∙h L) ~ L
+  is-section-inv-concat-htpy H L x = is-section-inv-concat (H x) (L x)
+
+  is-retraction-inv-concat-htpy' :
+    (K : g ~ h) (H : f ~ g) → (H ∙h K) ∙h inv-htpy K ~ H
+  is-retraction-inv-concat-htpy' K H x = is-retraction-inv-concat' (K x) (H x)
+
+  is-section-inv-concat-htpy' :
+    (K : g ~ h) (L : f ~ h) → (L ∙h inv-htpy K) ∙h K ~ L
+  is-section-inv-concat-htpy' K L x = is-section-inv-concat' (K x) (L x)
+```
+
 ## Reasoning with homotopies
 
 Homotopies can be constructed by equational reasoning in the following way:

src/foundation-core/identity-types.lagda.md

@@ -421,7 +421,7 @@ module _
 
   double-transpose-eq-concat :
     {x y u v : A} (r : x ＝ u) (p : x ＝ y) (s : u ＝ v) (q : y ＝ v) →
-    p ∙ q ＝ r ∙ s → (inv r) ∙ p ＝ s ∙ (inv q)
+    p ∙ q ＝ r ∙ s → inv r ∙ p ＝ s ∙ inv q
   double-transpose-eq-concat refl p s refl α =
     (inv right-unit ∙ α) ∙ inv right-unit
 

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

@@ -24,10 +24,11 @@ open import foundation-core.sections
 
 ## Idea
 
-An **inverse** for a map `f : A → B` is a map `g : B → A` equipped with
-[homotopies](foundation-core.homotopies.md) ` (f ∘ g) ~ id` and `(g ∘ f) ~ id`.
-Such data, however is [structure](foundation.structure.md) on the map `f`, and
-not generally a [property](foundation-core.propositions.md).
+An {{#concept "inverse" Disambiguation="maps of types" Agda=is-inverse}} for a
+map `f : A → B` is a map `g : B → A` equipped with
+[homotopies](foundation-core.homotopies.md) `f ∘ g ~ id` and `g ∘ f ~ id`. Such
+data, however, is [structure](foundation.structure.md) on the map `f`, and not
+generally a [property](foundation-core.propositions.md).
 
 ## Definition
 

src/foundation-core/retractions.lagda.md

@@ -240,6 +240,6 @@ module _
 ## See also
 
 - Retracts of types are defined in
-  [`foundation.retracts-of-types`](foundation.retracts-of-types.md).
+  [`foundation-core.retracts-of-types`](foundation-core.retracts-of-types.md).
 - Retracts of maps are defined in
   [`foundation.retracts-of-maps`](foundation.retracts-of-maps.md).