# Commuting squares of homotopies

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

Created on 2024-02-06.

module foundation-core.commuting-squares-of-homotopies where

Imports
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-squares-of-identifications
open import foundation-core.homotopies
open import foundation-core.whiskering-homotopies-concatenation


## Idea

A square of homotopies

          top
f ------> g
|         |
left |         | right
∨         ∨
h ------> i
bottom


is said to be a commuting square of homotopies if there is a homotopy left ∙h bottom ~ top ∙h right . Such a homotopy is called a coherence of the square.

## Definitions

### Commuting squares of homotopies

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
where

coherence-square-homotopies : UU (l1 ⊔ l2)
coherence-square-homotopies =
left ∙h bottom ~ top ∙h right

coherence-square-homotopies' : UU (l1 ⊔ l2)
coherence-square-homotopies' =
top ∙h right ~ left ∙h bottom


### Horizontally constant squares

Horizontally constant squares are commuting squares of homotopies of the form

       refl-htpy
f ----------> f
|             |
H |             | H
∨             ∨
g ----------> g.
refl-htpy

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} (H : f ~ g)
where

horizontal-refl-coherence-square-homotopies :
coherence-square-homotopies refl-htpy H H refl-htpy
horizontal-refl-coherence-square-homotopies x =
horizontal-refl-coherence-square-identifications (H x)


### Vertically constant squares

Vertically constant squares are commuting squares of homotopies of the form

                H
f -----> g
|        |
refl-htpy |        | refl-htpy
∨        ∨
f -----> g.
H

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} (H : f ~ g)
where

vertical-refl-coherence-square-homotopies :
coherence-square-homotopies H refl-htpy refl-htpy H
vertical-refl-coherence-square-homotopies x =
vertical-refl-coherence-square-identifications (H x)


### Squares with refl on the top and bottom

Given a homotopy H ~ H', we can obtain a coherence square with refl-htpy on the top and bottom.

       refl-htpy
f ----------> f
|             |
H |             | H'
∨             ∨
g ----------> g
refl-htpy

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x}
(H H' : f ~ g)
where

coherence-square-homotopies-horizontal-refl :
H ~ H' →
coherence-square-homotopies
( refl-htpy)
( H)
( H')
( refl-htpy)
coherence-square-homotopies-horizontal-refl K =
right-unit-htpy ∙h K


Conversely, given a coherence square as above, we can obtain a homotopy H ~ H'.

  inv-coherence-square-homotopies-horizontal-refl :
coherence-square-homotopies
( refl-htpy)
( H)
( H')
( refl-htpy) →
H ~ H'
inv-coherence-square-homotopies-horizontal-refl K =
inv-htpy-right-unit-htpy ∙h K


### Squares with refl-htpy on the left and right

Given a homotopy H ~ H', we can obtain a coherence square with refl-htpy on the left and right.

                 H'
f ------> g
|         |
refl-htpy |         | refl-htpy
∨         ∨
f ------> g
H

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x}
(H H' : f ~ g)
where

coherence-square-homotopies-vertical-refl :
H ~ H' →
coherence-square-homotopies
( H')
( refl-htpy)
( refl-htpy)
( H)
coherence-square-homotopies-vertical-refl K =
K ∙h inv-htpy right-unit-htpy


Conversely, given a coherence square as above, we can obtain a homotopy H ~ H'.

  inv-coherence-square-homotopies-vertical-refl :
coherence-square-homotopies
( H')
( refl-htpy)
( refl-htpy)
( H) →
H ~ H'
inv-coherence-square-homotopies-vertical-refl K =
K ∙h right-unit-htpy


## Operations

### Inverting squares of homotopies horizontally

Given a commuting square of homotopies

           top
f -------> g
|          |
left |          | right
∨          ∨
h -------> i,
bottom


the square of homotopies

              top⁻¹
g ------------> f
|               |
right |               | left
∨               ∨
i ------------> h
bottom⁻¹


commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

horizontal-inv-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies (inv-htpy top) right left (inv-htpy bottom)
horizontal-inv-coherence-square-homotopies top left right bottom H x =
horizontal-inv-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)


### Inverting squares of homotopies vertically

Given a commuting square of homotopies

           top
f -------> g
|          |
left |          | right
∨          ∨
h -------> i,
bottom


the square of homotopies

            bottom
h -------> i
|          |
left⁻¹ |          | right⁻¹
∨          ∨
f -------> g
top


commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

vertical-inv-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies bottom (inv-htpy left) (inv-htpy right) top
vertical-inv-coherence-square-homotopies top left right bottom H x =
vertical-inv-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)


### Functions acting on squares of homotopies

Given a commuting square of homotopies

           top
f -------> g
|          |
left |          | right
∨          ∨
h -------> i
bottom


in (x : A) → B x, and given a dependent map F : {x : A} → B x → C x, the square of homotopies

                 F ·l top
f f -----------> f g
|                |
F ·l left |                | F ·l right
∨                ∨
h -------------> i
F ·l bottom


commutes.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
{f g h i : (x : A) → B x}
(F : {x : A} → B x → C x)
where

map-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies
( F ·l top)
( F ·l left)
( F ·l right)
( F ·l bottom)
map-coherence-square-homotopies top left right bottom H x =
map-coherence-square-identifications
( F)
( top x)
( left x)
( right x)
( bottom x)
( H x)


Similarly we may whisker it on the right.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : B → UU l3}
{f g h i : (y : B) → C y}
where

right-whisker-comp-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
(F : A → B) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies
( top ·r F)
( left ·r F)
( right ·r F)
( bottom ·r F)
right-whisker-comp-coherence-square-homotopies top left right bottom F α =
α ·r F


### Concatenating homotopies of edges and coherences of commuting squares of homotopies

Consider a commuting square of homotopies and a homotopy of one of the four sides with another homotopy, as for example in the diagram below:

             top
a ---------> b
|           | |
left |     right |~| right'
∨           ∨ ∨
c ---------> d.
bottom


Then any homotopy witnessing that the square commutes can be concatenated with the homotopy on the side, to obtain a new commuting square of homotopies.

Note. To avoid cyclic module dependencies we will give direct proofs that concatenating homotopies of edges of a square with the coherence of its commutativity is an equivalence.

#### Concatenating homotopies of the top edge with a coherence of a commuting square of homotopies

Consider a commuting diagram of homotopies

           top'
------->
f -------> g
|   top    |
left |          | right
∨          ∨
h -------> i.
bottom


with a homotopy top ~ top'. Then we get maps back and forth

           top                             top'
f -------> g                    f -------> g
|          |                    |          |
left |          | right    ↔    left |          | right
∨          ∨                    ∨          ∨
h -------> i                    h -------> i.
bottom                          bottom


We record that this construction is an equivalence in foundation.commuting-squares-of-homotopies.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
{top' : f ~ g} (s : top ~ top')
where

concat-top-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left right bottom →
coherence-square-homotopies top' left right bottom
concat-top-homotopy-coherence-square-homotopies H x =
concat-top-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)

inv-concat-top-homotopy-coherence-square-homotopies :
coherence-square-homotopies top' left right bottom →
coherence-square-homotopies top left right bottom
inv-concat-top-homotopy-coherence-square-homotopies H x =
inv-concat-top-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)


