Preidempotent maps

module foundation.preidempotent-maps where
Imports 
open import foundation-core.dependent-pair-types
open import foundation-core.functions
open import foundation-core.homotopies
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.universe-levels

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