# Commuting squares of identifications

Content created by Fredrik Bakke and Raymond Baker.

Created on 2024-02-19.

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

Imports
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.whiskering-identifications-concatenation


## Idea

A square of identifications

           top
x -------> y
|          |
left |          | right
∨          ∨
z -------> w
bottom


is said to be a commuting square if there is an identification left ∙ bottom ＝ top ∙ right. Such an identification is called a coherence of the square.

## Definitions

### Commuting squares of identifications

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
where

coherence-square-identifications : UU l
coherence-square-identifications = left ∙ bottom ＝ top ∙ right


### Horizontally constant squares

Horizontally constant squares are commuting squares of identifications of the form

       refl
a -----> a
|        |
p |        | p
∨        ∨
b -----> b.
refl

module _
{l : Level} {A : UU l} {a b : A} (p : a ＝ b)
where

horizontal-refl-coherence-square-identifications :
coherence-square-identifications refl p p refl
horizontal-refl-coherence-square-identifications = right-unit


### Vertically constant squares

Vertically constant squares are commuting squares of identifications of the form

           p
a -----> b
|        |
refl |        | refl
∨        ∨
a -----> b.
p

module _
{l : Level} {A : UU l} {a b : A} (p : a ＝ b)
where

vertical-refl-coherence-square-identifications :
coherence-square-identifications p refl refl p
vertical-refl-coherence-square-identifications = inv right-unit


### Squares with refl on the top and bottom

Given an identification α : p ＝ q, we can obtain a coherence square with refl on the top and bottom, like the diagram below.

       refl
a -----> a
|        |
p |        | q
∨        ∨
b -----> b
refl

module _
{l : Level} {A : UU l} {a b : A} (p q : a ＝ b)
where

coherence-square-identifications-horizontal-refl :
p ＝ q →
coherence-square-identifications
( refl)
( p)
( q)
( refl)
coherence-square-identifications-horizontal-refl α =
right-unit ∙ α


Conversely, given a coherence square as above, we can obtain an equality p ＝ q.

  inv-coherence-square-identifications-horizontal-refl :
coherence-square-identifications
( refl)
( p)
( q)
( refl) →
p ＝ q
inv-coherence-square-identifications-horizontal-refl α =
inv right-unit ∙ α


### Squares with refl on the left and right

Given an identification α : p ＝ q, we can obtain a coherence square with refl on the left and right, like the diagram below.

           q
a -----> b
|        |
refl |        | refl
∨        ∨
a -----> b
p

  coherence-square-identifications-vertical-refl :
p ＝ q →
coherence-square-identifications
( q)
( refl)
( refl)
( p)
coherence-square-identifications-vertical-refl α =
α ∙ inv right-unit


Conversely, given a coherence square as above, we can obtain an equality  p ＝ q.

  inv-coherence-square-identifications-vertical-refl :
coherence-square-identifications
( q)
( refl)
( refl)
( p) →
p ＝ q
inv-coherence-square-identifications-vertical-refl α =
α ∙ right-unit


## Operations

### Inverting squares of identifications horizontally

Given a commuting square of identifications

           top
x -------> y
|          |
left |          | right
∨          ∨
z -------> w,
bottom


the square of identifications

             inv top
y ------------> x
|               |
right |               | left
∨               ∨
w ------------> z
inv bottom


commutes.

module _
{l : Level} {A : UU l} {x y z w : A}
where

horizontal-inv-coherence-square-identifications :
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) →
coherence-square-identifications top left right bottom →
coherence-square-identifications (inv top) right left (inv bottom)
horizontal-inv-coherence-square-identifications refl left right bottom coh =
inv (right-transpose-eq-concat left bottom right coh)


### Inverting squares of identifications vertically

Given a commuting square of identifications

           top
x -------> y
|          |
left |          | right
∨          ∨
z -------> w,
bottom


the square of identifications

              bottom
z -------> w
|          |
inv left |          | inv right
∨          ∨
x -------> y
top


commutes.

module _
{l : Level} {A : UU l} {x y z w : A}
where

vertical-inv-coherence-square-identifications :
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) →
coherence-square-identifications top left right bottom →
coherence-square-identifications bottom (inv left) (inv right) top
vertical-inv-coherence-square-identifications top refl right bottom coh =
right-transpose-eq-concat top right (bottom) (inv coh)