#### Concatenating homotopies of the left edge with a coherence of a commuting square of homotopies

Consider a commuting diagram of homotopies

              top
f -------> g
| |         |
left' | | left    | right
∨ ∨         ∨
h -------> i.
bottom


with a homotopy left ~ left'. Then we get maps back and forth

           top                              top
f -------> g                     f -------> g
|          |                     |          |
left |          | right    ↔    left' |          | right
∨          ∨                     ∨          ∨
h -------> i                     h -------> i.
bottom                           bottom


We record that this construction is an equivalence in foundation.commuting-squares-of-homotopies.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
{left' : f ~ h} (s : left ~ left')
where

concat-left-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left right bottom →
coherence-square-homotopies top left' right bottom
concat-left-homotopy-coherence-square-homotopies H x =
concat-left-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)

inv-concat-left-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left' right bottom →
coherence-square-homotopies top left right bottom
inv-concat-left-homotopy-coherence-square-homotopies H x =
inv-concat-left-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)


#### Concatenating homotopies of the right edge with a coherence of a commuting square of homotopies

Consider a commuting diagram of homotopies

            top
f -------> g
|         | |
left |   right | | right'
∨         ∨ ∨
h -------> i.
bottom


with a homotopy right ~ right'. Then we get maps back and forth

           top                             top
f -------> g                    f -------> g
|          |                    |          |
left |          | right    ↔    left |          | right'
∨          ∨                    ∨          ∨
h -------> i                    h -------> i.
bottom                          bottom

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
{right' : g ~ i} (s : right ~ right')
where

concat-right-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left right bottom →
coherence-square-homotopies top left right' bottom
concat-right-homotopy-coherence-square-homotopies H x =
concat-right-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)

inv-concat-right-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left right' bottom →
coherence-square-homotopies top left right bottom
inv-concat-right-homotopy-coherence-square-homotopies H x =
inv-concat-right-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)


We record that this construction is an equivalence in foundation.commuting-squares-of-homotopies.

#### Concatenating homotopies of the bottom edge with a coherence of a commuting square of homotopies

Consider a commuting diagram of homotopies

            top
f -------> g
|          |
left |          | right
∨  bottom  ∨
h -------> i.
------->
bottom'


