Coherently idempotent maps

Content created by Fredrik Bakke.

Created on 2024-08-21.
Last modified on 2024-08-21.

module foundation.coherently-idempotent-maps where
Imports 
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

Idea

A coherently idempotent map is an idempotent map f : A → A equipped with an infinitely coherent hierarchy of homotopies 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 of iterated application of the splitting construction on quasicoherently idempotent maps given in [Shu17]:

  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 and . Our definition of an idempotent map corresponds in their terminology to a pre-idempotent map.

Definitions

The structure on a map of coherent idempotence

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

References

[Shu17]
Michael Shulman. Idempotents in intensional type theory. Logical Methods in Computer Science, 12:1–24, 04 2017. arXiv:1507.03634, doi:10.2168/LMCS-12(3:9)2016.
[Shu14]
Mike Shulman. Splitting Idempotents. Blog post, 12 2014. URL: https://homotopytypetheory.org/2014/12/08/splitting-idempotents/.

Recent changes