### Functions acting on squares of identifications

Given a commuting square of identifications

           top
x -------> y
|          |
left |          | right
∨          ∨
z -------> w
bottom


in a type A, and given a map f : A → B, the square of identifications

                 ap f top
f x -----------> f y
|                |
ap f left |                | ap f right
∨                ∨
z -------------> w
ap f bottom


commutes.

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

map-coherence-square-identifications :
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) →
coherence-square-identifications top left right bottom →
coherence-square-identifications
( ap f top)
( ap f left)
( ap f right)
( ap f bottom)
map-coherence-square-identifications refl refl _ _ coh = ap (ap f) coh


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

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

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


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

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

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

Consider a commuting diagram of identifications

           top'
------->
x -------> y
|   top    |
left |          | right
∨          ∨
z -------> w.
bottom


with an identification top ＝ top'. Then we get an equivalence

           top                             top'
x -------> y                    x -------> y
|          |                    |          |
left |          | right    ≃    left |          | right
∨          ∨                    ∨          ∨
z -------> w                    z -------> w.
bottom                          bottom

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
{top' : x ＝ y} (s : top ＝ top')
where

concat-top-identification-coherence-square-identifications :
coherence-square-identifications top left right bottom →
coherence-square-identifications top' left right bottom
concat-top-identification-coherence-square-identifications t =
t ∙ ap (concat' _ right) s

inv-concat-top-identification-coherence-square-identifications :
coherence-square-identifications top' left right bottom →
coherence-square-identifications top left right bottom
inv-concat-top-identification-coherence-square-identifications t =
t ∙ inv (ap (concat' _ right) s)

is-section-inv-concat-top-identification-coherence-square-identifications :
is-section
concat-top-identification-coherence-square-identifications
inv-concat-top-identification-coherence-square-identifications
is-section-inv-concat-top-identification-coherence-square-identifications =
is-section-inv-concat' (ap (concat' _ right) s)

is-retraction-inv-concat-top-identification-coherence-square-identifications :
is-retraction
concat-top-identification-coherence-square-identifications
inv-concat-top-identification-coherence-square-identifications
is-retraction-inv-concat-top-identification-coherence-square-identifications =
is-retraction-inv-concat' (ap (concat' _ right) s)


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

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

Consider a commuting diagram of identifications

              top
x -------> y
| |         |
left' | | left    | right
∨ ∨         ∨
z -------> w.
bottom


with an identification left ＝ left'. Then we get an equivalence

           top                              top
x -------> y                     x -------> y
|          |                     |          |
left |          | right    ≃    left' |          | right
∨          ∨                     ∨          ∨
z -------> w                     z -------> w.
bottom                           bottom

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
{left' : x ＝ z} (s : left ＝ left')
where