with a homotopy bottom ~ bottom'. Then we get maps back and forth

           top                             top
f -------> g                    f -------> g
|          |                    |          |
left |          | right    ↔    left |          | right
∨          ∨                    ∨          ∨
h -------> i                    h -------> i.
bottom                          bottom'

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
{bottom' : h ~ i} (s : bottom ~ bottom')
where

concat-bottom-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left right bottom →
coherence-square-homotopies top left right bottom'
concat-bottom-homotopy-coherence-square-homotopies H x =
concat-bottom-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)

inv-concat-bottom-homotopy-coherence-square-homotopies :
coherence-square-homotopies top left right bottom' →
coherence-square-homotopies top left right bottom
inv-concat-bottom-homotopy-coherence-square-homotopies H x =
inv-concat-bottom-identification-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( s x)
( H x)


We record that this construction is an equivalence in foundation.commuting-squares-of-homotopies.

### Whiskering and splicing coherences of commuting squares of homotopies with respect to concatenation of homotopies

Given a commuting square of homotopies

           top
f -------> g
|          |
left |          | right
∨          ∨
h -------> i,
bottom


we may consider four ways of attaching new homotopies to it:

1. Prepending H : u ~ f to the left gives us a commuting square

             H ∙h top
u -------> g
|          |
H ∙h left |          | right
∨          ∨
h -------> i.
bottom


More precisely, we have an equivalence

  (left ∙h bottom ~ top ∙h right) ≃ ((H ∙h left) ∙h bottom ~ (H ∙h top) ∙h right).

2. Appending a homotopy H : i ~ u to the right gives a commuting square of homotopies

                top
f ------------> g
|               |
left |               | right ∙h H
∨               ∨
h ------------> u.
bottom ∙h H


More precisely, we have an equivalence

  (left ∙h bottom ~ top ∙h right) ≃ (left ∙h (bottom ∙h H) ~ top ∙h (right ∙h H)).

3. Splicing a homotopy H : h ~ u and its inverse into the middle gives a commuting square of homotopies

                   top
f --------------> g
|                 |
left ∙h H |                 | right
∨                 ∨
u --------------> i.
H⁻¹ ∙h bottom


More precisely, we have an equivalence

  (left ∙h bottom ~ top ∙h right) ≃ ((left ∙h H) ∙h (H⁻¹ ∙h bottom) ~ top ∙h right).


Similarly, we have an equivalence

  (left ∙h bottom ~ top ∙h right) ≃ ((left ∙h H⁻¹) ∙h (H ∙h bottom) ~ top ∙h right).

4. Splicing a homotopy H : g ~ u and its inverse into the middle gives a commuting square of homotopies

         top ∙h H
f --------> u
|           |
left |           | H⁻¹ ∙h right
∨           ∨
h --------> i.
bottom


More precisely, we have an equivalence

  (left ∙h bottom ~ top ∙h right) ≃ (left ∙h bottom ~ (top ∙h H) ∙h (H⁻¹ ∙h right)).


Similarly, we have an equivalence

  (left ∙h bottom ~ top ∙h right) ≃ (left ∙h bottom ~ (top ∙h H⁻¹) ∙h (H ∙h right)).


These operations are useful in proofs involving homotopy algebra, because taking equiv-right-whisker-concat-coherence-square-homotopies as an example, it provides us with two maps: the forward direction states (H ∙h r ~ K ∙h s) → (H ∙h (r ∙h t)) ~ K ∙h (s ∙h t)), which allows one to append a homotopy without needing to reassociate on the right, and the backwards direction conversely allows one to cancel out a homotopy in parentheses.

#### Left whiskering coherences of commuting squares of homotopies

For any homotopy H : u ~ f we obtain maps back and forth

           top                                H ∙h top
f -------> g                         u -------> g
|          |                         |          |
left |          | right    ↔    H ∙h left |          | right
∨          ∨                         ∨          ∨
h -------> i                         h -------> i
bottom                               bottom


of coherences of commuting squares of homotopies. We show in foundation.commuting-squares-of-homotopies that these maps are equivalences.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

left-whisker-concat-coherence-square-homotopies :
{u : (x : A) → B x} (H : u ~ f)
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies (H ∙h top) (H ∙h left) right bottom
left-whisker-concat-coherence-square-homotopies
H top left right bottom coh x =
left-whisker-concat-coherence-square-identifications
( H x)
( top x)
( left x)
( right x)
( bottom x)
( coh x)

left-unwhisker-concat-coherence-square-homotopies :
{u : (x : A) → B x} (H : u ~ f)
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
coherence-square-homotopies (H ∙h top) (H ∙h left) right bottom →
coherence-square-homotopies top left right bottom
left-unwhisker-concat-coherence-square-homotopies
H top left right bottom coh x =
left-unwhisker-concat-coherence-square-identifications
( H x)
( top x)
( left x)
( right x)
( bottom x)
( coh x)


