# Transport along higher identifications

Content created by Fredrik Bakke, Egbert Rijke and Raymond Baker.

Created on 2023-09-24.

module foundation.transport-along-higher-identifications 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.function-types
open import foundation.homotopies
open import foundation.homotopy-algebra
open import foundation.path-algebra
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import foundation-core.identity-types
open import foundation-core.transport-along-identifications
open import foundation-core.whiskering-homotopies-concatenation


### The action on identifications of transport

module _
{l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y}
where

tr² : (B : A → UU l2) (α : p ＝ p') (b : B x) → (tr B p b) ＝ (tr B p' b)
tr² B α b = ap (λ t → tr B t b) α

module _
{l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y}
{α α' : p ＝ p'}
where

tr³ : (B : A → UU l2) (β : α ＝ α') (b : B x) → (tr² B α b) ＝ (tr² B α' b)
tr³ B β b = ap (λ t → tr² B t b) β

module _
{l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y}
{α α' : p ＝ p'} {γ γ' : α ＝ α'}
where

tr⁴ : (B : A → UU l2) (ψ : γ ＝ γ') → (tr³ B γ) ~ (tr³ B γ')
tr⁴ B ψ b = ap (λ t → tr³ B t b) ψ


### Computing 2-dimensional transport in a family of identifications with a fixed source

