# Uniform pointed homotopies

```agda
module structured-types.uniform-pointed-homotopies where
```

<details><summary>Imports</summary>

```agda
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
```

</details>

## Idea

The concept of _uniform pointed homotopy_ is an
[equivalent](foundation-core.equivalences.md) way of defining
[pointed homotopies](structured-types.pointed-homotopies.md). A uniform pointed
homotopy `H` between two
[pointed dependent functions](structured-types.pointed-dependent-functions.md)
`f` and `g` is defined to be a pointed dependent function of the
[pointed type family](structured-types.pointed-families-of-types.md) of
[identifications](foundation-core.identity-types.md) 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

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

A {{#concept "uniform pointed homotopy" Agda=uniform-pointed-htpy}} from `f` to
`g` is defined to be a
[pointed dependent function](structured-types.pointed-dependent-functions.md) of
the pointed type family `x ↦ f₀ x ＝ g₀ x`. In other words, a pointed dependent
function consists of an unpointed [homotopy](foundation-core.homotopies.md)
`H₀ : f₀ ~ g₀` between the underlying dependent functions and an identification
witnessing that the triangle of identifications

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

[commutes](foundation.commuting-triangles-of-identifications.md).

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](structured-types.pointed-2-homotopies.md).

## 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

```text
                      H *
                f * ------> g *
                   \       ∧
  preserves-point f \     / inv (preserves-point g)
                     \   /
                      ∨ /
                       *
```

commutes.

```agda
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.

```agda
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

```agda
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

```agda
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

```agda
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

```agda
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)
```