#### Right whiskering coherences of commuting squares of homotopies

For any homotopy H : i ~ u we obtain maps back and forth

           top                                 top
f -------> g                     f ------------> g
|          |                     |               |
left |          | right    ↔     left |               | right ∙h H
∨          ∨                     ∨               ∨
h -------> i                     h ------------> i
bottom                           bottom ∙h H


of coherences of commuting squares of homotopies. We show in foundation.commuting-squares-of-homotopies that these maps are equivalences.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
where

right-whisker-concat-coherence-square-homotopies :
coherence-square-homotopies top left right bottom →
{u : (x : A) → B x} (H : i ~ u) →
coherence-square-homotopies top left (right ∙h H) (bottom ∙h H)
right-whisker-concat-coherence-square-homotopies coh H x =
right-whisker-concat-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( coh x)
( H x)

right-unwhisker-cohernece-square-homotopies :
{u : (x : A) → B x} (H : i ~ u) →
coherence-square-homotopies top left (right ∙h H) (bottom ∙h H) →
coherence-square-homotopies top left right bottom
right-unwhisker-cohernece-square-homotopies H coh x =
right-unwhisker-cohernece-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)
( coh x)


### Double whiskering of commuting squares of homotopies

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h u v i : (x : A) → B x}
where

double-whisker-coherence-square-homotopies :
(p : f ~ g)
(top : g ~ u) (left : g ~ h) (right : u ~ v) (bottom : h ~ v)
(s : v ~ i) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies
( p ∙h top)
( p ∙h left)
( right ∙h s)
( bottom ∙h s)
double-whisker-coherence-square-homotopies p top left right bottom q H =
left-whisker-concat-coherence-square-homotopies p top left
( right ∙h q)
( bottom ∙h q)
( right-whisker-concat-coherence-square-homotopies
( top)
( left)
( right)
( bottom)
( H)
( q))


#### Left splicing coherences of commuting squares of homotopies

For any inverse pair of homotopies H : g ~ u and K : u ~ g equipped with α : inv-htpy H ~ K we obtain maps back and forth

           top                                    top
f -------> g                         f -----------> g
|          |                         |              |
left |          | right    ↔    left ∙h H |              | right
∨          ∨                         ∨              ∨
h -------> i                         u -----------> i
bottom                               K ∙h bottom


of coherences of commuting squares of homotopies. We show in foundation.commuting-squares-of-homotopies that these maps are equivalences.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
where

left-splice-coherence-square-homotopies :
{u : (x : A) → B x} (H : h ~ u) (K : u ~ h) (α : inv-htpy H ~ K) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies top (left ∙h H) right (K ∙h bottom)
left-splice-coherence-square-homotopies H K α coh x =
left-splice-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)
( K x)
( α x)
( coh x)

left-unsplice-coherence-square-homotopies :
{u : (x : A) → B x} (H : h ~ u) (K : u ~ h) (α : inv-htpy H ~ K) →
coherence-square-homotopies top (left ∙h H) right (K ∙h bottom) →
coherence-square-homotopies top left right bottom
left-unsplice-coherence-square-homotopies H K α coh x =
left-unsplice-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)
( K x)
( α x)
( coh x)


#### Right splicing coherences of commuting squares of homotopies

For any inverse pair of homotopies H : g ~ u and K : u ~ g equipped with α : inv-htpy H ~ K we obtain maps back and forth

           top                             top ∙h H
f -------> g                     f --------> u
|          |                     |           |
left |          | right    ↔     left |           | K ∙h right
∨          ∨                     ∨           ∨
h -------> i                     h --------> i
bottom                           bottom


of coherences of commuting squares of homotopies. We show in foundation.commuting-squares-of-homotopies that these maps are equivalences.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i)
where

right-splice-coherence-square-homotopies :
{u : (x : A) → B x} (H : g ~ u) (K : u ~ g) (α : inv-htpy H ~ K) →
coherence-square-homotopies top left right bottom →
coherence-square-homotopies (top ∙h H) left (inv-htpy H ∙h right) bottom
right-splice-coherence-square-homotopies H K α coh x =
right-splice-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)
( K x)
( α x)
( coh x)

right-unsplice-coherence-square-homotopies :
{u : (x : A) → B x} (H : g ~ u) (K : u ~ g) (α : inv-htpy H ~ K) →
coherence-square-homotopies (top ∙h H) left (inv-htpy H ∙h right) bottom →
coherence-square-homotopies top left right bottom
right-unsplice-coherence-square-homotopies H K α coh x =
right-unsplice-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)
( K x)
( α x)
( coh x)


### Horizontally pasting squares of homotopies