concat-left-identification-coherence-square-identifications :
coherence-square-identifications top left right bottom →
coherence-square-identifications top left' right bottom
concat-left-identification-coherence-square-identifications t =
inv (ap (concat' _ bottom) s) ∙ t

inv-concat-left-identification-coherence-square-identifications :
coherence-square-identifications top left' right bottom →
coherence-square-identifications top left right bottom
inv-concat-left-identification-coherence-square-identifications t =
ap (concat' _ bottom) s ∙ t

is-section-inv-concat-left-identification-coherence-square-identifications :
is-section
concat-left-identification-coherence-square-identifications
inv-concat-left-identification-coherence-square-identifications
is-section-inv-concat-left-identification-coherence-square-identifications =
is-retraction-inv-concat (ap (concat' _ bottom) s)

is-retraction-inv-concat-left-identification-coherence-square-identifications :
is-retraction
concat-left-identification-coherence-square-identifications
inv-concat-left-identification-coherence-square-identifications
is-retraction-inv-concat-left-identification-coherence-square-identifications =
is-section-inv-concat (ap (concat' _ bottom) s)


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

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

Consider a commuting diagram of identifications

            top
x -------> y
|         | |
left |   right | | right'
∨         ∨ ∨
z -------> w.
bottom


with an identification right ＝ right'. Then we get an equivalence

           top                             top
x -------> y                    x -------> y
|          |                    |          |
left |          | right    ≃    left |          | right'
∨          ∨                    ∨          ∨
z -------> w                    z -------> w.
bottom                          bottom

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
{right' : y ＝ w} (s : right ＝ right')
where

concat-right-identification-coherence-square-identifications :
coherence-square-identifications top left right bottom →
coherence-square-identifications top left right' bottom
concat-right-identification-coherence-square-identifications t =
t ∙ ap (concat top _) s

inv-concat-right-identification-coherence-square-identifications :
coherence-square-identifications top left right' bottom →
coherence-square-identifications top left right bottom
inv-concat-right-identification-coherence-square-identifications t =
t ∙ inv (ap (concat top _) s)

is-section-inv-concat-right-identification-coherence-square-identifications :
is-section
concat-right-identification-coherence-square-identifications
inv-concat-right-identification-coherence-square-identifications
is-section-inv-concat-right-identification-coherence-square-identifications =
is-section-inv-concat' (ap (concat top _) s)

is-retraction-inv-concat-right-identification-coherence-square-identifications :
is-retraction
concat-right-identification-coherence-square-identifications
inv-concat-right-identification-coherence-square-identifications
is-retraction-inv-concat-right-identification-coherence-square-identifications =
is-retraction-inv-concat' (ap (concat top _) s)


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

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

Consider a commuting diagram of identifications

            top
x -------> y
|          |
left |          | right
∨  bottom  ∨
z -------> w.
------->
bottom'


with an identification bottom ＝ bottom'. Then we get an equivalence

           top                             top
x -------> y                    x -------> y
|          |                    |          |
left |          | right    ≃    left |          | right
∨          ∨                    ∨          ∨
z -------> w                    z -------> w.
bottom                          bottom'

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
{bottom' : z ＝ w} (s : bottom ＝ bottom')
where

concat-bottom-identification-coherence-square-identifications :
coherence-square-identifications top left right bottom →
coherence-square-identifications top left right bottom'
concat-bottom-identification-coherence-square-identifications t =
inv (ap (concat left _) s) ∙ t

inv-concat-bottom-identification-coherence-square-identifications :
coherence-square-identifications top left right bottom' →
coherence-square-identifications top left right bottom
inv-concat-bottom-identification-coherence-square-identifications t =
ap (concat left _) s ∙ t

is-section-inv-concat-bottom-identification-coherence-square-identifications :
is-section
concat-bottom-identification-coherence-square-identifications
inv-concat-bottom-identification-coherence-square-identifications
is-section-inv-concat-bottom-identification-coherence-square-identifications =
is-retraction-inv-concat (ap (concat left _) s)

is-retraction-inv-concat-bottom-identification-coherence-square-identifications :
is-retraction
concat-bottom-identification-coherence-square-identifications
inv-concat-bottom-identification-coherence-square-identifications
is-retraction-inv-concat-bottom-identification-coherence-square-identifications =
is-section-inv-concat (ap (concat left _) s)


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

### Whiskering and splicing coherences of commuting squares of identifications

Given a commuting square of identifications

           top
x -------> y
|          |
left |          | right
∨          ∨
z -------> w,
bottom


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

1. Prepending p : u ＝ x to the left gives us a commuting square

             p ∙ top
u -------> y
|          |
p ∙ left |          | right
∨          ∨
z -------> w.
bottom


More precisely, we have an equivalence

  (left ∙ bottom ＝ top ∙ right) ≃ ((p ∙ left) ∙ bottom ＝ (p ∙ top) ∙ right).

2. Appending an identification p : w ＝ u to the right gives a commuting square of identifications

                top
x ------------> y
|               |
left |               | right ∙ p
∨               ∨
z ------------> u.
bottom ∙ p


More precisely, we have an equivalence

  (left ∙ bottom ＝ top ∙ right) ≃ (left ∙ (bottom ∙ p) ＝ top ∙ (right ∙ p)).

3. Splicing an identification p : z ＝ u and its inverse into the middle gives a commuting square of identifications

                   top
x --------------> y
|                 |
left ∙ p |                 | right
∨                 ∨
u --------------> w.
p⁻¹ ∙ bottom


More precisely, we have an equivalence

  (left ∙ bottom ＝ top ∙ right) ≃ ((left ∙ p) ∙ (p⁻¹ ∙ bottom) ＝ top ∙ right).


Similarly, we have an equivalence

  (left ∙ bottom ＝ top ∙ right) ≃ ((left ∙ p⁻¹) ∙ (p ∙ bottom) ＝ top ∙ right).

4. Splicing an identification p : y ＝ u and its inverse into the middle gives a commuting square of identifications

          top ∙ p
x --------> u
|           |
left |           | p⁻¹ ∙ right
∨           ∨
z --------> w.
bottom


More precisely, we have an equivalence

  (left ∙ bottom ＝ top ∙ right) ≃ (left ∙ bottom ＝ (top ∙ p) ∙ (p⁻¹ ∙ right)).


Similarly, we have an equivalence

  (left ∙ bottom ＝ top ∙ right) ≃ (left ∙ bottom ＝ (top ∙ p⁻¹) ∙ (p ∙ right)).


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

#### Left whiskering coherences of commuting squares of identifications

For any identification p : u ＝ x we obtain an equivalence

           top                                p ∙ top
x -------> y                         u -------> y
|          |                         |          |
left |          | right    ≃     p ∙ left |          | right
∨          ∨                         ∨          ∨
z -------> w                         z -------> w
bottom                               bottom


of coherences of commuting squares of identifications.

module _
{l : Level} {A : UU l} {x y z w u : A}
where

left-whisker-concat-coherence-square-identifications :
(p : u ＝ x)
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) →
coherence-square-identifications top left right bottom →
coherence-square-identifications (p ∙ top) (p ∙ left) right bottom
left-whisker-concat-coherence-square-identifications
refl top left right bottom =
id

left-unwhisker-concat-coherence-square-identifications :
(p : u ＝ x)
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) →
coherence-square-identifications (p ∙ top) (p ∙ left) right bottom →
coherence-square-identifications top left right bottom
left-unwhisker-concat-coherence-square-identifications
refl top left right bottom =
id


#### Right whiskering coherences of commuting squares of identifications

For any identification p : w ＝ u we obtain an equivalence

           top                                 top
x -------> y                     x ------------> y
|          |                     |               |
left |          | right    ≃     left |               | right ∙ p
∨          ∨                     ∨               ∨
z -------> w                     z ------------> w
bottom                           bottom ∙ p


of coherences of commuting squares of identifications.

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
where

right-whisker-concat-coherence-square-identifications :
coherence-square-identifications top left right bottom →
{u : A} (p : w ＝ u) →
coherence-square-identifications top left (right ∙ p) (bottom ∙ p)
right-whisker-concat-coherence-square-identifications s refl =
concat-bottom-identification-coherence-square-identifications
( top)
( left)
( right ∙ refl)
( bottom)
( inv right-unit)
( concat-right-identification-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( inv right-unit)
( s))

right-unwhisker-cohernece-square-identifications :
{u : A} (p : w ＝ u) →
coherence-square-identifications top left (right ∙ p) (bottom ∙ p) →
coherence-square-identifications top left right bottom
right-unwhisker-cohernece-square-identifications refl =
( inv-concat-right-identification-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( inv right-unit)) ∘
( inv-concat-bottom-identification-coherence-square-identifications
( top)
( left)
( right ∙ refl)
( bottom)
( inv right-unit))


### Double whiskering of commuting squares of identifications

module _
{l : Level} {A : UU l} {x y z u v w : A}
where

double-whisker-coherence-square-identifications :
(p : x ＝ y)
(top : y ＝ u) (left : y ＝ z) (right : u ＝ v) (bottom : z ＝ v)
(s : v ＝ w) →
coherence-square-identifications top left right bottom →
coherence-square-identifications
( p ∙ top)
( p ∙ left)
( right ∙ s)
( bottom ∙ s)
double-whisker-coherence-square-identifications
p top left right bottom q H =
left-whisker-concat-coherence-square-identifications p top left
( right ∙ q)
( bottom ∙ q)
( right-whisker-concat-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( H)
( q))


#### Left splicing coherences of commuting squares of identifications

For any inverse pair of identifications p : y ＝ u and q : u ＝ y equipped with α : inv p ＝ q we obtain an equivalence

           top                                    top
x -------> y                         x -----------> y
|          |                         |              |
left |          | right    ≃     left ∙ p |              | right
∨          ∨                         ∨              ∨
z -------> w                         u -----------> w
bottom                               q ∙ bottom


of coherences of commuting squares of identifications.

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
where

left-splice-coherence-square-identifications :
{u : A} (p : z ＝ u) (q : u ＝ z) (α : inv p ＝ q) →
coherence-square-identifications top left right bottom →
coherence-square-identifications top (left ∙ p) right (q ∙ bottom)
left-splice-coherence-square-identifications refl .refl refl =
concat-left-identification-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( inv right-unit)

left-unsplice-coherence-square-identifications :
{u : A} (p : z ＝ u) (q : u ＝ z) (α : inv p ＝ q) →
coherence-square-identifications top (left ∙ p) right (q ∙ bottom) →
coherence-square-identifications top left right bottom
left-unsplice-coherence-square-identifications refl .refl refl =
inv-concat-left-identification-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( inv right-unit)


#### Right splicing coherences of commuting squares of identifications

For any inverse pair of identifications p : y ＝ u and q : u ＝ y equipped with α : inv p ＝ q we obtain an equivalence

           top                             top ∙ p
x -------> y                     x --------> u
|          |                     |           |
left |          | right    ≃     left |           | q ∙ right
∨          ∨                     ∨           ∨
z -------> w                     z --------> w
bottom                           bottom


of coherences of commuting squares of identifications.

module _
{l : Level} {A : UU l} {x y z w : A}
(top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w)
where

right-splice-coherence-square-identifications :
{u : A} (p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
coherence-square-identifications top left right bottom →
coherence-square-identifications (top ∙ p) left (inv p ∙ right) bottom
right-splice-coherence-square-identifications refl .refl refl =
concat-top-identification-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( inv right-unit)

right-unsplice-coherence-square-identifications :
{u : A} (p : y ＝ u) (q : u ＝ y) (α : inv p ＝ q) →
coherence-square-identifications (top ∙ p) left (inv p ∙ right) bottom →
coherence-square-identifications top left right bottom
right-unsplice-coherence-square-identifications refl .refl refl =
inv-concat-top-identification-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( inv right-unit)


### Horizontally pasting squares of identifications

Consider two squares of identifications as in the diagram

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


with s : left ∙ bottom-left ＝ top-left ∙ middle and t : middle ∙ bottom-right ＝ top-right ∙ right. Then the outer square commutes.

module _
{l : Level} {A : UU l} {a b c d e f : A}
(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-identifications :
coherence-square-identifications top-left left middle bottom-left →
coherence-square-identifications top-right middle right bottom-right →
coherence-square-identifications
(top-left ∙ top-right) left right (bottom-left ∙ bottom-right)
horizontal-pasting-coherence-square-identifications s t =
( right-whisker-concat-coherence-square-identifications
( top-left)
( left)
( middle)
( bottom-left)
( s)
( bottom-right)) ∙
( ( inv (assoc top-left middle bottom-right)) ∙
( left-whisker-concat-coherence-square-identifications
( top-left)
( top-right)
( middle)
( right)
( bottom-right)
( t)))


### Vertically pasting squares of identifications

Consider two squares of identifications as in the diagram

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


with s : top-left ∙ middle ＝ top ∙ top-right and t : bottom-left ∙ bottom ＝ middle ∙ bottom-right. Then the outer square commutes.

module _
{l : Level} {A : UU l} {a b c d e f : 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)
where

vertical-pasting-coherence-square-identifications :
coherence-square-identifications top top-left top-right middle →
coherence-square-identifications middle bottom-left bottom-right bottom →
coherence-square-identifications
top (top-left ∙ bottom-left) (top-right ∙ bottom-right) bottom
vertical-pasting-coherence-square-identifications s t =
( left-whisker-concat-coherence-square-identifications
( top-left)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( t)) ∙
( ( assoc top-left middle bottom-right) ∙
( right-whisker-concat-coherence-square-identifications
( top)
( top-left)
( top-right)
( middle)
( s)
( bottom-right)))


## Properties

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

module _
{l : Level} {A : UU l} {a b c d : A}
where

left-unit-law-horizontal-pasting-coherence-square-identifications :
(top : a ＝ b) (left : a ＝ c) (right : b ＝ d) (bottom : c ＝ d)
(s : coherence-square-identifications top left right bottom) →
horizontal-pasting-coherence-square-identifications
( refl)
( top)
( left)
( left)
( right)
( refl)
( bottom)
( horizontal-refl-coherence-square-identifications left)
( s) ＝
s
left-unit-law-horizontal-pasting-coherence-square-identifications
refl refl right refl s = refl


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

module _
{l : Level} {A : UU l} {a b c d : A}
where

right-unit-law-horizontal-pasting-coherence-square-identifications :
(top : a ＝ b) (left : a ＝ c) (right : b ＝ d) (bottom : c ＝ d)
(s : coherence-square-identifications top left right bottom) →
horizontal-pasting-coherence-square-identifications
( top)
( refl)
( left)
( right)
( right)
( bottom)
( refl)
( s)
( horizontal-refl-coherence-square-identifications right) ∙
right-whisker-concat right-unit right ＝
left-whisker-concat left right-unit ∙ s
right-unit-law-horizontal-pasting-coherence-square-identifications
refl refl .refl refl refl =
refl


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

module _
{l : Level} {A : UU l} {a b c d : A}
where

left-unit-law-vertical-pasting-coherence-square-identifications :
(top : a ＝ b) (left : a ＝ c) (right : b ＝ d) (bottom : c ＝ d)
(s : coherence-square-identifications top left right bottom) →
vertical-pasting-coherence-square-identifications
( top)
( refl)
( refl)
( top)
( left)
( right)
( bottom)
( vertical-refl-coherence-square-identifications top)
( s) ＝
s
left-unit-law-vertical-pasting-coherence-square-identifications
refl refl .refl refl refl = refl


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

module _
{l : Level} {A : UU l} {a b c d : A}
where

right-unit-law-vertical-pasting-coherence-square-identifications :
(top : a ＝ b) (left : a ＝ c) (right : b ＝ d) (bottom : c ＝ d)
(s : coherence-square-identifications top left right bottom) →
vertical-pasting-coherence-square-identifications
( top)
( left)
( right)
( bottom)
( refl)
( refl)
( bottom)
( s)
( vertical-refl-coherence-square-identifications bottom) ∙
left-whisker-concat top right-unit ＝
right-whisker-concat right-unit bottom ∙ s
right-unit-law-vertical-pasting-coherence-square-identifications
refl refl .(refl ∙ refl) refl refl =
refl


### Computing the right whiskering of a vertically constant square with an identification

Consider the vertically constant square of identifications

           p
x -----> y
|        |
refl |        | refl
∨        ∨
x -----> y
p


at an identification p : x ＝ y, and consider an identification q : y ＝ z. Then the right whiskering of the above square with q is the commuting square of identifications

            p
x -------> y
|          |
refl |   refl   | q
∨          ∨
x -------> z
p ∙ q

module _
{l1 : Level} {A : UU l1}
where

right-whisker-concat-vertical-refl-coherence-square-identifications :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
right-whisker-concat-coherence-square-identifications p refl refl p
( vertical-refl-coherence-square-identifications p)
( q) ＝
refl
right-whisker-concat-vertical-refl-coherence-square-identifications
refl refl =
refl


### Computing the right whiskering of a horizontally constant square with an identification

Consider a horizontally constant commuting square of identifications

       refl
x -----> x
|        |
p |        | p
∨        ∨
y -----> y
refl


at an identification p and consider an identification q : y ＝ z. Then the right whiskering of the above square with q is the square

       refl
x -----> x
|        |
p |  refl  | p ∙ q
∨        ∨
y -----> z.
q

module _
{l1 : Level} {A : UU l1}
where

right-whisker-concat-horizontal-refl-coherence-square-identifications :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
right-whisker-concat-coherence-square-identifications refl p p refl
( horizontal-refl-coherence-square-identifications p)
( q) ＝
refl
right-whisker-concat-horizontal-refl-coherence-square-identifications
refl refl =
refl


### Computing the left whiskering of a horizontally constant square with an identification

Consider an identification p : x ＝ y and a horizontally constant commuting square of identifications

       refl
y -----> y
|        |
q |        | q
∨        ∨
z -----> z
refl


at an identification q : y ＝ z. The the left whiskering of the above square with p is the commuting square

                                  q ∙ refl
x ------------------------------------------------------> y
|                                                         |
q ∙ p |  right-unit ∙ inv (right-whisker-concat right-unit p)   | p
∨                                                         ∨
z ------------------------------------------------------> z.
refl

module _
{l1 : Level} {A : UU l1}
where

left-whisker-concat-horizontal-refl-coherence-square-identifications :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
left-whisker-concat-coherence-square-identifications p refl q q refl
( horizontal-refl-coherence-square-identifications q) ∙
right-whisker-concat right-unit q ＝
right-unit
left-whisker-concat-horizontal-refl-coherence-square-identifications
refl refl =
refl

left-whisker-concat-horizontal-refl-coherence-square-identifications' :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
left-whisker-concat-coherence-square-identifications p refl q q refl
( horizontal-refl-coherence-square-identifications q) ＝
right-unit ∙ inv (right-whisker-concat right-unit q)
left-whisker-concat-horizontal-refl-coherence-square-identifications'
refl refl =
refl


### Computing the left whiskering of a vertically constant square with an identification

Consider the vertically constant square of identifications

           q
y -----> z
|        |
refl |        | refl
∨        ∨
y -----> z
q


at an identification q : y ＝ z and consider an identification p : x ＝ y. Then the left whiskering of the above square with p is the square

                                    p ∙ q
x ---------------------------------------------------> z
|                                                      |
p ∙ refl |  right-whisker-concat right-unit q ∙ inv right-unit  | refl
∨                                                      ∨
y ---------------------------------------------------> z.
q

module _
{l1 : Level} {A : UU l1}
where

left-whisker-concat-vertical-refl-coherence-square-identifications :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
left-whisker-concat-coherence-square-identifications p q refl refl q
( vertical-refl-coherence-square-identifications q) ∙
right-unit ＝
right-whisker-concat right-unit q
left-whisker-concat-vertical-refl-coherence-square-identifications
refl refl =
refl

left-whisker-concat-vertical-refl-coherence-square-identifications' :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
left-whisker-concat-coherence-square-identifications p q refl refl q
( vertical-refl-coherence-square-identifications q) ＝
right-whisker-concat right-unit q ∙ inv right-unit
left-whisker-concat-vertical-refl-coherence-square-identifications'
refl refl =
refl


### Left whiskering horizontal concatenations of squares with identifications

Consider a commuting diagram of identifications of the form

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


and consider an identification p : x ＝ a. Then the left whiskering of p and the horizontal concatenation of coherences of commuting squares is up to associativity the horizontal concatenation of the squares

              p ∙ top-left      top-right
x -------------> c -------------> e
|                |                |
p ∙ left |                | middle         | right
∨                ∨                ∨
b -------------> d -------------> f
bottom-left      bottom-right


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

module _
{l1 : Level} {A : UU l1}
where

left-whisker-concat-horizontal-pasting-coherence-square-identifications :
{x a b c d e f : A} (p : x ＝ 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-identifications top-left left middle bottom-left)
(r : coherence-square-identifications top-right middle right bottom-right) →
left-whisker-concat-coherence-square-identifications p
( top-left ∙ top-right)
( left)
( right)
( bottom-left ∙ bottom-right)
( horizontal-pasting-coherence-square-identifications
( top-left)
( top-right)
( left)
( middle)
( right)
( bottom-left)
( bottom-right)
( l)
( r)) ＝
horizontal-pasting-coherence-square-identifications
( p ∙ top-left)
( top-right)
( p ∙ left)
( middle)
( right)
( bottom-left)
( bottom-right)
( left-whisker-concat-coherence-square-identifications p
( top-left)
( left)
( middle)
( bottom-left)
( l))
( r) ∙
right-whisker-concat
( assoc p top-left top-right)
( right)
left-whisker-concat-horizontal-pasting-coherence-square-identifications
refl top-left top-right left middle right bottom-left bottom-right l r =
inv right-unit


### Left whiskering vertical concatenations of squares with identifications

Consider two squares of identifications as in the diagram

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


and consider an identification p : x ＝ a. Then the left whiskering of p with the vertical pasting of the two squares above is up to associativity the vertical pasting of the squares

                  p ∙ top
x --------> b
|           |
p ∙ top-left |           | top-right
∨  middle   ∨
c --------> d
|           |
bottom-left |           | bottom-right
∨           ∨
e --------> f.
bottom

module _
{l1 : Level} {A : UU l1}
where

left-whisker-concat-vertical-concat-coherence-square-identifications :
{x a b c d e f : A} (p : x ＝ 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-identifications top top-left top-right middle) →
(b :
coherence-square-identifications middle bottom-left bottom-right bottom) →
right-whisker-concat (assoc p top-left bottom-left) bottom ∙
left-whisker-concat-coherence-square-identifications p
( top)
( top-left ∙ bottom-left)
( top-right ∙ bottom-right)
( bottom)
( vertical-pasting-coherence-square-identifications
( top)
( top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( t)
( b)) ＝
vertical-pasting-coherence-square-identifications
( p ∙ top)
( p ∙ top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( left-whisker-concat-coherence-square-identifications p
( top)
( top-left)
( top-right)
( middle)
( t))
( b)
left-whisker-concat-vertical-concat-coherence-square-identifications
refl top top-left top-right middle bottom-left bottom-right bottom t b =
refl


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

Consider a commuting diagram of identifications of the form

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


and consider an identification q : f ＝ y. 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 ∙ q
∨                ∨                     ∨
b -------------> d ------------------> y
bottom-left      bottom-right ∙ q

module _
{l1 : Level} {A : UU l1}
where

right-whisker-concat-horizontal-pasting-coherence-square-identifications :
{a b c d e f y : 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-identifications top-left left middle bottom-left) →
(r : coherence-square-identifications top-right middle right bottom-right) →
(q : f ＝ y) →
right-whisker-concat-coherence-square-identifications
( top-left ∙ top-right)
( left)
( right)
( bottom-left ∙ bottom-right)
( horizontal-pasting-coherence-square-identifications
( top-left)
( top-right)
( left)
( middle)
( right)
( bottom-left)
( bottom-right)
( l)
( r))
( q) ＝
left-whisker-concat left (assoc bottom-left bottom-right q) ∙
horizontal-pasting-coherence-square-identifications
( top-left)
( top-right)
( left)
( middle)
( right ∙ q)
( bottom-left)
( bottom-right ∙ q)
( l)
( right-whisker-concat-coherence-square-identifications
( top-right)
( middle)
( right)
( bottom-right)
( r)
( q))
right-whisker-concat-horizontal-pasting-coherence-square-identifications
refl refl refl .refl .refl refl refl refl refl refl =
refl


### Right whiskering vertical concatenations of squares with identifications

Consider two squares of identifications as in the diagram

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


and consider an identification q : f ＝ y. Then the right whiskering of the vertical pasting of the two squares above with q is up to associativity the vertical pasting of the squares

                     top
a ------------> b
|               |
top-left |               | top-right
∨    middle     ∨
c ------------> d
|               |
bottom-left |               | bottom-right ∙ q
∨               ∨
e ------------> y.
bottom ∙ q

module _
{l1 : Level} {A : UU l1}
where

right-whisker-concat-vertical-pasting-coherence-square-identifications :
{a b c d e f y : 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-identifications top top-left top-right middle) →
(b :
coherence-square-identifications middle bottom-left bottom-right bottom) →
(q : f ＝ y) →
right-whisker-concat-coherence-square-identifications
( top)
( top-left ∙ bottom-left)
( top-right ∙ bottom-right)
( bottom)
( vertical-pasting-coherence-square-identifications
( top)
( top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right)
( bottom)
( t)
( b))
( q) ∙
left-whisker-concat top (assoc top-right bottom-right q) ＝
vertical-pasting-coherence-square-identifications
( top)
( top-left)
( top-right)
( middle)
( bottom-left)
( bottom-right ∙ q)
( bottom ∙ q)
( t)
( right-whisker-concat-coherence-square-identifications
( middle)
( bottom-left)
( bottom-right)
( bottom)
( b)
( q))
right-whisker-concat-vertical-pasting-coherence-square-identifications
refl refl .refl refl refl .refl refl refl refl refl =
refl