Literature – Idempotents in Intensional Type Theory (#1160)

Adds a literature file for the article _Idempotents in Intensional Type
Theory_ by Shulman. Most of sections 1-3, 5, and 9 are formalized.

#1103 #1055

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,

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

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

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

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

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)

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

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