Consider two squares of homotopies as in the diagram

            top-left         top-right
a -------------> b -------------> c
|                |                |
left |                | middle         | right
∨                ∨                ∨
d -------------> e -------------> f
bottom-left      bottom-right


with H : left ∙h bottom-left ~ top-left ∙h middle and K : middle ∙h bottom-right ~ top-right ∙h right. Then the outer square commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a b c d e f : (x : A) → B x}
(top-left : a ~ b) (top-right : b ~ c)
(left : a ~ d) (middle : b ~ e) (right : c ~ f)
(bottom-left : d ~ e) (bottom-right : e ~ f)
where

horizontal-pasting-coherence-square-homotopies :
coherence-square-homotopies top-left left middle bottom-left →
coherence-square-homotopies top-right middle right bottom-right →
coherence-square-homotopies
(top-left ∙h top-right) left right (bottom-left ∙h bottom-right)
horizontal-pasting-coherence-square-homotopies H K x =
horizontal-pasting-coherence-square-identifications
( top-left x)
( top-right x)
( left x)
( middle x)
( right x)
( bottom-left x)
( bottom-right x)
( H x)
( K x)


### Vertically pasting squares of homotopies

Consider two squares of homotopies as in the diagram

                  top
a --------> b
|           |
top-left |           | top-right
∨  middle   ∨
c --------> d
|           |
bottom-left |           | bottom-right
∨           ∨
e --------> f
bottom


with H : top-left ∙h middle ~ top ∙h top-right and K : bottom-left ∙h bottom ~ middle ∙h bottom-right. Then the outer square commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a b c d e f : (x : A) → B x}
(top : a ~ b) (top-left : a ~ c) (top-right : b ~ d)
(middle : c ~ d) (bottom-left : c ~ e) (bottom-right : d ~ f)
(bottom : e ~ f)
where

vertical-pasting-coherence-square-homotopies :
coherence-square-homotopies top top-left top-right middle →
coherence-square-homotopies middle bottom-left bottom-right bottom →
coherence-square-homotopies
top (top-left ∙h bottom-left) (top-right ∙h bottom-right) bottom
vertical-pasting-coherence-square-homotopies H K x =
vertical-pasting-coherence-square-identifications
( top x)
( top-left x)
( top-right x)
( middle x)
( bottom-left x)
( bottom-right x)
( bottom x)
( H x)
( K x)


## Properties

### Left unit law for horizontal pasting of commuting squares of homotopies

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

left-unit-law-horizontal-pasting-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
(H : coherence-square-homotopies top left right bottom) →
horizontal-pasting-coherence-square-homotopies
( refl-htpy)
( top)
( left)
( left)
( right)
( refl-htpy)
( bottom)
( horizontal-refl-coherence-square-homotopies left)
( H) ~
H
left-unit-law-horizontal-pasting-coherence-square-homotopies
top left right bottom H x =
left-unit-law-horizontal-pasting-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)


### Right unit law for horizontal pasting of commuting squares of homotopies

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

right-unit-law-horizontal-pasting-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
(H : coherence-square-homotopies top left right bottom) →
horizontal-pasting-coherence-square-homotopies
( top)
( refl-htpy)
( left)
( right)
( right)
( bottom)
( refl-htpy)
( H)
( horizontal-refl-coherence-square-homotopies right) ∙h
right-whisker-concat-htpy right-unit-htpy right ~
left-whisker-concat-htpy left right-unit-htpy ∙h H
right-unit-law-horizontal-pasting-coherence-square-homotopies
top left right bottom H x =
right-unit-law-horizontal-pasting-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)


### Left unit law for vertical pasting of commuting squares of homotopies

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

left-unit-law-vertical-pasting-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
(H : coherence-square-homotopies top left right bottom) →
vertical-pasting-coherence-square-homotopies
( top)
( refl-htpy)
( refl-htpy)
( top)
( left)
( right)
( bottom)
( vertical-refl-coherence-square-homotopies top)
( H) ~
H
left-unit-law-vertical-pasting-coherence-square-homotopies
top left right bottom H x =
left-unit-law-vertical-pasting-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)


### Right unit law for vertical pasting of commuting squares of homotopies

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h i : (x : A) → B x}
where

right-unit-law-vertical-pasting-coherence-square-homotopies :
(top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) →
(H : coherence-square-homotopies top left right bottom) →
vertical-pasting-coherence-square-homotopies
( top)
( left)
( right)
( bottom)
( refl-htpy)
( refl-htpy)
( bottom)
( H)
( vertical-refl-coherence-square-homotopies bottom) ∙h
left-whisker-concat-htpy top right-unit-htpy ~
right-whisker-concat-htpy right-unit-htpy bottom ∙h H
right-unit-law-vertical-pasting-coherence-square-homotopies
top left right bottom H x =
right-unit-law-vertical-pasting-coherence-square-identifications
( top x)
( left x)
( right x)
( bottom x)
( H x)