module _
{l : Level} {A : UU l} {a b c : A} {q q' : b ＝ c}
where

tr²-Id-right :
(α : q ＝ q') (p : a ＝ b) →
coherence-square-identifications
( tr-Id-right q p)
( tr² (Id a) α p)
( left-whisker-concat p α)
( tr-Id-right q' p)
tr²-Id-right α p =
inv-nat-htpy (λ (t : b ＝ c) → tr-Id-right t p) α


### Coherences and algebraic identities for tr²

#### Computing tr² along the concatenation of identifications

module _
{l1 l2 : Level} {A : UU l1} {x y : A}
{B : A → UU l2}
where

tr²-concat :
{p p' p'' : x ＝ y} (α : p ＝ p') (β : p' ＝ p'') →
tr² B (α ∙ β) ~ tr² B α ∙h tr² B β
tr²-concat α β b = ap-concat (λ t → tr B t b) α β


#### Computing tr² along the inverse of an identification

module _
{l1 l2 : Level} {A : UU l1} {x y : A}
{B : A → UU l2}
where

tr²-inv :
{p p' : x ＝ y} (α : p ＝ p') →
tr² B (inv α) ~ inv-htpy (tr² B α)
tr²-inv α b = ap-inv (λ t → tr B t b) α

left-inverse-law-tr² :
{p p' : x ＝ y} (α : p ＝ p') →
tr² B (inv α) ∙h tr² B α ~ refl-htpy
left-inverse-law-tr² α =
( right-whisker-concat-htpy (tr²-inv α) (tr² B α)) ∙h
( left-inv-htpy (tr² B α))

right-inverse-law-tr² :
{p p' : x ＝ y} (α : p ＝ p') →
tr² B α ∙h tr² B (inv α) ~ refl-htpy
right-inverse-law-tr² α =
( left-whisker-concat-htpy (tr² B α) (tr²-inv α)) ∙h
( right-inv-htpy (tr² B α))


#### Computing tr² along the unit laws for vertical concatenation of identifications

module _
{l1 l2 : Level} {A : UU l1} {x y : A}
{B : A → UU l2}
where

tr²-left-unit :
(p : x ＝ y) → tr² B left-unit ~ tr-concat refl p
tr²-left-unit p = refl-htpy

tr²-right-unit :
(p : x ＝ y) → tr² B right-unit ~ tr-concat p refl
tr²-right-unit refl = refl-htpy


#### Computing tr² along the whiskering of identification

module _
{l1 l2 : Level} {A : UU l1} {x y z : A}
{B : A → UU l2}
where

tr²-left-whisker :
(p : x ＝ y) {q q' : y ＝ z} (β : q ＝ q') →
coherence-square-homotopies
( tr-concat p q)
( tr² B (left-whisker-concat p β))
( tr² B β ·r tr B p)
( tr-concat p q')
tr²-left-whisker refl refl = refl-htpy

module _
{l1 l2 : Level} {A : UU l1} {x y z : A}
{B : A → UU l2}
where

tr²-right-whisker :
{p p' : x ＝ y} (α : p ＝ p') (q : y ＝ z) →
coherence-square-homotopies
( tr-concat p q)
( tr² B (right-whisker-concat α q))
( ( tr B q) ·l (tr² B α))
( tr-concat p' q)
tr²-right-whisker refl refl = inv-htpy right-unit-htpy


### Coherences and algebraic identities for tr³

#### Computing tr³ along the concatenation of identifications

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
{x y : A} {p p' : x ＝ y} {α α' α'' : p ＝ p'}
where

tr³-concat :
(γ : α ＝ α') (δ : α' ＝ α'') → tr³ B (γ ∙ δ) ~ (tr³ B γ) ∙h (tr³ B δ)
tr³-concat γ δ b = ap-concat (λ t → tr² B t b) γ δ


#### Computing tr³ along the horizontal concatenation of identifications

module _
{l1 l2 : Level} {A : UU l1} {x y : A} {p p' p'' : x ＝ y}
{α α' : p ＝ p'} {β β' : p' ＝ p''} {B : A → UU l2}
where

tr³-horizontal-concat :
(γ : α ＝ α') (δ : β ＝ β') →
coherence-square-homotopies
( tr²-concat α β)
( tr³ B (horizontal-concat-Id² γ δ))
( horizontal-concat-htpy² (tr³ B γ) (tr³ B δ))
( tr²-concat α' β')
tr³-horizontal-concat refl refl = inv-htpy right-unit-htpy


#### Computing tr³ along the inverse of an identification

module _
{l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y} {α α' : p ＝ p'}
{B : A → UU l2}
where

tr³-inv :
(γ : α ＝ α') →
tr³ B (inv γ) ~ inv-htpy (tr³ B γ)
tr³-inv γ b = ap-inv (λ t → tr² B t b) γ

left-inv-law-tr³ :
(γ : α ＝ α') →
tr³ B (inv γ) ∙h tr³ B γ ~ refl-htpy
left-inv-law-tr³ γ =
( right-whisker-concat-htpy (tr³-inv γ) (tr³ B γ)) ∙h
( left-inv-htpy (tr³ B γ))

right-inv-law-tr³ :
(γ : α ＝ α') →
tr³ B γ ∙h tr³ B (inv γ) ~ refl-htpy
right-inv-law-tr³ γ =
( left-whisker-concat-htpy (tr³ B γ) (tr³-inv γ)) ∙h
( right-inv-htpy (tr³ B γ))


#### Computing tr³ along the unit laws for vertical concatenation of identifications

module _
{l1 l2 : Level} {A : UU l1} {x y : A} {p q : x ＝ y}
{B : A → UU l2}
where

tr³-right-unit :
(α : p ＝ q) →
tr³ B (right-unit {p = α}) ~ tr²-concat α refl ∙h right-unit-htpy
tr³-right-unit refl = refl-htpy

tr³-left-unit :
(α : p ＝ q) →
tr³ B (left-unit {p = α}) ~ tr²-concat refl α ∙h left-unit-htpy
tr³-left-unit α = refl-htpy


#### Computing tr³ along the unit laws for whiskering of identifications

These coherences take the form of the following commutative diagrams. Note that there is an asymmetry between the left and right coherence laws due to the asymmetry in the definition of concatenation of identifications.

module _
{l1 l2 : Level} {A : UU l1} {x y : A}
{B : A → UU l2}
where

tr³-left-unit-law-left-whisker-concat :
{q q' : x ＝ y} (β : q ＝ q') →
coherence-square-homotopies
( inv-htpy right-unit-htpy)
( refl-htpy)
( tr²-left-whisker refl β)
( tr³ B (left-unit-law-left-whisker-concat β))
tr³-left-unit-law-left-whisker-concat refl = refl-htpy

module _
{l1 l2 : Level} {A : UU l1} {x y : A}
{B : A → UU l2}
where

tr³-right-unit-law-right-whisker-concat :
{p p' : x ＝ y} (α : p ＝ p') →
coherence-square-homotopies
( ( tr²-concat (right-whisker-concat α refl) right-unit) ∙h
( left-whisker-concat-htpy
( tr² B (right-whisker-concat α refl))
( tr²-right-unit p')))
( tr³ B (inv (right-unit-law-right-whisker-concat α)))
( tr²-right-whisker α refl)
( ( tr²-concat right-unit α) ∙h
( right-whisker-concat-htpy (tr²-right-unit p) (tr² B α)) ∙h
( inv-htpy
( left-whisker-concat-htpy
( tr-concat p refl)
( left-unit-law-left-whisker-comp (tr² B α)))))
tr³-right-unit-law-right-whisker-concat {p = refl} {p' = refl} refl =
refl-htpy


The above coherences have simplified forms when we consider 2-loops

module _
{l1 l2 : Level} {A : UU l1} {x : A}
{B : A → UU l2}
where

tr³-left-unit-law-left-whisker-concat-Ω² :
(β : refl {x = x} ＝ refl) →
coherence-square-homotopies
( inv-htpy right-unit-htpy)
( refl-htpy)
( tr²-left-whisker refl β)
( tr³ B (left-unit-law-left-whisker-concat β))
tr³-left-unit-law-left-whisker-concat-Ω² β =
tr³-left-unit-law-left-whisker-concat β

tr³-right-unit-law-right-whisker-concat-Ω² :
(α : refl {x = x} ＝ refl) →
coherence-square-homotopies
( inv-htpy right-unit-htpy)
( tr³ B (inv (right-unit-law-right-whisker-concat α ∙ right-unit)))
( tr²-right-whisker α refl)
( inv-htpy (left-unit-law-left-whisker-comp (tr² B α)))
tr³-right-unit-law-right-whisker-concat-Ω² α =
concat-top-homotopy-coherence-square-homotopies
( ( tr³ B (inv right-unit)) ∙h
( tr²-concat (right-whisker-concat α refl) refl))
( tr³
( B)
( inv (right-unit-law-right-whisker-concat α ∙ right-unit)))
( tr²-right-whisker α refl)
( inv-htpy (left-unit-law-left-whisker-comp (tr² B α)))
( ( right-whisker-concat-htpy
( tr³-inv right-unit)
( tr²-concat (right-whisker-concat α refl) refl)) ∙h
( inv-htpy
( left-transpose-htpy-concat
( tr³ B right-unit)
( inv-htpy right-unit-htpy)
( tr²-concat (right-whisker-concat α refl) refl)
( inv-htpy
( right-transpose-htpy-concat
( tr²-concat (right-whisker-concat α refl) refl)
( right-unit-htpy)
( tr³ B right-unit)
( inv-htpy
( tr³-right-unit (right-whisker-concat α refl))))))))
( concat-left-homotopy-coherence-square-homotopies
( ( tr³ B (inv right-unit)) ∙h
( tr²-concat (right-whisker-concat α refl) refl))
( ( tr³ B (inv right-unit)) ∙h
( tr³ B (inv (right-unit-law-right-whisker-concat α))))
( tr²-right-whisker α refl)
( inv-htpy (left-unit-law-left-whisker-comp (tr² B α)))
( ( inv-htpy
( tr³-concat
( inv right-unit)
( inv (right-unit-law-right-whisker-concat α)))) ∙h
( tr⁴
( B)
( inv
( distributive-inv-concat
( right-unit-law-right-whisker-concat α) (right-unit)))))
( left-whisker-concat-coherence-square-homotopies
( tr³ B (inv right-unit))
( tr²-concat (right-whisker-concat α refl) refl)
( tr³ B (inv (right-unit-law-right-whisker-concat α)))
( tr²-right-whisker α refl)
( inv-htpy (left-unit-law-left-whisker-comp (tr² B α)))
( concat-bottom-homotopy-coherence-square-homotopies
( tr²-concat (right-whisker-concat α refl) refl)
( tr³ B (inv (right-unit-law-right-whisker-concat α)))
( tr²-right-whisker α refl)
( inv-htpy
( left-whisker-concat-htpy
( refl-htpy)
( left-unit-law-left-whisker-comp (tr² B α))))
( ap-inv-htpy
( left-unit-law-left-whisker-concat-htpy
( left-unit-law-left-whisker-comp (tr² B α))))
( concat-top-homotopy-coherence-square-homotopies
( ( tr²-concat (right-whisker-concat α refl) refl) ∙h
( refl-htpy))
( tr³ B (inv (right-unit-law-right-whisker-concat α)))
( tr²-right-whisker α refl)
( inv-htpy
( left-whisker-concat-htpy
( refl-htpy)
( left-unit-law-left-whisker-comp (tr² B α))))
( right-unit-htpy)
( tr³-right-unit-law-right-whisker-concat α)))))


#### Computing tr³ along commutative-left-whisker-right-whisker-concat

This coherence naturally takes the form of a filler for a cube whose left face is

tr³ B (commutative-left-whisker-right-whisker-concat β α)


and whose right face is

commutative-right-whisker-left-whisker-htpy (tr² B β) (tr² B α)


However, this cube has trivial front and back faces. Thus, we only prove a simplified form of the coherence.

##### Non-trivial faces of the cube
module _
{l1 l2 : Level} {A : UU l1} {x y z : A}
{B : A → UU l2} {p p' : x ＝ y} {q q' : y ＝ z}
where

tr²-left-whisker-concat-tr²-right-whisker-concat :
(β : q ＝ q') (α : p ＝ p') →
coherence-square-homotopies
( tr-concat p q)
( ( tr² B (left-whisker-concat p β)) ∙h
( tr² B (right-whisker-concat α q')))
( (tr² B β ·r tr B p) ∙h (tr B q' ·l tr² B α))
( tr-concat p' q')
tr²-left-whisker-concat-tr²-right-whisker-concat β α =
( vertical-pasting-coherence-square-homotopies
( tr-concat p q)
( tr² B (left-whisker-concat p β))
( right-whisker-comp (tr² B β) (tr B p))
( tr-concat p q')
( tr² B (right-whisker-concat α q'))
( left-whisker-comp (tr B q') (tr² B α))
( tr-concat p' q')
( tr²-left-whisker p β)
( tr²-right-whisker α q'))

tr²-concat-left-whisker-concat-right-whisker-concat :
(β : q ＝ q') (α : p ＝ p') →
coherence-square-homotopies
( tr-concat p q)
( tr² B (left-whisker-concat p β ∙ right-whisker-concat α q'))
( (tr² B β ·r tr B p) ∙h (tr B q' ·l tr² B α))
( tr-concat p' q')
tr²-concat-left-whisker-concat-right-whisker-concat β α =
( right-whisker-concat-htpy
( tr²-concat
( left-whisker-concat p β)
( right-whisker-concat α q'))
( tr-concat p' q')) ∙h
( tr²-left-whisker-concat-tr²-right-whisker-concat β α)

tr²-right-whisker-concat-tr²-left-whisker-concat :
(α : p ＝ p') (β : q ＝ q') →
coherence-square-homotopies
( tr-concat p q)
( ( tr² B (right-whisker-concat α q)) ∙h
( tr² B (left-whisker-concat p' β)))
( (tr B q ·l tr² B α) ∙h (tr² B β ·r tr B p'))
( tr-concat p' q')
tr²-right-whisker-concat-tr²-left-whisker-concat α β =
( vertical-pasting-coherence-square-homotopies
( tr-concat p q)
( tr² B (right-whisker-concat α q))
( left-whisker-comp (tr B q) (tr² B α))
( tr-concat p' q)
( tr² B (left-whisker-concat p' β))
( right-whisker-comp (tr² B β) (tr B p'))
( tr-concat p' q')
( tr²-right-whisker α q)
( tr²-left-whisker p' β))

tr²-concat-right-whisker-concat-left-whisker-concat :
(α : p ＝ p') (β : q ＝ q') →
coherence-square-homotopies
( tr-concat p q)
( tr² B (right-whisker-concat α q ∙ left-whisker-concat p' β))
( ( tr B q ·l tr² B α) ∙h (tr² B β ·r tr B p'))
( tr-concat p' q')
tr²-concat-right-whisker-concat-left-whisker-concat α β =
( right-whisker-concat-htpy
( tr²-concat
( right-whisker-concat α q)
( left-whisker-concat p' β))
( tr-concat p' q')) ∙h
( tr²-right-whisker-concat-tr²-left-whisker-concat α β)

##### The coherence itself
module _
{l1 l2 : Level} {A : UU l1} {x y z : A}
{B : A → UU l2}
where

tr³-commutative-left-whisker-right-whisker-concat :
{q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') →
coherence-square-homotopies
( tr²-concat-left-whisker-concat-right-whisker-concat β α)
( right-whisker-concat-htpy
( tr³
( B)
( commutative-left-whisker-right-whisker-concat β α))
( tr-concat p' q'))
( left-whisker-concat-htpy
( tr-concat p q)
( commutative-right-whisker-left-whisker-htpy
( tr² B β)
( tr² B α)))
( tr²-concat-right-whisker-concat-left-whisker-concat α β)
tr³-commutative-left-whisker-right-whisker-concat
{q = refl} refl {p = refl} refl =
refl-htpy

##### A simplification of the non-trivial faces of the cube when α and β are 2-loops
module _
{l1 l2 : Level} {A : UU l1} {a : A}
{B : A → UU l2}
where

tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( ( tr² B (left-whisker-concat refl α)) ∙h
( tr² B (right-whisker-concat β refl))) ~
( tr² B α ∙h (id ·l (tr² B β)))
tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β =
horizontal-concat-htpy²
( tr³ B (left-unit-law-left-whisker-concat α))
( ( tr³
( B)
( inv (right-unit-law-right-whisker-concat β ∙ right-unit))) ∙h
( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))))

compute-tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( inv-coherence-square-homotopies-horizontal-refl
( ( tr² B (left-whisker-concat refl α)) ∙h
( tr² B (right-whisker-concat β refl)))
( tr² B α ∙h id ·l (tr² B β))
( tr²-left-whisker-concat-tr²-right-whisker-concat α β)) ~
( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β)
compute-tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β =
( vertical-pasting-inv-coherence-square-homotopies-horizontal-refl
( tr² B (left-whisker-concat refl α))
( tr² B α)
( tr² B (right-whisker-concat β refl))
( id ·l (tr² B β))
( tr²-left-whisker refl α)
( tr²-right-whisker β refl)) ∙h
( z-concat-htpy³
( inv-htpy (tr³-left-unit-law-left-whisker-concat-Ω² α))
( inv-htpy (tr³-right-unit-law-right-whisker-concat-Ω² β)))

tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( ( tr² B (right-whisker-concat α refl)) ∙h
( tr² B (left-whisker-concat refl β))) ~
( ( id ·l (tr² B α)) ∙h (tr² B β))
tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² α β =
horizontal-concat-htpy²
( ( tr³
( B)
( inv (right-unit-law-right-whisker-concat α ∙ right-unit))) ∙h
( inv-htpy (left-unit-law-left-whisker-comp (tr² B α))))
( tr³ B (left-unit-law-left-whisker-concat β))

compute-tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( inv-coherence-square-homotopies-horizontal-refl
( ( tr² B (right-whisker-concat α refl)) ∙h
( tr² B (left-whisker-concat refl β)))
( id ·l (tr² B α) ∙h tr² B β)
( tr²-right-whisker-concat-tr²-left-whisker-concat α β)) ~
( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² α β)
compute-tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² α β =
( vertical-pasting-inv-coherence-square-homotopies-horizontal-refl
( tr² B (right-whisker-concat α refl))
( id ·l (tr² B α))
( tr² B (left-whisker-concat refl β))
( tr² B β)
( tr²-right-whisker α refl)
( tr²-left-whisker refl β)) ∙h
( z-concat-htpy³
( inv-htpy (tr³-right-unit-law-right-whisker-concat-Ω² α))
( inv-htpy (tr³-left-unit-law-left-whisker-concat-Ω² β)))

tr²-concat-left-whisker-concat-right-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( tr²
( B)
( ( left-whisker-concat refl α) ∙
( right-whisker-concat β refl))) ~
( ( ( tr² B α) ·r (tr B refl)) ∙h ((tr B refl) ·l (tr² B β)))
tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β =
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl)) ∙h
( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β)

compute-tr²-concat-left-whisker-concat-right-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( ( inv-htpy right-unit-htpy) ∙h
( tr²-concat-left-whisker-concat-right-whisker-concat α β)) ~
( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β)
compute-tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β =
( inv-htpy
( assoc-htpy
( inv-htpy right-unit-htpy)
( right-whisker-concat-htpy
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl))
( refl-htpy))
( tr²-left-whisker-concat-tr²-right-whisker-concat α β))) ∙h
( right-whisker-concat-htpy
( vertical-inv-coherence-square-homotopies
( right-whisker-concat-htpy
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl))
( refl-htpy))
( right-unit-htpy)
( right-unit-htpy)
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl))
( right-unit-law-right-whisker-concat-htpy
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl))))
( tr²-left-whisker-concat-tr²-right-whisker-concat α β)) ∙h
( assoc-htpy
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl))
( inv-htpy right-unit-htpy)
( tr²-left-whisker-concat-tr²-right-whisker-concat α β)) ∙h
( left-whisker-concat-htpy
( tr²-concat
( left-whisker-concat refl α)
( right-whisker-concat β refl))
( compute-tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β))

tr²-concat-right-whisker-concat-left-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( tr²
( B)
( ( right-whisker-concat α refl) ∙
( left-whisker-concat refl β))) ~
( ( ( tr B refl) ·l (tr² B α)) ∙h ((tr² B β) ·r (tr B refl)))
tr²-concat-right-whisker-concat-left-whisker-concat-Ω² α β =
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β)) ∙h
( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² α β)

compute-tr²-concat-right-whisker-concat-left-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
( ( inv-htpy right-unit-htpy) ∙h
( tr²-concat-right-whisker-concat-left-whisker-concat α β)) ~
( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² α β)
compute-tr²-concat-right-whisker-concat-left-whisker-concat-Ω² α β =
( inv-htpy
( assoc-htpy
( inv-htpy right-unit-htpy)
( right-whisker-concat-htpy
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β))
( refl-htpy))
( tr²-right-whisker-concat-tr²-left-whisker-concat α β))) ∙h
( right-whisker-concat-htpy
( vertical-inv-coherence-square-homotopies
( right-whisker-concat-htpy
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β))
( refl-htpy))
( right-unit-htpy)
( right-unit-htpy)
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β))
( right-unit-law-right-whisker-concat-htpy
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β))))
( tr²-right-whisker-concat-tr²-left-whisker-concat α β)) ∙h
( assoc-htpy
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β))
( inv-htpy right-unit-htpy)
( tr²-right-whisker-concat-tr²-left-whisker-concat α β)) ∙h
( left-whisker-concat-htpy
( tr²-concat
( right-whisker-concat α refl)
( left-whisker-concat refl β))
( compute-tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² α β))

##### A simplification of the main coherence when α and β are 2-loops
module _
{l1 l2 : Level} {A : UU l1} {a : A}
{B : A → UU l2}
where

tr³-commutative-left-whisker-right-whisker-concat-Ω² :
(α β : refl {x = a} ＝ refl) →
coherence-square-homotopies
( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β)
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( commutative-right-whisker-left-whisker-htpy
( tr² B α)
( tr² B β))
( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α)
tr³-commutative-left-whisker-right-whisker-concat-Ω² α β =
concat-bottom-homotopy-coherence-square-homotopies
( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β)
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( commutative-right-whisker-left-whisker-htpy
( tr² B α)
( tr² B β))
( ( inv-htpy right-unit-htpy) ∙h
( tr²-concat-right-whisker-concat-left-whisker-concat β α))
( compute-tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α)
( concat-top-homotopy-coherence-square-homotopies
( ( inv-htpy right-unit-htpy) ∙h
( tr²-concat-left-whisker-concat-right-whisker-concat α β))
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( commutative-right-whisker-left-whisker-htpy
( tr² B α)
( tr² B β))
( ( inv-htpy right-unit-htpy) ∙h
( tr²-concat-right-whisker-concat-left-whisker-concat β α))
( compute-tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β)
( horizontal-pasting-coherence-square-homotopies
( inv-htpy right-unit-htpy)
( tr²-concat-left-whisker-concat-right-whisker-concat α β)
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( right-whisker-concat-htpy
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( refl-htpy))
( commutative-right-whisker-left-whisker-htpy
( tr² B α)
( tr² B β))
( inv-htpy right-unit-htpy)
( tr²-concat-right-whisker-concat-left-whisker-concat β α)
( horizontal-inv-coherence-square-homotopies
( right-unit-htpy)
( right-whisker-concat-htpy
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( refl-htpy))
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( right-unit-htpy)
( inv-htpy
( right-unit-law-right-whisker-concat-htpy
( tr³
( B)
( commutative-left-whisker-right-whisker-concat α β)))))
( concat-right-homotopy-coherence-square-homotopies
( tr²-concat-left-whisker-concat-right-whisker-concat α β)
( right-whisker-concat-htpy
( tr³ B (commutative-left-whisker-right-whisker-concat α β))
( refl-htpy))
( left-whisker-concat-htpy
( refl-htpy)
( commutative-right-whisker-left-whisker-htpy
( tr² B α)
( tr² B β)))
( tr²-concat-right-whisker-concat-left-whisker-concat β α)
( left-unit-law-left-whisker-comp
( commutative-right-whisker-left-whisker-htpy
( tr² B α)
( tr² B β)))
( tr³-commutative-left-whisker-right-whisker-concat α β))))