# Higher homotopies of morphisms of arrows

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-02-06.

module foundation.higher-homotopies-morphisms-arrows where

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-homotopies
open import foundation.commuting-squares-of-identifications
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies-morphisms-arrows
open import foundation.homotopy-induction
open import foundation.morphisms-arrows
open import foundation.path-algebra
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels
open import foundation.whiskering-higher-homotopies-composition
open import foundation.whiskering-homotopies-concatenation
open import foundation.whiskering-identifications-concatenation

open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.identity-types


## Idea

Consider two morphisms of arrows α := (i , j , H) and α' := (i' , j' , H') and two homotopies of morphisms of arrows β := (I , J , K) and β' : (I' , J' , K') between them. A 2-homotopy of morphisms of arrows is a triple (γ₀, γ₁ , γ₂) consisting of homotopies

  γ₀ : I ~ I'
γ₁ : J ~ J'


and a homotopy witnessing that the square of homotopies

                 left-whisker-concat-htpy H (g · γ₀)
H ∙ (g ·l I) ---------------------------------------> H ∙ (g · I')
|                                                     |
K |                                                     | K'
∨                                                     ∨
(J · f) ∙ H' ---------------------------------------> (J' · f) ∙ H'
right-whisker-concat-htpy (γ₁ · f) H'


## Definitions

### Homotopies of homotopies of arrows

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α α' : hom-arrow f g)
(β β' : htpy-hom-arrow f g α α')
where