### Computing the right whiskering of a vertically constant square with a homotopy

Consider the vertically constant square of homotopies

           H
f -----> g
|        |
refl |        | refl
∨        ∨
f -----> g
H


at a homotopy H : f ~ g, and consider a homotopy K : g ~ h. Then the right whiskering of the above square with K is the commuting square of homotopies

            H
f -------> g
|          |
refl |   refl   | K
∨          ∨
f -------> h
H ∙h K

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
where

right-whisker-concat-vertical-refl-coherence-square-homotopies :
(H : f ~ g) (K : g ~ h) →
right-whisker-concat-coherence-square-homotopies H refl-htpy refl-htpy H
( vertical-refl-coherence-square-homotopies H)
( K) ~
refl-htpy
right-whisker-concat-vertical-refl-coherence-square-homotopies H K x =
right-whisker-concat-vertical-refl-coherence-square-identifications
( H x)
( K x)


### Computing the right whiskering of a horizontally constant square with a homotopy

Consider a horizontally constant commuting square of homotopies

       refl-htpy
f ----------> f
|             |
H |             | H
∨             ∨
g ----------> g
refl-htpy


at a homotopy H and consider a homotopy K : g ~ h. Then the right whiskering of the above square with K is the square

       refl-htpy
f ----------> f
|             |
H |  refl-htpy  | H ∙h K
∨             ∨
g ----------> h.
K

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
where

right-whisker-concat-horizontal-refl-coherence-square-homotopies :
(H : f ~ g) (K : g ~ h) →
right-whisker-concat-coherence-square-homotopies refl-htpy H H refl-htpy
( horizontal-refl-coherence-square-homotopies H)
( K) ~
refl-htpy
right-whisker-concat-horizontal-refl-coherence-square-homotopies H K x =
right-whisker-concat-horizontal-refl-coherence-square-identifications
( H x)
( K x)


### Computing the left whiskering of a horizontally constant square with a homotopy

Consider a homotopy H : f ~ g and a horizontally constant commuting square of homotopies

       refl-htpy
g ----------> g
|             |
K |             | K
∨             ∨
h ----------> h
refl-htpy


at a homotopy K : g ~ h. The the left whiskering of the above square with H is the commuting square

                                    K ∙h refl-htpy
f -----------------------------------------------------------------> g
|                                                                    |
K ∙h H | right-unit-htpy ∙h (right-whisker-concat-htpy right-unit-htpy H)⁻¹ | H
∨                                                                    ∨
h -----------------------------------------------------------------> h.
refl-htpy

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
where

left-whisker-concat-horizontal-refl-coherence-square-homotopies :
(H : f ~ g) (K : g ~ h) →
left-whisker-concat-coherence-square-homotopies H refl-htpy K K refl-htpy
( horizontal-refl-coherence-square-homotopies K) ∙h
right-whisker-concat-htpy right-unit-htpy K ~
right-unit-htpy
left-whisker-concat-horizontal-refl-coherence-square-homotopies H K x =
left-whisker-concat-horizontal-refl-coherence-square-identifications
( H x)
( K x)

left-whisker-concat-horizontal-refl-coherence-square-homotopies' :
(H : f ~ g) (K : g ~ h) →
left-whisker-concat-coherence-square-homotopies H refl-htpy K K refl-htpy
( horizontal-refl-coherence-square-homotopies K) ~
right-unit-htpy ∙h inv-htpy (right-whisker-concat-htpy right-unit-htpy K)
left-whisker-concat-horizontal-refl-coherence-square-homotopies' H K x =
left-whisker-concat-horizontal-refl-coherence-square-identifications'
( H x)
( K x)


### Computing the left whiskering of a vertically constant square with a homotopy

Consider the vertically constant square of homotopies

                K
g -----> h
|        |
refl-htpy |        | refl-htpy
∨        ∨
g -----> h
K


at a homotopy K : g ~ h and consider a homotopy H : f ~ g. Then the left whiskering of the above square with H is the square

                                            H ∙h K
f ----------------------------------------------------------> h
|                                                             |
H ∙h refl-htpy | right-whisker-concat-htpy right-unit-htpy K ∙h right-unit⁻¹ | refl-htpy
∨                                                             ∨
g ----------------------------------------------------------> h.
K

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x}
where

left-whisker-concat-vertical-refl-coherence-square-homotopies :
(H : f ~ g) (K : g ~ h) →
left-whisker-concat-coherence-square-homotopies H K refl-htpy refl-htpy K
( vertical-refl-coherence-square-homotopies K) ∙h
right-unit-htpy ~
right-whisker-concat-htpy right-unit-htpy K
left-whisker-concat-vertical-refl-coherence-square-homotopies H K x =
left-whisker-concat-vertical-refl-coherence-square-identifications
( H x)
( K x)

