Pointed equivalences
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-05-07.
Last modified on 2024-03-23.
module structured-types.pointed-equivalences where
Imports
open import foundation.action-on-identifications-functions open import foundation.binary-equivalences open import foundation.cartesian-product-types open import foundation.commuting-squares-of-identifications open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.injective-maps open import foundation.path-algebra open import foundation.propositions open import foundation.retractions open import foundation.sections open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.transposition-identifications-along-equivalences open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels open import foundation.whiskering-identifications-concatenation open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-retractions open import structured-types.pointed-sections open import structured-types.pointed-types open import structured-types.postcomposition-pointed-maps open import structured-types.precomposition-pointed-maps open import structured-types.universal-property-pointed-equivalences open import structured-types.whiskering-pointed-homotopies-composition
Idea
A pointed equivalence¶ e : A ≃∗ B consists of an
equivalence e : A ≃ B equipped with an
identification p : e * ＝ * witnessing
that the underlying map of e preserves the base point of A.
The notion of pointed equivalence is described equivalently as a pointed map of which the underlying function is an equivalence, i.e.,
(A ≃∗ B) ≃ Σ (f : A →∗ B), is-equiv (map-pointed-map f)
Furthermore, a pointed equivalence can also be described equivalently as an equivalence in the category of pointed types.
Definitions
The predicate of being a pointed equivalence
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) where is-pointed-equiv : UU (l1 ⊔ l2) is-pointed-equiv = is-equiv (map-pointed-map f) is-prop-is-pointed-equiv : is-prop is-pointed-equiv is-prop-is-pointed-equiv = is-property-is-equiv (map-pointed-map f) is-pointed-equiv-Prop : Prop (l1 ⊔ l2) is-pointed-equiv-Prop = is-equiv-Prop (map-pointed-map f) module _ (H : is-pointed-equiv) where map-inv-is-pointed-equiv : type-Pointed-Type B → type-Pointed-Type A map-inv-is-pointed-equiv = map-inv-is-equiv H is-section-map-inv-is-pointed-equiv : is-section (map-pointed-map f) map-inv-is-pointed-equiv is-section-map-inv-is-pointed-equiv = is-section-map-inv-is-equiv H is-retraction-map-inv-is-pointed-equiv : is-retraction (map-pointed-map f) map-inv-is-pointed-equiv is-retraction-map-inv-is-pointed-equiv = is-retraction-map-inv-is-equiv H preserves-point-map-inv-is-pointed-equiv : map-inv-is-pointed-equiv (point-Pointed-Type B) ＝ point-Pointed-Type A preserves-point-map-inv-is-pointed-equiv = preserves-point-is-retraction-pointed-map f ( map-inv-is-pointed-equiv) ( is-retraction-map-inv-is-pointed-equiv) pointed-map-inv-is-pointed-equiv : B →∗ A pointed-map-inv-is-pointed-equiv = pointed-map-is-retraction-pointed-map f ( map-inv-is-pointed-equiv) ( is-retraction-map-inv-is-pointed-equiv) coherence-point-is-retraction-map-inv-is-pointed-equiv : coherence-point-unpointed-htpy-pointed-Π ( pointed-map-inv-is-pointed-equiv ∘∗ f) ( id-pointed-map) ( is-retraction-map-inv-is-pointed-equiv) coherence-point-is-retraction-map-inv-is-pointed-equiv = coherence-point-is-retraction-pointed-map f ( map-inv-is-pointed-equiv) ( is-retraction-map-inv-is-pointed-equiv) is-pointed-retraction-pointed-map-inv-is-pointed-equiv : is-pointed-retraction f pointed-map-inv-is-pointed-equiv is-pointed-retraction-pointed-map-inv-is-pointed-equiv = is-pointed-retraction-is-retraction-pointed-map f ( map-inv-is-pointed-equiv) ( is-retraction-map-inv-is-pointed-equiv) coherence-point-is-section-map-inv-is-pointed-equiv : coherence-point-unpointed-htpy-pointed-Π ( f ∘∗ pointed-map-inv-is-pointed-equiv) ( id-pointed-map) ( is-section-map-inv-is-pointed-equiv) coherence-point-is-section-map-inv-is-pointed-equiv = ( right-whisker-concat ( ap-concat ( map-pointed-map f) ( inv (ap _ (preserves-point-pointed-map f))) ( _) ∙ ( horizontal-concat-Id² ( ap-inv ( map-pointed-map f) ( ap _ (preserves-point-pointed-map f)) ∙ ( inv ( ap ( inv) ( ap-comp ( map-pointed-map f) ( map-inv-is-pointed-equiv) ( preserves-point-pointed-map f))))) ( inv (coherence-map-inv-is-equiv H (point-Pointed-Type A))))) ( preserves-point-pointed-map f)) ∙ ( assoc ( inv ( ap ( map-pointed-map f ∘ map-inv-is-pointed-equiv) ( preserves-point-pointed-map f))) ( is-section-map-inv-is-pointed-equiv _) ( preserves-point-pointed-map f)) ∙ ( inv ( ( right-unit) ∙ ( left-transpose-eq-concat ( ap ( map-pointed-map f ∘ map-inv-is-pointed-equiv) ( preserves-point-pointed-map f)) ( is-section-map-inv-is-pointed-equiv _) ( ( is-section-map-inv-is-pointed-equiv _) ∙ ( preserves-point-pointed-map f)) ( ( inv (nat-htpy is-section-map-inv-is-pointed-equiv _)) ∙ ( left-whisker-concat ( is-section-map-inv-is-pointed-equiv _) ( ap-id (preserves-point-pointed-map f))))))) is-pointed-section-pointed-map-inv-is-pointed-equiv : is-pointed-section f pointed-map-inv-is-pointed-equiv pr1 is-pointed-section-pointed-map-inv-is-pointed-equiv = is-section-map-inv-is-pointed-equiv pr2 is-pointed-section-pointed-map-inv-is-pointed-equiv = coherence-point-is-section-map-inv-is-pointed-equiv
Pointed equivalences
pointed-equiv : {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) → UU (l1 ⊔ l2) pointed-equiv A B = Σ ( type-Pointed-Type A ≃ type-Pointed-Type B) ( λ e → map-equiv e (point-Pointed-Type A) ＝ point-Pointed-Type B) infix 6 _≃∗_ _≃∗_ = pointed-equiv module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (e : A ≃∗ B) where equiv-pointed-equiv : type-Pointed-Type A ≃ type-Pointed-Type B equiv-pointed-equiv = pr1 e map-pointed-equiv : type-Pointed-Type A → type-Pointed-Type B map-pointed-equiv = map-equiv equiv-pointed-equiv preserves-point-pointed-equiv : map-pointed-equiv (point-Pointed-Type A) ＝ point-Pointed-Type B preserves-point-pointed-equiv = pr2 e pointed-map-pointed-equiv : A →∗ B pr1 pointed-map-pointed-equiv = map-pointed-equiv pr2 pointed-map-pointed-equiv = preserves-point-pointed-equiv is-equiv-map-pointed-equiv : is-equiv map-pointed-equiv is-equiv-map-pointed-equiv = is-equiv-map-equiv equiv-pointed-equiv is-pointed-equiv-pointed-equiv : is-pointed-equiv pointed-map-pointed-equiv is-pointed-equiv-pointed-equiv = is-equiv-map-pointed-equiv pointed-map-inv-pointed-equiv : B →∗ A pointed-map-inv-pointed-equiv = pointed-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) map-inv-pointed-equiv : type-Pointed-Type B → type-Pointed-Type A map-inv-pointed-equiv = map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) preserves-point-map-inv-pointed-equiv : map-inv-pointed-equiv (point-Pointed-Type B) ＝ point-Pointed-Type A preserves-point-map-inv-pointed-equiv = preserves-point-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) is-pointed-section-pointed-map-inv-pointed-equiv : is-pointed-section ( pointed-map-pointed-equiv) ( pointed-map-inv-pointed-equiv) is-pointed-section-pointed-map-inv-pointed-equiv = is-pointed-section-pointed-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) is-section-map-inv-pointed-equiv : is-section ( map-pointed-equiv) ( map-inv-pointed-equiv) is-section-map-inv-pointed-equiv = is-section-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) coherence-point-is-section-map-inv-pointed-equiv : coherence-point-unpointed-htpy-pointed-Π ( pointed-map-pointed-equiv ∘∗ pointed-map-inv-pointed-equiv) ( id-pointed-map) ( is-section-map-inv-pointed-equiv) coherence-point-is-section-map-inv-pointed-equiv = coherence-point-is-section-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) is-pointed-retraction-pointed-map-inv-pointed-equiv : is-pointed-retraction ( pointed-map-pointed-equiv) ( pointed-map-inv-pointed-equiv) is-pointed-retraction-pointed-map-inv-pointed-equiv = is-pointed-retraction-pointed-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) is-retraction-map-inv-pointed-equiv : is-retraction ( map-pointed-equiv) ( map-inv-pointed-equiv) is-retraction-map-inv-pointed-equiv = is-retraction-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv) coherence-point-is-retraction-map-inv-pointed-equiv : coherence-point-unpointed-htpy-pointed-Π ( pointed-map-inv-pointed-equiv ∘∗ pointed-map-pointed-equiv) ( id-pointed-map) ( is-retraction-map-inv-pointed-equiv) coherence-point-is-retraction-map-inv-pointed-equiv = coherence-point-is-retraction-map-inv-is-pointed-equiv ( pointed-map-pointed-equiv) ( is-pointed-equiv-pointed-equiv)
The equivalence between pointed equivalences and the type of pointed maps that are pointed equivalences
module _ {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) where compute-pointed-equiv : (A ≃∗ B) ≃ Σ (A →∗ B) is-pointed-equiv compute-pointed-equiv = equiv-right-swap-Σ inv-compute-pointed-equiv : Σ (A →∗ B) is-pointed-equiv ≃ (A ≃∗ B) inv-compute-pointed-equiv = equiv-right-swap-Σ
The identity pointed equivalence
module _ {l : Level} {A : Pointed-Type l} where id-pointed-equiv : A ≃∗ A pr1 id-pointed-equiv = id-equiv pr2 id-pointed-equiv = refl
Composition of pointed equivalences
module _ {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} where comp-pointed-equiv : (B ≃∗ C) → (A ≃∗ B) → (A ≃∗ C) pr1 (comp-pointed-equiv f e) = equiv-pointed-equiv f ∘e equiv-pointed-equiv e pr2 (comp-pointed-equiv f e) = preserves-point-comp-pointed-map ( pointed-map-pointed-equiv f) ( pointed-map-pointed-equiv e)
Inverses of pointed equivalences
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (e : A ≃∗ B) where abstract is-pointed-equiv-inv-pointed-equiv : is-pointed-equiv (pointed-map-inv-pointed-equiv e) is-pointed-equiv-inv-pointed-equiv = is-equiv-is-invertible ( map-pointed-equiv e) ( is-retraction-map-inv-pointed-equiv e) ( is-section-map-inv-pointed-equiv e) equiv-inv-pointed-equiv : type-Pointed-Type B ≃ type-Pointed-Type A pr1 equiv-inv-pointed-equiv = map-inv-pointed-equiv e pr2 equiv-inv-pointed-equiv = is-pointed-equiv-inv-pointed-equiv inv-pointed-equiv : B ≃∗ A pr1 inv-pointed-equiv = equiv-inv-pointed-equiv pr2 inv-pointed-equiv = preserves-point-map-inv-pointed-equiv e
Properties
Extensionality of the universe of pointed types
module _ {l1 : Level} (A : Pointed-Type l1) where abstract is-torsorial-pointed-equiv : is-torsorial (λ (B : Pointed-Type l1) → A ≃∗ B) is-torsorial-pointed-equiv = is-torsorial-Eq-structure ( is-torsorial-equiv (type-Pointed-Type A)) ( type-Pointed-Type A , id-equiv) ( is-torsorial-Id (point-Pointed-Type A)) extensionality-Pointed-Type : (B : Pointed-Type l1) → (A ＝ B) ≃ (A ≃∗ B) extensionality-Pointed-Type = extensionality-Σ ( λ b e → map-equiv e (point-Pointed-Type A) ＝ b) ( id-equiv) ( refl) ( λ B → equiv-univalence) ( λ a → id-equiv) eq-pointed-equiv : (B : Pointed-Type l1) → A ≃∗ B → A ＝ B eq-pointed-equiv B = map-inv-equiv (extensionality-Pointed-Type B)
Any pointed map satisfying the universal property of pointed equivalences is a pointed equivalence
In other words, any pointed map f : A →∗ B such that precomposing by f
- ∘∗ f : (B →∗ C) → (A →∗ C)
is an equivalence for any pointed type C, is an equivalence.
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) (H : universal-property-pointed-equiv f) where pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv : B →∗ A pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv = map-inv-is-equiv (H A) id-pointed-map map-inv-is-pointed-equiv-universal-property-pointed-equiv : type-Pointed-Type B → type-Pointed-Type A map-inv-is-pointed-equiv-universal-property-pointed-equiv = map-pointed-map pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv preserves-point-map-inv-is-pointed-equiv-universal-property-pointed-equiv : map-inv-is-pointed-equiv-universal-property-pointed-equiv ( point-Pointed-Type B) ＝ point-Pointed-Type A preserves-point-map-inv-is-pointed-equiv-universal-property-pointed-equiv = preserves-point-pointed-map pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv is-pointed-retraction-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv : is-pointed-retraction f pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv is-pointed-retraction-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv = pointed-htpy-eq _ _ (is-section-map-inv-is-equiv (H A) (id-pointed-map)) is-retraction-map-inv-is-pointed-equiv-universal-property-pointed-equiv : is-retraction ( map-pointed-map f) ( map-inv-is-pointed-equiv-universal-property-pointed-equiv) is-retraction-map-inv-is-pointed-equiv-universal-property-pointed-equiv = htpy-pointed-htpy ( is-pointed-retraction-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv) is-pointed-section-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv : is-pointed-section f pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv is-pointed-section-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv = pointed-htpy-eq _ _ ( is-injective-is-equiv (H B) ( eq-pointed-htpy ((f ∘∗ _) ∘∗ f) (id-pointed-map ∘∗ f) ( concat-pointed-htpy ( associative-comp-pointed-map f _ f) ( concat-pointed-htpy ( left-whisker-comp-pointed-htpy f _ _ ( is-pointed-retraction-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv)) ( concat-pointed-htpy ( right-unit-law-comp-pointed-map f) ( inv-left-unit-law-comp-pointed-map f)))))) is-section-map-inv-is-pointed-equiv-universal-property-pointed-equiv : is-section ( map-pointed-map f) ( map-inv-is-pointed-equiv-universal-property-pointed-equiv) is-section-map-inv-is-pointed-equiv-universal-property-pointed-equiv = htpy-pointed-htpy ( is-pointed-section-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv) abstract is-pointed-equiv-universal-property-pointed-equiv : is-pointed-equiv f is-pointed-equiv-universal-property-pointed-equiv = is-equiv-is-invertible ( map-inv-is-pointed-equiv-universal-property-pointed-equiv) ( is-section-map-inv-is-pointed-equiv-universal-property-pointed-equiv) ( is-retraction-map-inv-is-pointed-equiv-universal-property-pointed-equiv)
Any pointed equivalence satisfies the universal property of pointed equivalences
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) where map-inv-universal-property-pointed-equiv-is-pointed-equiv : (H : is-pointed-equiv f) {l : Level} (C : Pointed-Type l) → (A →∗ C) → (B →∗ C) map-inv-universal-property-pointed-equiv-is-pointed-equiv H C = precomp-pointed-map ( pointed-map-inv-is-pointed-equiv f H) ( C) is-section-map-inv-universal-property-pointed-equiv-is-pointed-equiv : (H : is-pointed-equiv f) → {l : Level} (C : Pointed-Type l) → is-section ( precomp-pointed-map f C) ( map-inv-universal-property-pointed-equiv-is-pointed-equiv ( H) ( C)) is-section-map-inv-universal-property-pointed-equiv-is-pointed-equiv H C h = eq-pointed-htpy ( (h ∘∗ pointed-map-inv-is-pointed-equiv f H) ∘∗ f) ( h) ( concat-pointed-htpy ( associative-comp-pointed-map h ( pointed-map-inv-is-pointed-equiv f H) ( f)) ( left-whisker-comp-pointed-htpy h ( pointed-map-inv-is-pointed-equiv f H ∘∗ f) ( id-pointed-map) ( is-pointed-retraction-pointed-map-inv-is-pointed-equiv f H))) section-universal-property-pointed-equiv-is-pointed-equiv : (H : is-pointed-equiv f) → {l : Level} (C : Pointed-Type l) → section (precomp-pointed-map f C) pr1 (section-universal-property-pointed-equiv-is-pointed-equiv H C) = map-inv-universal-property-pointed-equiv-is-pointed-equiv H C pr2 (section-universal-property-pointed-equiv-is-pointed-equiv H C) = is-section-map-inv-universal-property-pointed-equiv-is-pointed-equiv ( H) ( C) is-retraction-map-inv-universal-property-pointed-equiv-is-pointed-equiv : (H : is-pointed-equiv f) → {l : Level} (C : Pointed-Type l) → is-retraction ( precomp-pointed-map f C) ( map-inv-universal-property-pointed-equiv-is-pointed-equiv ( H) ( C)) is-retraction-map-inv-universal-property-pointed-equiv-is-pointed-equiv H C h = eq-pointed-htpy ( (h ∘∗ f) ∘∗ pointed-map-inv-is-pointed-equiv f H) ( h) ( concat-pointed-htpy ( associative-comp-pointed-map h f ( pointed-map-inv-is-pointed-equiv f H)) ( left-whisker-comp-pointed-htpy h ( f ∘∗ pointed-map-inv-is-pointed-equiv f H) ( id-pointed-map) ( is-pointed-section-pointed-map-inv-is-pointed-equiv f H))) retraction-universal-property-pointed-equiv-is-pointed-equiv : (H : is-pointed-equiv f) → {l : Level} (C : Pointed-Type l) → retraction (precomp-pointed-map f C) pr1 (retraction-universal-property-pointed-equiv-is-pointed-equiv H C) = map-inv-universal-property-pointed-equiv-is-pointed-equiv H C pr2 (retraction-universal-property-pointed-equiv-is-pointed-equiv H C) = is-retraction-map-inv-universal-property-pointed-equiv-is-pointed-equiv ( H) ( C) abstract universal-property-pointed-equiv-is-pointed-equiv : is-pointed-equiv f → universal-property-pointed-equiv f pr1 (universal-property-pointed-equiv-is-pointed-equiv H C) = section-universal-property-pointed-equiv-is-pointed-equiv H C pr2 (universal-property-pointed-equiv-is-pointed-equiv H C) = retraction-universal-property-pointed-equiv-is-pointed-equiv H C equiv-precomp-pointed-map : {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (C : Pointed-Type l3) → (A ≃∗ B) → (B →∗ C) ≃ (A →∗ C) pr1 (equiv-precomp-pointed-map C f) g = g ∘∗ (pointed-map-pointed-equiv f) pr2 (equiv-precomp-pointed-map C f) = universal-property-pointed-equiv-is-pointed-equiv ( pointed-map-pointed-equiv f) ( is-equiv-map-pointed-equiv f) ( C)
Postcomposing by pointed equivalences is a pointed equivalence
The predicate of being an equivalence by postcomposition of pointed maps
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) where is-equiv-postcomp-pointed-map : UUω is-equiv-postcomp-pointed-map = {l : Level} (X : Pointed-Type l) → is-equiv (postcomp-pointed-map f X)
Any pointed map that is an equivalence by postcomposition is a pointed equivalence
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) (H : is-equiv-postcomp-pointed-map f) where pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map : B →∗ A pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map = map-inv-is-equiv (H B) id-pointed-map map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map : type-Pointed-Type B → type-Pointed-Type A map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map = map-pointed-map ( pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) is-pointed-section-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map : is-pointed-section f ( pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) is-pointed-section-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map = pointed-htpy-eq ( f ∘∗ pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) ( id-pointed-map) ( is-section-map-inv-is-equiv (H B) id-pointed-map) is-section-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map : is-section ( map-pointed-map f) ( map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) is-section-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map = htpy-pointed-htpy ( is-pointed-section-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) is-pointed-retraction-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map : is-pointed-retraction f ( pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) is-pointed-retraction-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map = pointed-htpy-eq ( pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map ∘∗ f) ( id-pointed-map) ( is-injective-is-equiv ( H A) ( eq-pointed-htpy ( ( f) ∘∗ ( ( pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) ∘∗ ( f))) ( f ∘∗ id-pointed-map) ( concat-pointed-htpy ( inv-associative-comp-pointed-map f _ f) ( concat-pointed-htpy ( right-whisker-comp-pointed-htpy ( f ∘∗ _) ( id-pointed-map) ( is-pointed-section-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) ( f)) ( concat-pointed-htpy ( left-unit-law-comp-pointed-map f) ( inv-pointed-htpy (right-unit-law-comp-pointed-map f))))))) is-retraction-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map : is-retraction ( map-pointed-map f) ( map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) is-retraction-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map = htpy-pointed-htpy ( is-pointed-retraction-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) abstract is-pointed-equiv-is-equiv-postcomp-pointed-map : is-pointed-equiv f is-pointed-equiv-is-equiv-postcomp-pointed-map = is-equiv-is-invertible ( map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) ( is-section-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) ( is-retraction-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map)
Any pointed equivalence is an equivalence by postcomposition
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) (H : is-pointed-equiv f) where map-inv-is-equiv-postcomp-is-pointed-equiv : {l : Level} (X : Pointed-Type l) → (X →∗ B) → (X →∗ A) map-inv-is-equiv-postcomp-is-pointed-equiv = postcomp-pointed-map (pointed-map-inv-is-pointed-equiv f H) is-section-map-inv-is-equiv-postcomp-is-pointed-equiv : {l : Level} (X : Pointed-Type l) → is-section ( postcomp-pointed-map f X) ( map-inv-is-equiv-postcomp-is-pointed-equiv X) is-section-map-inv-is-equiv-postcomp-is-pointed-equiv X h = eq-pointed-htpy ( f ∘∗ (pointed-map-inv-is-pointed-equiv f H ∘∗ h)) ( h) ( concat-pointed-htpy ( inv-associative-comp-pointed-map f ( pointed-map-inv-is-pointed-equiv f H) ( h)) ( concat-pointed-htpy ( right-whisker-comp-pointed-htpy ( f ∘∗ pointed-map-inv-is-pointed-equiv f H) ( id-pointed-map) ( is-pointed-section-pointed-map-inv-is-pointed-equiv f H) ( h)) ( left-unit-law-comp-pointed-map h))) is-retraction-map-inv-is-equiv-postcomp-is-pointed-equiv : {l : Level} (X : Pointed-Type l) → is-retraction ( postcomp-pointed-map f X) ( map-inv-is-equiv-postcomp-is-pointed-equiv X) is-retraction-map-inv-is-equiv-postcomp-is-pointed-equiv X h = eq-pointed-htpy ( pointed-map-inv-is-pointed-equiv f H ∘∗ (f ∘∗ h)) ( h) ( concat-pointed-htpy ( inv-associative-comp-pointed-map ( pointed-map-inv-is-pointed-equiv f H) ( f) ( h)) ( concat-pointed-htpy ( right-whisker-comp-pointed-htpy ( pointed-map-inv-is-pointed-equiv f H ∘∗ f) ( id-pointed-map) ( is-pointed-retraction-pointed-map-inv-is-pointed-equiv f H) ( h)) ( left-unit-law-comp-pointed-map h))) abstract is-equiv-postcomp-is-pointed-equiv : is-equiv-postcomp-pointed-map f is-equiv-postcomp-is-pointed-equiv X = is-equiv-is-invertible ( map-inv-is-equiv-postcomp-is-pointed-equiv X) ( is-section-map-inv-is-equiv-postcomp-is-pointed-equiv X) ( is-retraction-map-inv-is-equiv-postcomp-is-pointed-equiv X) equiv-postcomp-pointed-map : {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (C : Pointed-Type l3) → (A ≃∗ B) → (C →∗ A) ≃ (C →∗ B) pr1 (equiv-postcomp-pointed-map C e) = postcomp-pointed-map (pointed-map-pointed-equiv e) C pr2 (equiv-postcomp-pointed-map C e) = is-equiv-postcomp-is-pointed-equiv ( pointed-map-pointed-equiv e) ( is-pointed-equiv-pointed-equiv e) ( C)
The composition operation on pointed equivalences is a binary equivalence
module _ {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} where abstract is-equiv-comp-pointed-equiv : (f : B ≃∗ C) → is-equiv (λ (e : A ≃∗ B) → comp-pointed-equiv f e) is-equiv-comp-pointed-equiv f = is-equiv-map-Σ _ ( is-equiv-postcomp-equiv-equiv (equiv-pointed-equiv f)) ( λ e → is-equiv-comp _ ( ap (map-pointed-equiv f)) ( is-emb-is-equiv (is-equiv-map-pointed-equiv f) _ _) ( is-equiv-concat' _ (preserves-point-pointed-equiv f))) equiv-comp-pointed-equiv : (f : B ≃∗ C) → (A ≃∗ B) ≃ (A ≃∗ C) pr1 (equiv-comp-pointed-equiv f) = comp-pointed-equiv f pr2 (equiv-comp-pointed-equiv f) = is-equiv-comp-pointed-equiv f abstract is-equiv-comp-pointed-equiv' : (e : A ≃∗ B) → is-equiv (λ (f : B ≃∗ C) → comp-pointed-equiv f e) is-equiv-comp-pointed-equiv' e = is-equiv-map-Σ _ ( is-equiv-precomp-equiv-equiv (equiv-pointed-equiv e)) ( λ f → is-equiv-concat ( ap (map-equiv f) (preserves-point-pointed-equiv e)) ( _)) equiv-comp-pointed-equiv' : (e : A ≃∗ B) → (B ≃∗ C) ≃ (A ≃∗ C) pr1 (equiv-comp-pointed-equiv' e) f = comp-pointed-equiv f e pr2 (equiv-comp-pointed-equiv' e) = is-equiv-comp-pointed-equiv' e abstract is-binary-equiv-comp-pointed-equiv : is-binary-equiv (λ (f : B ≃∗ C) (e : A ≃∗ B) → comp-pointed-equiv f e) pr1 is-binary-equiv-comp-pointed-equiv = is-equiv-comp-pointed-equiv' pr2 is-binary-equiv-comp-pointed-equiv = is-equiv-comp-pointed-equiv
Recent changes
- 2024-03-23. Egbert Rijke. Deloopings and Eilenberg-Mac Lane spaces (#1079).
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).
- 2024-02-06. Fredrik Bakke. Rename
(co)prodto(co)product(#1017). - 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-31. Fredrik Bakke. Rename
is-torsorial-pathtois-torsorial-Id(#1016).