Preidempotent maps

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-04-28.
Last modified on 2023-11-01.

module foundation.preidempotent-maps where
Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.sets

Idea

A preidempotent map is a map f : A → A equipped with a homotopy f ∘ f ~ f.

Definition

is-preidempotent : {l : Level} {A : UU l}  (A  A)  UU l
is-preidempotent f = (f  f) ~ f

preidempotent-map : {l : Level} (A : UU l)  UU l
preidempotent-map A = Σ (A  A) is-preidempotent

Properties

Being preidempotent over a set is a property

is-prop-is-preidempotent-is-set :
  {l : Level} {A : UU l}  is-set A  (f : A  A)  is-prop (is-preidempotent f)
is-prop-is-preidempotent-is-set is-set-A f =
  is-prop-Π λ x  is-set-A (f (f x)) (f x)

References

Recent changes