left-whisker-concat-vertical-refl-coherence-square-homotopies' :
(H : f ~ g) (K : g ~ h) →
left-whisker-concat-coherence-square-homotopies H K refl-htpy refl-htpy K
( vertical-refl-coherence-square-homotopies K) ~
right-whisker-concat-htpy right-unit-htpy K ∙h inv-htpy right-unit-htpy
left-whisker-concat-vertical-refl-coherence-square-homotopies' H K x =
left-whisker-concat-vertical-refl-coherence-square-identifications'
( H x)
( K x)


### Left whiskering horizontal concatenations of squares with homotopies

Consider a commuting diagram of homotopies of the form

            top-left        top-right
a -------------> c -------------> e
|                |                |
left |                | middle         | right
∨                ∨                ∨
b -------------> d -------------> f
bottom-left      bottom-right


and consider a homotopy H : f ~ a. Then the left whiskering of H and the horizontal concatenation of coherences of commuting squares is up to associativity the horizontal concatenation of the squares

               H ∙h top-left      top-right
u -------------> c -------------> e
|                |                |
H ∙h left |                | middle         | right
∨                ∨                ∨
b -------------> d -------------> f
bottom-left      bottom-right


where the left square is the left whiskering of H and the original left square.

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

left-whisker-concat-horizontal-pasting-coherence-square-homotopies :
{u a b c d e f : (x : A) → B x} (H : u ~ a)
(top-left : a ~ c) (top-right : c ~ e)
(left : a ~ b) (middle : c ~ d) (right : e ~ f)
(bottom-left : b ~ d) (bottom-right : d ~ f)
(l : coherence-square-homotopies top-left left middle bottom-left)
(r : coherence-square-homotopies top-right middle right bottom-right) →
left-whisker-concat-coherence-square-homotopies H
( top-left ∙h top-right)
( left)
( right)
( bottom-left ∙h bottom-right)
( horizontal-pasting-coherence-square-homotopies
( top-left)
( top-right)
( left)
( middle)
( right)
( bottom-left)
( bottom-right)
( l)
( r)) ~
horizontal-pasting-coherence-square-homotopies
( H ∙h top-left)
( top-right)
( H ∙h left)
( middle)
( right)
( bottom-left)
( bottom-right)
( left-whisker-concat-coherence-square-homotopies H
( top-left)
( left)
( middle)
( bottom-left)
( l))
( r) ∙h
right-whisker-concat-htpy
( assoc-htpy H top-left top-right)
( right)
left-whisker-concat-horizontal-pasting-coherence-square-homotopies
H top-left top-right left middle right bottom-left bottom-right l r x =
left-whisker-concat-horizontal-pasting-coherence-square-identifications
( H x)
( top-left x)
( top-right x)
( left x)
( middle x)
( right x)
( bottom-left x)
( bottom-right x)
( l x)
( r x)


### Left whiskering vertical concatenations of squares with homotopies

Consider two squares of homotopies as in the diagram

                  top
a --------> b
|           |
top-left |           | top-right
∨  middle   ∨
c --------> d
|           |
bottom-left |           | bottom-right
∨           ∨
e --------> f
bottom


and consider a homotopy H : f ~ a. Then the left whiskering of H with the vertical pasting of the two squares above is up to associativity the vertical pasting of the squares

                  H ∙h top
u --------> b
|           |
H ∙h top-left |           | top-right
∨  middle   ∨
c --------> d
|           |
bottom-left |           | bottom-right
∨           ∨
e --------> f.
bottom

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

