Contractible maps
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-09-11.
module foundation.contractible-maps where open import foundation-core.contractible-maps public
Imports
open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.logical-equivalences open import foundation.truncated-maps open import foundation.universe-levels open import foundation-core.propositions open import foundation-core.truncation-levels
Properties
Being a contractible map is a property
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-prop-is-contr-map : (f : A → B) → is-prop (is-contr-map f) is-prop-is-contr-map f = is-prop-is-trunc-map neg-two-𝕋 f is-contr-map-Prop : (A → B) → Prop (l1 ⊔ l2) pr1 (is-contr-map-Prop f) = is-contr-map f pr2 (is-contr-map-Prop f) = is-prop-is-contr-map f
Being a contractible map is equivalent to being an equivalence
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where equiv-is-equiv-is-contr-map : (f : A → B) → is-contr-map f ≃ is-equiv f equiv-is-equiv-is-contr-map f = equiv-iff ( is-contr-map-Prop f) ( is-equiv-Prop f) ( is-equiv-is-contr-map) ( is-contr-map-is-equiv) equiv-is-contr-map-is-equiv : (f : A → B) → is-equiv f ≃ is-contr-map f equiv-is-contr-map-is-equiv f = equiv-iff ( is-equiv-Prop f) ( is-contr-map-Prop f) ( is-contr-map-is-equiv) ( is-equiv-is-contr-map)
See also
- For the notion of biinvertible maps see
foundation.equivalences
. - For the notions of inverses and coherently invertible maps, also known as
half-adjoint equivalences, see
foundation.coherently-invertible-maps
. - For the notion of path-split maps see
foundation.path-split-maps
.
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).