# Pointed retractions of pointed maps ```agda module structured-types.pointed-retractions where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.retractions open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-types ``` </details> ## Idea A {{#concept "pointed retraction" Disambiguation="pointed map" Agda=pointed-retraction}} of a [pointed map](structured-types.pointed-maps.md) `f : A →∗ B` consists of a pointed map `g : B →∗ A` equipped with a [pointed homotopy](structured-types.pointed-homotopies.md) `H : g ∘∗ f ~∗ id`. ## Definitions ### The predicate of being a pointed retraction of a pointed map ```agda module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) where is-pointed-retraction : (B →∗ A) → UU l1 is-pointed-retraction g = g ∘∗ f ~∗ id-pointed-map ``` ### The type of pointed retractions of a pointed map ```agda module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) where pointed-retraction : UU (l1 ⊔ l2) pointed-retraction = Σ (B →∗ A) (is-pointed-retraction f) module _ (r : pointed-retraction) where pointed-map-pointed-retraction : B →∗ A pointed-map-pointed-retraction = pr1 r is-pointed-retraction-pointed-retraction : is-pointed-retraction f pointed-map-pointed-retraction is-pointed-retraction-pointed-retraction = pr2 r map-pointed-retraction : type-Pointed-Type B → type-Pointed-Type A map-pointed-retraction = map-pointed-map pointed-map-pointed-retraction preserves-point-pointed-map-pointed-retraction : map-pointed-retraction (point-Pointed-Type B) = point-Pointed-Type A preserves-point-pointed-map-pointed-retraction = preserves-point-pointed-map pointed-map-pointed-retraction is-retraction-pointed-retraction : is-retraction (map-pointed-map f) map-pointed-retraction is-retraction-pointed-retraction = htpy-pointed-htpy is-pointed-retraction-pointed-retraction retraction-pointed-retraction : retraction (map-pointed-map f) pr1 retraction-pointed-retraction = map-pointed-retraction pr2 retraction-pointed-retraction = is-retraction-pointed-retraction coherence-point-is-retraction-pointed-retraction : coherence-point-unpointed-htpy-pointed-Π ( pointed-map-pointed-retraction ∘∗ f) ( id-pointed-map) ( is-retraction-pointed-retraction) coherence-point-is-retraction-pointed-retraction = coherence-point-pointed-htpy is-pointed-retraction-pointed-retraction ``` ## Properties ### Any retraction of a pointed map preserves the base point in a unique way making the retracting homotopy pointed Consider a [retraction](foundation-core.retractions.md) `g : B → A` of a pointed map `f := (f₀ , f₁) : A →∗ B`. Then `g` is base point preserving. **Proof.** Our goal is to show that `g * = *`. Since `f` is pointed, we have `f * = *` and hence ```text (ap g f₁)⁻¹ H * g * -------------> g (f₀ *) -------> *. ``` In order to show that the retracting homotopy `H : g ∘ f₀ ~ id` is pointed, we have to show that the triangle of identifications ```text H * g (f₀ *) -----> * \ / ap g f₁ ∙ ((ap g f₁)⁻¹ ∙ H *) \ / refl \ / ∨ ∨ * ``` commutes. This follows by the fact that concatenating with an inverse identification is inverse to concatenating with the original identification, and the right unit law of concatenation. Note that the pointing of `g` chosen above is the unique way making the retracting homotopy pointed, because the map `p ↦ ap g f₁ ∙ p` is an equivalence with a contractible fiber at `H * ∙ refl`. ```agda module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) (g : type-Pointed-Type B → type-Pointed-Type A) (H : is-retraction (map-pointed-map f) g) where abstract uniquely-preserves-point-is-retraction-pointed-map : is-contr ( Σ ( g (point-Pointed-Type B) = point-Pointed-Type A) ( coherence-square-identifications ( H (point-Pointed-Type A)) ( ap g (preserves-point-pointed-map f)) ( refl))) uniquely-preserves-point-is-retraction-pointed-map = is-contr-map-is-equiv ( is-equiv-concat (ap g (preserves-point-pointed-map f)) _) ( H (point-Pointed-Type A) ∙ refl) preserves-point-is-retraction-pointed-map : g (point-Pointed-Type B) = point-Pointed-Type A preserves-point-is-retraction-pointed-map = inv (ap g (preserves-point-pointed-map f)) ∙ H (point-Pointed-Type A) pointed-map-is-retraction-pointed-map : B →∗ A pr1 pointed-map-is-retraction-pointed-map = g pr2 pointed-map-is-retraction-pointed-map = preserves-point-is-retraction-pointed-map coherence-point-is-retraction-pointed-map : coherence-point-unpointed-htpy-pointed-Π ( pointed-map-is-retraction-pointed-map ∘∗ f) ( id-pointed-map) ( H) coherence-point-is-retraction-pointed-map = ( is-section-inv-concat (ap g (preserves-point-pointed-map f)) _) ∙ ( inv right-unit) is-pointed-retraction-is-retraction-pointed-map : is-pointed-retraction f pointed-map-is-retraction-pointed-map pr1 is-pointed-retraction-is-retraction-pointed-map = H pr2 is-pointed-retraction-is-retraction-pointed-map = coherence-point-is-retraction-pointed-map ```