left-whisker-concat-vertical-concat-coherence-square-homotopies :
{u a b c d e f : (x : A) → B x} (H : u ~ a) →
(top : a ~ b) (top-left : a ~ c) (top-right : b ~ d) (middle : c ~ d)
(bottom-left : c ~ e) (bottom-right : d ~ f) (bottom : e ~ f)
(t : coherence-square-homotopies top top-left top-right middle) →
(b :
coherence-square-homotopies middle bottom-left bottom-right bottom) →
right-whisker-concat-htpy (assoc-htpy H top-left bottom-left) bottom ∙h
left-whisker-concat-coherence-square-homotopies H
( top)
( top-left ∙h bottom-left)
( top-right ∙h bottom-right)
( bottom)
( vertical-pasting-coherence-square-homotopies
( top)
( top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( t)
( b)) ~
vertical-pasting-coherence-square-homotopies
( H ∙h top)
( H ∙h top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( left-whisker-concat-coherence-square-homotopies H
( top)
( top-left)
( top-right)
( middle)
( t))
( b)
left-whisker-concat-vertical-concat-coherence-square-homotopies
H top top-left top-right middle bottom-left bottom-right bottom t b x =
left-whisker-concat-vertical-concat-coherence-square-identifications
( H x)
( top x)
( top-left x)
( top-right x)
( middle x)
( bottom-left x)
( bottom-right x)
( bottom x)
( t x)
( b x)


### Right whiskering horizontal pastings of commuting squares of homotopies

Consider a commuting diagram of homotopies of the form

            top-left        top-right
a -------------> c -------------> e
|                |                |
left |                | middle         | right
∨                ∨                ∨
b -------------> d -------------> f
bottom-left      bottom-right


and consider a homotopy K : f ~ g. Then the right whiskering of the horizontal pasting of the squares above is up to associativity the horizontal pasting of the squares

            top-left           top-right
a -------------> c ------------------> e
|                |                     |
left |                | middle              | right ∙h K
∨                ∨                     ∨
b -------------> d ------------------> g
bottom-left      bottom-right ∙h K

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

right-whisker-concat-horizontal-pasting-coherence-square-homotopies :
{a b c d e f g : (x : A) → B x}
(top-left : a ~ c) (top-right : c ~ e)
(left : a ~ b) (middle : c ~ d) (right : e ~ f)
(bottom-left : b ~ d) (bottom-right : d ~ f)
(l : coherence-square-homotopies top-left left middle bottom-left) →
(r : coherence-square-homotopies top-right middle right bottom-right) →
(K : f ~ g) →
right-whisker-concat-coherence-square-homotopies
( top-left ∙h top-right)
( left)
( right)
( bottom-left ∙h bottom-right)
( horizontal-pasting-coherence-square-homotopies
( top-left)
( top-right)
( left)
( middle)
( right)
( bottom-left)
( bottom-right)
( l)
( r))
( K) ~
left-whisker-concat-htpy left (assoc-htpy bottom-left bottom-right K) ∙h
horizontal-pasting-coherence-square-homotopies
( top-left)
( top-right)
( left)
( middle)
( right ∙h K)
( bottom-left)
( bottom-right ∙h K)
( l)
( right-whisker-concat-coherence-square-homotopies
( top-right)
( middle)
( right)
( bottom-right)
( r)
( K))
right-whisker-concat-horizontal-pasting-coherence-square-homotopies
top-left top-right left middle right bottom-left bottom-right l r K x =
right-whisker-concat-horizontal-pasting-coherence-square-identifications
( top-left x)
( top-right x)
( left x)
( middle x)
( right x)
( bottom-left x)
( bottom-right x)
( l x)
( r x)
( K x)


### Right whiskering vertical concatenations of squares with homotopies

Consider two squares of homotopies as in the diagram

                  top
a --------> b
|           |
top-left |           | top-right
∨  middle   ∨
c --------> d
|           |
bottom-left |           | bottom-right
∨           ∨
e --------> f
bottom


and consider a homotopy K : f ~ g. Then the right whiskering of the vertical pasting of the two squares above with K is up to associativity the vertical pasting of the squares

                     top
a ------------> b
|               |
top-left |               | top-right
∨    middle     ∨
c ------------> d
|               |
bottom-left |               | bottom-right ∙h K
∨               ∨
e ------------> g.
bottom ∙h K

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

right-whisker-concat-vertical-pasting-coherence-square-homotopies :
{a b c d e f g : (x : A) → B x}
(top : a ~ b) (top-left : a ~ c) (top-right : b ~ d)
(middle : c ~ d)
(bottom-left : c ~ e) (bottom-right : d ~ f) (bottom : e ~ f)
(t : coherence-square-homotopies top top-left top-right middle) →
(b :
coherence-square-homotopies middle bottom-left bottom-right bottom) →
(K : f ~ g) →
right-whisker-concat-coherence-square-homotopies
( top)
( top-left ∙h bottom-left)
( top-right ∙h bottom-right)
( bottom)
( vertical-pasting-coherence-square-homotopies
( top)
( top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( t)
( b))
( K) ∙h
left-whisker-concat-htpy top (assoc-htpy top-right bottom-right K) ~
vertical-pasting-coherence-square-homotopies
( top)
( top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right ∙h K)
( bottom ∙h K)
( t)
( right-whisker-concat-coherence-square-homotopies
( middle)
( bottom-left)
( bottom-right)
( bottom)
( b)
( K))
right-whisker-concat-vertical-pasting-coherence-square-homotopies
top top-left top-right middle bottom-left bottom-right bottom t b K x =
right-whisker-concat-vertical-pasting-coherence-square-identifications
( top x)
( top-left x)
( top-right x)
( middle x)
( bottom-left x)
( bottom-right x)
( bottom x)
( t x)
( b x)
( K x)