Pointed homotopies

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

Created on 2022-05-07.
Last modified on 2024-03-13.

module structured-types.pointed-homotopies where

Imports

open import foundation.action-on-higher-identifications-functions
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-equivalences
open import foundation.commuting-triangles-of-identifications
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import foundation-core.torsorial-type-families

open import structured-types.pointed-dependent-functions
open import structured-types.pointed-families-of-types
open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

A pointed homotopy^¶ between pointed dependent functions f := (f₀ , f₁) and g := (g₀ , g₁) of type pointed-Π A B consists of an unpointed homotopy H₀ : f₀ ~ g₀ and an identification H₁ : f₁ ＝ (H₀ *) ∙ g₁ witnessing that the triangle of identifications

        H₀ *
  f₀ * ------> g₀ *
      \       /
    f₁ \     / g₁
        \   /
         ∨ ∨
          *

commutes. This identification is called the base point coherence^¶ of the pointed homotopy H := (H₀ , H₁).

An equivalent way of defining pointed homotopies occurs when we consider the type family x ↦ f₀ x ＝ g₀ x over the base type A. This is a pointed type family, where the base point is the identification

  f₁ ∙ inv g₁ : f₀ * ＝ g₀ *.

A pointed homotopy f ~∗ g is therefore equivalently defined as a pointed dependent function of the pointed type family x ↦ f₀ x ＝ g₀ x. Such a pointed dependent function consists of an unpointed homotopy H₀ : f₀ ~ g₀ between the underlying dependent functions and an identification witnessing that the triangle of identifications

        H₀ *
  f₀ * ------> g₀ *
      \       ∧
    f₁ \     / inv g₁
        \   /
         ∨ /
          *

commutes. Notice that the identification on the right in this triangle goes up, in the inverse direction of the identification g₁.

Note that in this second definition of pointed homotopies we defined pointed homotopies between pointed dependent functions to be certain pointed dependent functions. This implies that the second definition is a uniform definition that can easily be iterated in order to consider pointed higher homotopies. For this reason, we call the second definition of pointed homotopies uniform pointed homotopies.

Note that the difference between our main definition of pointed homotopies and the uniform definition of pointed homotopies is the direction of the identification on the right in the commuting triangle

        H₀ *
  f₀ * ------> g₀ *
      \       /
    f₁ \     / g₁
        \   /
         ∨ ∨
          *.

In the definition of uniform pointed homotopies it goes in the reverse direction. This makes it slightly more complicated to construct an identification witnessing that the triangle commutes in the case of uniform pointed homotopies. Furthermore, this complication becomes more significant and bothersome when we are trying to construct a pointed 2-homotopy. For this reason, our first definition where pointed homotopies are defined to consist of unpointed homotopies and a base point coherence, is taken to be our main definition of pointed homotopy. The only disadvantage of the nonuniform definition of pointed homotopies is that it does not easily iterate.

We will write f ~∗ g for the type of (nonuniform) pointed homotopies, and we will write H ~²∗ K for the nonuniform definition of pointed 2-homotopies.

Definitions

Unpointed homotopies between pointed dependent functions

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A}
  (f g : pointed-Π A B)
  where

  unpointed-htpy-pointed-Π : UU (l1 ⊔ l2)
  unpointed-htpy-pointed-Π = function-pointed-Π f ~ function-pointed-Π g

Unpointed homotopies between pointed maps

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
  (f g : A →∗ B)
  where

  unpointed-htpy-pointed-map : UU (l1 ⊔ l2)
  unpointed-htpy-pointed-map = map-pointed-map f ~ map-pointed-map g

The base point coherence of unpointed homotopies between pointed maps

The base point coherence of pointed homotopies asserts that its underlying homotopy preserves the base point, in the sense that the triangle of identifications

                      H *
                f * ------> g *
                   \       /
  preserves-point f \     / preserves-point g
                     \   /
                      ∨ ∨
                       *

commutes.

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A}
  (f g : pointed-Π A B) (G : unpointed-htpy-pointed-Π f g)
  where

  coherence-point-unpointed-htpy-pointed-Π : UU l2
  coherence-point-unpointed-htpy-pointed-Π =
    coherence-triangle-identifications
      ( preserves-point-function-pointed-Π f)
      ( preserves-point-function-pointed-Π g)
      ( G (point-Pointed-Type A))