Endomorphisms

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-08-12.
Last modified on 2023-09-13.

module foundation-core.endomorphisms where
Imports 
open import foundation.dependent-pair-types
open import foundation.sets
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

open import structured-types.pointed-types

Idea

An endomorphism on a type A is a map A → A.

Definition

endo : {l : Level} → UU l → UU l
endo A = A → A

endo-Pointed-Type : {l : Level} → UU l → Pointed-Type l
pr1 (endo-Pointed-Type A) = A → A
pr2 (endo-Pointed-Type A) = id

Properties

If the domain is a set the type of endomorphisms is a set

is-set-endo : {l : Level} {A : UU l} → is-set A → is-set (endo A)
is-set-endo is-set-A = is-set-function-type is-set-A

endo-Set : {l : Level} → Set l → Set l
pr1 (endo-Set A) = endo (type-Set A)
pr2 (endo-Set A) = is-set-endo (is-set-type-Set A)

If the domain is k-truncated the type of endomorphisms is k-truncated

is-trunc-endo :
  {l : Level} {A : UU l} (k : 𝕋) → is-trunc k A → is-trunc k (endo A)
is-trunc-endo k is-trunc-A = is-trunc-function-type k is-trunc-A

endo-Truncated-Type :
  {l : Level} (k : 𝕋) → Truncated-Type l k → Truncated-Type l k
pr1 (endo-Truncated-Type k A) = endo (type-Truncated-Type A)
pr2 (endo-Truncated-Type k A) = is-trunc-endo k (is-trunc-type-Truncated-Type A)

See also

Recent changes