# Pointed homotopies
```agda
module structured-types.pointed-homotopies where
```
<details><summary>Imports</summary>
```agda
open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.whiskering-homotopies
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
```
</details>
## Idea
A pointed homotopy between pointed dependent functions is a pointed dependent
function of the pointed family of pointwise identifications. Since pointed
homotopies are defined for pointed dependent functions, a pointed homotopy
between pointed homotopies is just an instance of a pointed homotopy.
## Definition
```agda
module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A}
(f : pointed-Π A B)
where
htpy-pointed-Π : pointed-Π A B → UU (l1 ⊔ l2)
htpy-pointed-Π g =
pointed-Π A
( pair
( λ x →
Id
( function-pointed-Π f x)
( function-pointed-Π g x))
( ( preserves-point-function-pointed-Π f) ∙
( inv (preserves-point-function-pointed-Π g))))
extensionality-pointed-Π : (g : pointed-Π A B) → Id f g ≃ htpy-pointed-Π g
extensionality-pointed-Π =
extensionality-Σ
( λ {g} q H →
Id
( 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-htpy-pointed-Π :
(g : pointed-Π A B) → (htpy-pointed-Π g) → Id f g
eq-htpy-pointed-Π g = map-inv-equiv (extensionality-pointed-Π g)
_~∗_ :
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
pointed-Π A B → pointed-Π A B → UU (l1 ⊔ l2)
_~∗_ {A = A} {B} = htpy-pointed-Π
infix 6 _~∗_
htpy-pointed-htpy :
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
(f g : pointed-Π A B) → f ~∗ g →
function-pointed-Π f ~ function-pointed-Π g
htpy-pointed-htpy f g = pr1
triangle-pointed-htpy :
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A} →
(f g : pointed-Π A B) (H : f ~∗ g) →
( htpy-pointed-htpy f g H (point-Pointed-Type A)) ＝
( ( preserves-point-function-pointed-Π f) ∙
( inv (preserves-point-function-pointed-Π g)))
triangle-pointed-htpy f g = pr2
```
## Properties
### Pointed homotopies are equivalent to identifications of pointed maps
```agda
module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
where
refl-htpy-pointed-map : f ~∗ f
pr1 refl-htpy-pointed-map = refl-htpy
pr2 refl-htpy-pointed-map = inv (right-inv (preserves-point-pointed-map f))
htpy-pointed-map : (g : A →∗ B) → UU (l1 ⊔ l2)
htpy-pointed-map = htpy-pointed-Π f
extensionality-pointed-map : (g : A →∗ B) → Id f g ≃ (htpy-pointed-map g)
extensionality-pointed-map = extensionality-pointed-Π f
eq-htpy-pointed-map : (g : A →∗ B) → (htpy-pointed-map g) → Id f g
eq-htpy-pointed-map g = map-inv-equiv (extensionality-pointed-map g)
```
### The category laws for pointed maps
```agda
module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
where
left-unit-law-comp-pointed-map :
htpy-pointed-map (comp-pointed-map id-pointed-map f) f
left-unit-law-comp-pointed-map =
pair
( refl-htpy)
( ( inv (right-inv (pr2 f))) ∙
( ap
( concat'
( map-pointed-map f (point-Pointed-Type A))
( inv (pr2 f)))
( ( inv (ap-id (pr2 f))) ∙
( inv right-unit))))
right-unit-law-comp-pointed-map :
htpy-pointed-map (comp-pointed-map f id-pointed-map) f
right-unit-law-comp-pointed-map =
pair
( refl-htpy)
( inv (right-inv (pr2 f)))
module _
{l1 l2 l3 l4 : Level}
where
associative-comp-pointed-map :
{A : Pointed-Type l1} {B : Pointed-Type l2}
{C : Pointed-Type l3} {D : Pointed-Type l4}
(h : C →∗ D) (g : B →∗ C) (f : A →∗ B) →
htpy-pointed-map
( comp-pointed-map (comp-pointed-map h g) f)
( comp-pointed-map h (comp-pointed-map g f))
associative-comp-pointed-map
(pair h refl) (pair g refl) (pair f refl) =
pair refl-htpy refl
inv-associative-comp-pointed-map :
{A : Pointed-Type l1} {B : Pointed-Type l2}
{C : Pointed-Type l3} {D : Pointed-Type l4}
(h : C →∗ D) (g : B →∗ C) (f : A →∗ B) →
htpy-pointed-map
( comp-pointed-map h (comp-pointed-map g f))
( comp-pointed-map (comp-pointed-map h g) f)
inv-associative-comp-pointed-map
(pair h refl) (pair g refl) (pair f refl) =
pair refl-htpy refl
```
### The groupoid laws for pointed homotopies
```agda
module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Fam l2 A}
where
concat-htpy-pointed-Π :
(f g h : pointed-Π A B) →
htpy-pointed-Π f g → htpy-pointed-Π g h → htpy-pointed-Π f h
concat-htpy-pointed-Π f g h G H =
pair
( pr1 G ∙h pr1 H)
( ( ap-binary (λ p q → p ∙ q) (pr2 G) (pr2 H)) ∙
( ( assoc (pr2 f) (inv (pr2 g)) (pr2 g ∙ inv (pr2 h))) ∙
( ap
( concat (pr2 f) (function-pointed-Π h (point-Pointed-Type A)))
( ( inv (assoc (inv (pr2 g)) (pr2 g) (inv (pr2 h)))) ∙
( ap
( concat' (point-Pointed-Fam A B) (inv (pr2 h)))
( left-inv (pr2 g)))))))
inv-htpy-pointed-Π :
(f g : pointed-Π A B) → htpy-pointed-Π f g → htpy-pointed-Π g f
inv-htpy-pointed-Π f g H =
pair
( inv-htpy (pr1 H))
( ( ap inv (pr2 H)) ∙
( ( distributive-inv-concat (pr2 f) (inv (pr2 g))) ∙
( ap
( concat'
( function-pointed-Π g (point-Pointed-Type A))
( inv (pr2 f)))
( inv-inv (pr2 g)))))
module _
{l1 l2 l3 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3}
where
left-whisker-htpy-pointed-map :
(g : B →∗ C) (f1 f2 : A →∗ B) (H : htpy-pointed-map f1 f2) →
htpy-pointed-map
( comp-pointed-map g f1)
( comp-pointed-map g f2)
left-whisker-htpy-pointed-map g f1 f2 H =
pair
( map-pointed-map g ·l (pr1 H))
( ( ( ( ap (ap (pr1 g)) (pr2 H)) ∙
( ap-concat (pr1 g) (pr2 f1) (inv (pr2 f2)))) ∙
( ap
( concat
( ap (pr1 g) (pr2 f1))
( map-pointed-map g
( map-pointed-map f2 (point-Pointed-Type A))))
( ( ( ( ap-inv (pr1 g) (pr2 f2)) ∙
( ap
( concat'
( pr1 g (point-Pointed-Fam A (constant-Pointed-Fam A B)))
( inv (ap (pr1 g) (pr2 f2)))))
( inv (right-inv (pr2 g)))) ∙
( assoc
( pr2 g)
( inv (pr2 g))
( inv (ap (pr1 g) (pr2 f2))))) ∙
( ap
( concat
( pr2 g)
( map-pointed-map g
( map-pointed-map f2 (point-Pointed-Type A))))
( inv
( distributive-inv-concat
( ap (pr1 g) (pr2 f2))
( pr2 g))))))) ∙
( inv
( assoc
( ap (pr1 g) (pr2 f1))
( pr2 g)
( inv (ap (pr1 g) (pr2 f2) ∙ pr2 g)))))
module _
{l1 l2 l3 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3}
where
right-whisker-htpy-pointed-map :
(g1 g2 : B →∗ C) (H : htpy-pointed-map g1 g2) (f : A →∗ B) →
htpy-pointed-map (comp-pointed-map g1 f) (comp-pointed-map g2 f)
right-whisker-htpy-pointed-map g1 g2 H (pair f refl) =
pair (pr1 H ·r f) (pr2 H)
module _
{l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
where
concat-htpy-pointed-map :
(f g h : A →∗ B) → htpy-pointed-map f g → htpy-pointed-map g h →
htpy-pointed-map f h
concat-htpy-pointed-map = concat-htpy-pointed-Π
```