Uniform pointed homotopies

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-03-13.

module structured-types.uniform-pointed-homotopies where
Imports 
open import foundation.commuting-triangles-of-identifications
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.homotopies
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.universe-levels

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

Idea

The concept of uniform pointed homotopy is an equivalent way of defining pointed homotopies. A uniform pointed homotopy H between two pointed dependent functions f and g is defined to be a pointed dependent function of the pointed type family of identifications between the values of f and g. The main idea is that, since uniform pointed homotopies between pointed dependent functions are again pointed dependent functions, we can easily consider uniform pointed homotopies between uniform pointed homotopies and so on. The definition of uniform pointed homotopies is uniform in the sense that they can be iterated in this way. We now give a more detailed description of the definition.

Consider two pointed dependent functions f := (f₀ , f₁) and g := (g₀ , g₁) in the pointed dependent function type Π∗ A B. Then the type family x ↦ f₀ x ＝ g₀ x over the base type A is a pointed type family, where the base point is the identification

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

A uniform pointed homotopy from f to g is defined to be a pointed dependent function of the pointed type family x ↦ f₀ x ＝ g₀ x. In other words, 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 in comparison to the pointed homotopies, the identification on the right in this triangle goes up, in the inverse direction of the identification g₁. 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.

Definitions

Preservation of the base point of unpointed homotopies between pointed maps