coherence-htpy-htpy-hom-arrow :
htpy-domain-htpy-hom-arrow f g α α' β ~
htpy-domain-htpy-hom-arrow f g α α' β' →
htpy-codomain-htpy-hom-arrow f g α α' β ~
htpy-codomain-htpy-hom-arrow f g α α' β' → UU (l1 ⊔ l4)
coherence-htpy-htpy-hom-arrow γ₀ γ₁ =
coherence-square-homotopies
( left-whisker-concat-htpy
( coh-hom-arrow f g α)
( left-whisker-comp² g γ₀))
( coh-htpy-hom-arrow f g α α' β)
( coh-htpy-hom-arrow f g α α' β')
( right-whisker-concat-htpy
( right-whisker-comp² γ₁ f)
( coh-hom-arrow f g α'))

htpy-htpy-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
htpy-htpy-hom-arrow =
Σ ( htpy-domain-htpy-hom-arrow f g α α' β ~
htpy-domain-htpy-hom-arrow f g α α' β')
( λ γ₀ →
Σ ( htpy-codomain-htpy-hom-arrow f g α α' β ~
htpy-codomain-htpy-hom-arrow f g α α' β')
( coherence-htpy-htpy-hom-arrow γ₀))

module _
(γ : htpy-htpy-hom-arrow)
where

htpy-domain-htpy-htpy-hom-arrow :
htpy-domain-htpy-hom-arrow f g α α' β ~
htpy-domain-htpy-hom-arrow f g α α' β'
htpy-domain-htpy-htpy-hom-arrow = pr1 γ

htpy-codomain-htpy-htpy-hom-arrow :
htpy-codomain-htpy-hom-arrow f g α α' β ~
htpy-codomain-htpy-hom-arrow f g α α' β'
htpy-codomain-htpy-htpy-hom-arrow = pr1 (pr2 γ)

coh-htpy-htpy-hom-arrow :
coherence-htpy-htpy-hom-arrow
( htpy-domain-htpy-htpy-hom-arrow)
( htpy-codomain-htpy-htpy-hom-arrow)
coh-htpy-htpy-hom-arrow = pr2 (pr2 γ)


### The reflexivity homotopy of homotopies of morphisms of arrows

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α α' : hom-arrow f g)
(β : htpy-hom-arrow f g α α')
where

htpy-domain-refl-htpy-htpy-hom-arrow :
htpy-domain-htpy-hom-arrow f g α α' β ~
htpy-domain-htpy-hom-arrow f g α α' β
htpy-domain-refl-htpy-htpy-hom-arrow = refl-htpy

htpy-codomain-refl-htpy-htpy-hom-arrow :
htpy-codomain-htpy-hom-arrow f g α α' β ~
htpy-codomain-htpy-hom-arrow f g α α' β
htpy-codomain-refl-htpy-htpy-hom-arrow = refl-htpy

coh-refl-htpy-htpy-hom-arrow :
coherence-htpy-htpy-hom-arrow f g α α' β β
( htpy-domain-refl-htpy-htpy-hom-arrow)
( htpy-codomain-refl-htpy-htpy-hom-arrow)
coh-refl-htpy-htpy-hom-arrow = right-unit-htpy

refl-htpy-htpy-hom-arrow : htpy-htpy-hom-arrow f g α α' β β
pr1 refl-htpy-htpy-hom-arrow = htpy-domain-refl-htpy-htpy-hom-arrow
pr1 (pr2 refl-htpy-htpy-hom-arrow) = htpy-codomain-refl-htpy-htpy-hom-arrow
pr2 (pr2 refl-htpy-htpy-hom-arrow) = coh-refl-htpy-htpy-hom-arrow


## Properties

### Homotopies of homotopies of morphisms of arrows characterize equality of homotopies of morphisms of arrows

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α α' : hom-arrow f g)
(β : htpy-hom-arrow f g α α')
where

htpy-eq-htpy-hom-arrow :
(β' : htpy-hom-arrow f g α α') → β ＝ β' → htpy-htpy-hom-arrow f g α α' β β'
htpy-eq-htpy-hom-arrow .β refl = refl-htpy-htpy-hom-arrow f g α α' β

is-torsorial-htpy-htpy-hom-arrow :
is-torsorial (htpy-htpy-hom-arrow f g α α' β)
is-torsorial-htpy-htpy-hom-arrow =
is-torsorial-Eq-structure
( is-torsorial-htpy _)
( htpy-domain-htpy-hom-arrow f g α α' β , refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-htpy _)
( htpy-codomain-htpy-hom-arrow f g α α' β , refl-htpy)
( is-torsorial-htpy _))

is-equiv-htpy-eq-htpy-hom-arrow :
(β' : htpy-hom-arrow f g α α') → is-equiv (htpy-eq-htpy-hom-arrow β')
is-equiv-htpy-eq-htpy-hom-arrow =
fundamental-theorem-id
( is-torsorial-htpy-htpy-hom-arrow)
( htpy-eq-htpy-hom-arrow)

extensionality-htpy-hom-arrow :
(β' : htpy-hom-arrow f g α α') →
(β ＝ β') ≃ htpy-htpy-hom-arrow f g α α' β β'
pr1 (extensionality-htpy-hom-arrow β') = htpy-eq-htpy-hom-arrow β'
pr2 (extensionality-htpy-hom-arrow β') = is-equiv-htpy-eq-htpy-hom-arrow β'

eq-htpy-htpy-hom-arrow :
(β' : htpy-hom-arrow f g α α') →
htpy-htpy-hom-arrow f g α α' β β' → β ＝ β'
eq-htpy-htpy-hom-arrow β' = map-inv-equiv (extensionality-htpy-hom-arrow β')


### The left unit law for concatenation of homotopies of morphisms of arrows

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α α' : hom-arrow f g)
(β : htpy-hom-arrow f g α α')
where

htpy-domain-left-unit-law-concat-htpy-hom-arrow :
htpy-domain-concat-htpy-hom-arrow f g α α α' (refl-htpy-hom-arrow f g α) β ~
htpy-domain-htpy-hom-arrow f g α α' β
htpy-domain-left-unit-law-concat-htpy-hom-arrow = refl-htpy

htpy-codomain-left-unit-law-concat-htpy-hom-arrow :
htpy-codomain-concat-htpy-hom-arrow f g α α α'
( refl-htpy-hom-arrow f g α)
( β) ~
htpy-codomain-htpy-hom-arrow f g α α' β
htpy-codomain-left-unit-law-concat-htpy-hom-arrow = refl-htpy

coh-left-unit-law-concat-htpy-hom-arrow :
coherence-htpy-htpy-hom-arrow f g α α'
( concat-htpy-hom-arrow f g α α α' (refl-htpy-hom-arrow f g α) β)
( β)
( htpy-domain-left-unit-law-concat-htpy-hom-arrow)
( htpy-codomain-left-unit-law-concat-htpy-hom-arrow)
coh-left-unit-law-concat-htpy-hom-arrow a =
( right-unit) ∙
( right-whisker-concat
( right-whisker-concat-horizontal-refl-coherence-square-identifications
( coh-hom-arrow f g α a)
( ap g (htpy-domain-htpy-hom-arrow f g α α' β a)))
( coh-htpy-hom-arrow f g α α' β a))

left-unit-law-concat-htpy-hom-arrow :
htpy-htpy-hom-arrow f g α α'
( concat-htpy-hom-arrow f g α α α' (refl-htpy-hom-arrow f g α) β)
( β)
pr1 left-unit-law-concat-htpy-hom-arrow =
htpy-domain-left-unit-law-concat-htpy-hom-arrow
pr1 (pr2 left-unit-law-concat-htpy-hom-arrow) =
htpy-codomain-left-unit-law-concat-htpy-hom-arrow
pr2 (pr2 left-unit-law-concat-htpy-hom-arrow) =
coh-left-unit-law-concat-htpy-hom-arrow


### The right unit law for concatenation of morphisms of arrows

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (α α' : hom-arrow f g)
(β : htpy-hom-arrow f g α α')
where

htpy-domain-right-unit-law-concat-htpy-hom-arrow :
htpy-domain-concat-htpy-hom-arrow f g α α' α' β
( refl-htpy-hom-arrow f g α') ~
htpy-domain-htpy-hom-arrow f g α α' β
htpy-domain-right-unit-law-concat-htpy-hom-arrow = right-unit-htpy

htpy-codomain-right-unit-law-concat-htpy-hom-arrow :
htpy-codomain-concat-htpy-hom-arrow f g α α' α' β
( refl-htpy-hom-arrow f g α') ~
htpy-codomain-htpy-hom-arrow f g α α' β
htpy-codomain-right-unit-law-concat-htpy-hom-arrow = right-unit-htpy

coh-right-unit-law-concat-htpy-hom-arrow :
coherence-htpy-htpy-hom-arrow f g α α'
( concat-htpy-hom-arrow f g α α' α' β (refl-htpy-hom-arrow f g α'))
( β)
( htpy-domain-right-unit-law-concat-htpy-hom-arrow)
( htpy-codomain-right-unit-law-concat-htpy-hom-arrow)
coh-right-unit-law-concat-htpy-hom-arrow a =
( assoc
( left-whisker-concat (coh-hom-arrow f g α a) (ap-concat g _ refl))
( _)
( right-whisker-concat right-unit (coh-hom-arrow f g α' a))) ∙
( horizontal-concat-Id²
( ( ap
( left-whisker-concat (coh-hom-arrow f g α a))
( compute-right-refl-ap-concat g
( htpy-domain-htpy-hom-arrow f g α α' β a))) ∙
( distributive-left-whisker-concat-concat
( coh-hom-arrow f g α a)
( ap (ap g) right-unit)
( inv right-unit)))
( right-unit-law-horizontal-pasting-coherence-square-identifications
( htpy-codomain-htpy-hom-arrow f g α α' β (f a))
( coh-hom-arrow f g α a)
( coh-hom-arrow f g α' a)
( ap g (htpy-domain-htpy-hom-arrow f g α α' β a))
( coh-htpy-hom-arrow f g α α' β a)) ∙
( unsplice-concat'
( left-whisker-concat (coh-hom-arrow f g α a) (ap (ap g) right-unit))
( compute-inv-left-whisker-concat (coh-hom-arrow f g α a) right-unit)
( coh-htpy-hom-arrow f g α α' β a)))

right-unit-law-concat-htpy-hom-arrow :
htpy-htpy-hom-arrow f g α α'
( concat-htpy-hom-arrow f g α α' α' β (refl-htpy-hom-arrow f g α'))
( β)
pr1 right-unit-law-concat-htpy-hom-arrow =
htpy-domain-right-unit-law-concat-htpy-hom-arrow
pr1 (pr2 right-unit-law-concat-htpy-hom-arrow) =
htpy-codomain-right-unit-law-concat-htpy-hom-arrow
pr2 (pr2 right-unit-law-concat-htpy-hom-arrow) =
coh-right-unit-law-concat-htpy-hom-arrow