The underlying homotopy of a uniform pointed homotopy preserves the base point in the sense that the triangle of identifications

                      H *
                f * ------> g *
                   \       ∧
  preserves-point f \     / inv (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

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

  compute-coherence-point-unpointed-htpy-pointed-Π :
    coherence-point-unpointed-htpy-pointed-Π f g G ≃
    preserves-point-unpointed-htpy-pointed-Π
  compute-coherence-point-unpointed-htpy-pointed-Π =
    equiv-transpose-right-coherence-triangle-identifications _ _ _

  preserves-point-coherence-point-unpointed-htpy-pointed-Π :
    coherence-point-unpointed-htpy-pointed-Π f g G →
    preserves-point-unpointed-htpy-pointed-Π
  preserves-point-coherence-point-unpointed-htpy-pointed-Π =
    transpose-right-coherence-triangle-identifications _ _ _ refl

  coherence-point-preserves-point-unpointed-htpy-pointed-Π :
    preserves-point-unpointed-htpy-pointed-Π →
    coherence-point-unpointed-htpy-pointed-Π f g G
  coherence-point-preserves-point-unpointed-htpy-pointed-Π =
    inv ∘ inv-right-transpose-eq-concat _ _ _

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

  preserves-point-pointed-htpy :
    preserves-point-unpointed-htpy-pointed-Π f g (htpy-pointed-htpy H)
  preserves-point-pointed-htpy =
    preserves-point-coherence-point-unpointed-htpy-pointed-Π f g
      ( htpy-pointed-htpy H)
      ( coherence-point-pointed-htpy H)

Uniform pointed homotopies

Note. The operation htpy-uniform-pointed-htpy that converts a uniform pointed homotopy to an unpointed homotopy is set up with the pointed functions as explicit arguments, because Agda has trouble inferring them.

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

  eq-value-Pointed-Fam : Pointed-Fam l2 A
  pr1 eq-value-Pointed-Fam =
    eq-value (function-pointed-Π f) (function-pointed-Π g)
  pr2 eq-value-Pointed-Fam =
    ( preserves-point-function-pointed-Π f) ∙
    ( inv (preserves-point-function-pointed-Π g))

  uniform-pointed-htpy : UU (l1 ⊔ l2)
  uniform-pointed-htpy = pointed-Π A eq-value-Pointed-Fam

  htpy-uniform-pointed-htpy :
    uniform-pointed-htpy → function-pointed-Π f ~ function-pointed-Π g
  htpy-uniform-pointed-htpy = pr1

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

  preserves-point-uniform-pointed-htpy :
    preserves-point-unpointed-htpy-pointed-Π f g
      ( htpy-uniform-pointed-htpy f g H)
  preserves-point-uniform-pointed-htpy = pr2 H

  coherence-point-uniform-pointed-htpy :
    coherence-point-unpointed-htpy-pointed-Π f g
      ( htpy-uniform-pointed-htpy f g H)
  coherence-point-uniform-pointed-htpy =
    coherence-point-preserves-point-unpointed-htpy-pointed-Π f g
      ( htpy-uniform-pointed-htpy f g H)
      ( preserves-point-uniform-pointed-htpy)

  pointed-htpy-uniform-pointed-htpy : f ~∗ g
  pr1 pointed-htpy-uniform-pointed-htpy =
    htpy-uniform-pointed-htpy f g H
  pr2 pointed-htpy-uniform-pointed-htpy =
    coherence-point-uniform-pointed-htpy

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

  make-uniform-pointed-htpy :
    (G : unpointed-htpy-pointed-Π f g) →
    coherence-point-unpointed-htpy-pointed-Π f g G →
    uniform-pointed-htpy f g
  pr1 (make-uniform-pointed-htpy G p) = G
  pr2 (make-uniform-pointed-htpy G p) =
    preserves-point-coherence-point-unpointed-htpy-pointed-Π f g G p

  uniform-pointed-htpy-pointed-htpy : f ~∗ g → uniform-pointed-htpy f g
  pr1 (uniform-pointed-htpy-pointed-htpy H) = htpy-pointed-htpy H
  pr2 (uniform-pointed-htpy-pointed-htpy H) = preserves-point-pointed-htpy H

  compute-uniform-pointed-htpy : (f ~∗ g) ≃ uniform-pointed-htpy f g
  compute-uniform-pointed-htpy =
    equiv-tot (compute-coherence-point-unpointed-htpy-pointed-Π f g)

The reflexive uniform pointed homotopy

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

  refl-uniform-pointed-htpy : uniform-pointed-htpy f f
  pr1 refl-uniform-pointed-htpy = refl-htpy
  pr2 refl-uniform-pointed-htpy =
    inv (right-inv (preserves-point-function-pointed-Π f))

Concatenation of uniform pointed homotopies

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

  htpy-concat-uniform-pointed-htpy : unpointed-htpy-pointed-Π f h
  htpy-concat-uniform-pointed-htpy =
    htpy-uniform-pointed-htpy f g G ∙h htpy-uniform-pointed-htpy g h H

  coherence-point-concat-uniform-pointed-htpy :
    coherence-point-unpointed-htpy-pointed-Π f h
      ( htpy-concat-uniform-pointed-htpy)
  coherence-point-concat-uniform-pointed-htpy =
    coherence-point-concat-pointed-htpy
      ( pointed-htpy-uniform-pointed-htpy G)
      ( pointed-htpy-uniform-pointed-htpy H)

  concat-uniform-pointed-htpy : uniform-pointed-htpy f h
  concat-uniform-pointed-htpy =
    make-uniform-pointed-htpy
      ( htpy-concat-uniform-pointed-htpy)
      ( coherence-point-concat-uniform-pointed-htpy)

Inverses of uniform pointed homotopies

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

  htpy-inv-uniform-pointed-htpy : unpointed-htpy-pointed-Π g f
  htpy-inv-uniform-pointed-htpy = inv-htpy (htpy-uniform-pointed-htpy f g H)

  coherence-point-inv-uniform-pointed-htpy :
    coherence-point-unpointed-htpy-pointed-Π g f htpy-inv-uniform-pointed-htpy
  coherence-point-inv-uniform-pointed-htpy =
    coherence-point-inv-pointed-htpy
      ( pointed-htpy-uniform-pointed-htpy H)

  inv-uniform-pointed-htpy : uniform-pointed-htpy g f
  inv-uniform-pointed-htpy =
    make-uniform-pointed-htpy
      ( htpy-inv-uniform-pointed-htpy)
      ( coherence-point-inv-uniform-pointed-htpy)

Properties

Extensionality of pointed dependent function types by uniform pointed homotopies

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

  uniform-extensionality-pointed-Π :
    (g : pointed-Π A B) → (f ＝ g) ≃ uniform-pointed-htpy f g
  uniform-extensionality-pointed-Π =
    extensionality-Σ
      ( λ {g} q H →
        H (point-Pointed-Type A) ＝
        preserves-point-function-pointed-Π f ∙
        inv (preserves-point-function-pointed-Π (g , q)))
      ( refl-htpy)
      ( inv (right-inv (preserves-point-function-pointed-Π f)))
      ( λ g → equiv-funext)
      ( λ p →
        ( equiv-right-transpose-eq-concat
          ( refl)
          ( p)
          ( preserves-point-function-pointed-Π f)) ∘e
        ( equiv-inv (preserves-point-function-pointed-Π f) p))

  eq-uniform-pointed-htpy :
    (g : pointed-Π A B) → uniform-pointed-htpy f g → f ＝ g
  eq-uniform-pointed-htpy g = map-inv-equiv (uniform-extensionality-pointed-Π g)

Recent changes