Commuting squares of pointed maps

Content created by Fredrik Bakke, Egbert Rijke and maybemabeline.

Created on 2023-05-03.

module structured-types.commuting-squares-of-pointed-maps where

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.whiskering-pointed-homotopies-composition


Idea

Consider a square of pointed maps

            top
A --------> X
|           |
left |           | right
∨           ∨
B --------> Y.
bottom


Such a square is said to be a commuting square of pointed maps if there is a pointed homotopy

  bottom ∘∗ left ~∗ right ∘∗ top.


Such a homotopy is referred to as the coherence of the commuting square of pointed maps.

Definitions

Coherences of commuting squares of pointed maps

module _
{l1 l2 l3 l4 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2}
{C : Pointed-Type l3} {X : Pointed-Type l4}
(top : C →∗ B) (left : C →∗ A) (right : B →∗ X) (bottom : A →∗ X)
where

coherence-square-pointed-maps : UU (l3 ⊔ l4)
coherence-square-pointed-maps =
bottom ∘∗ left ~∗ right ∘∗ top

coherence-square-maps-coherence-square-pointed-maps :
coherence-square-pointed-maps →
coherence-square-maps
( map-pointed-map top)
( map-pointed-map left)
( map-pointed-map right)
( map-pointed-map bottom)
coherence-square-maps-coherence-square-pointed-maps =
htpy-pointed-htpy


Operations

Left whiskering of coherences of commuting squares of pointed maps

Consider a commuting square of pointed maps

            top
A --------> X
|           |
left |           | right
∨           ∨
B --------> Y
bottom


and consider a pointed map f : Y →∗ Z. Then the square

              top
A -------------> X
|                |
left |                | f ∘∗ right
∨                ∨
B -------------> Z
f ∘∗ bottom


also commutes.

module _
{l1 l2 l3 l4 l5 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4} {Z : Pointed-Type l5}
(f : Y →∗ Z)
(top : A →∗ X) (left : A →∗ B) (right : X →∗ Y) (bottom : B →∗ Y)
(s : coherence-square-pointed-maps top left right bottom)
where

left-whisker-comp-coherence-square-pointed-maps :
coherence-square-pointed-maps top left (f ∘∗ right) (f ∘∗ bottom)
left-whisker-comp-coherence-square-pointed-maps =
concat-pointed-htpy
( associative-comp-pointed-map f bottom left)
( concat-pointed-htpy
( left-whisker-comp-pointed-htpy f _ _ s)
( inv-associative-comp-pointed-map f right top))


Left whiskering of coherences of commuting squares of pointed maps

Consider a commuting square of pointed maps

            top
A --------> X
|           |
left |           | right
∨           ∨
B --------> Y
bottom


and consider a pointed map f : Z →∗ A. Then the square

               f ∘∗ top
A ----------> X
|             |
left ∘∗ f |             | right
∨             ∨
B ----------> Z
bottom


also commutes.

module _
{l1 l2 l3 l4 l5 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4} {Z : Pointed-Type l5}
(top : A →∗ X) (left : A →∗ B) (right : X →∗ Y) (bottom : B →∗ Y)
(s : coherence-square-pointed-maps top left right bottom)
(f : Z →∗ A)
where

right-whisker-comp-coherence-square-pointed-maps :
coherence-square-pointed-maps (top ∘∗ f) (left ∘∗ f) right bottom
right-whisker-comp-coherence-square-pointed-maps =
concat-pointed-htpy
( inv-associative-comp-pointed-map bottom left f)
( concat-pointed-htpy
( right-whisker-comp-pointed-htpy _ _ s f)
( associative-comp-pointed-map right top f))


Horizontal pasting of coherences of commuting squares of pointed maps

Consider two commuting squares of pointed maps, as in the diagram

            top-left         top-right
A -------------> B --------------> C
|                |                 |
left |                | middle          | right
∨                ∨                 ∨
D -------------> E --------------> F
bottom-left      bottom-right


with pointed homotopies

  H : bottom-left ∘∗ left ~∗ middle ∘∗ top
K : bottom-right ∘∗ middle ~∗ right ∘∗ top-right.


The horizontal pasting of these coherences of commuting squares of pointed maps is the coherence of the commuting square

             top-right ∘∗ top-left
A -----------------------------> C
|                                |
left |                                | right
∨                                ∨
D -----------------------------> F
bottom-right ∘∗ bottom-left


obtained by concatenation of the following three pointed homotopies:

  (bottom-right ∘∗ bottom-left) ∘∗ left
~∗ (bottom-right ∘∗ middle) ∘∗ top-left
~∗ bottom-right ∘∗ (middle ∘∗ top-left)
~∗ right ∘∗ (top-right ∘∗ top-left).


The first and third homotopy in this concatenation are the whiskerings of coherences of commuting triangles of pointed maps.

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2}
{X : Pointed-Type l3} {Y : Pointed-Type l4}
{U : Pointed-Type l5} {V : Pointed-Type l6}
(top-left : A →∗ X) (top-right : X →∗ U)
(left : A →∗ B) (middle : X →∗ Y) (right : U →∗ V)
(bottom-left : B →∗ Y) (bottom-right : Y →∗ V)
(left-square :
coherence-square-pointed-maps top-left left middle bottom-left)
(right-square :
coherence-square-pointed-maps top-right middle right bottom-right)
where

horizontal-pasting-coherence-square-pointed-maps :
coherence-square-pointed-maps
( top-right ∘∗ top-left)
( left)
( right)
( bottom-right ∘∗ bottom-left)
horizontal-pasting-coherence-square-pointed-maps =
concat-pointed-htpy
( left-whisker-comp-coherence-square-pointed-maps
( bottom-right)
( top-left)
( left)
( middle)
( bottom-left)
( left-square))
( concat-pointed-htpy
( associative-comp-pointed-map bottom-right middle top-left)
( right-whisker-comp-coherence-square-pointed-maps
( top-right)
( middle)
( right)
( bottom-right)
( right-square)
( top-left)))


Vertical pasting of coherences of commuting squares of pointed maps

Consider two commuting squares of pointed maps, as in the diagram

                   top
A --------> B
|           |
top-left |           | top-right
∨  middle   ∨
C --------> D
|           |
bottom-left |           | bottom-right
∨           ∨
E --------> F
bottom


with pointed homotopies

  H : middle ∘∗ top-left ~∗ top-right ∘∗ top
K : bottom ∘∗ bottom-left ~∗  bottom-right ∘∗ middle.


The vertical pasting of these coherences of commuting squares of pointed maps is the coherence of the commuting square

                               top
A --------> B
|           |
bottom-left ∘∗ top-left |           | bottom-right ∘∗ top-right
∨           ∨
E --------> F
bottom


obtained by concatenation of the following three pointed homotopies:

  bottom ∘∗ (bottom-left ∘∗ top-left)
~∗ bottom-right ∘∗ (middle ∘∗ top-left)
~∗ (bottom-right ∘∗ middle) ∘∗ top-left
~∗ (bottom-right ∘∗ top-right) ∘∗ top.


The first and third homotopy in this concatenation are the whiskerings of coherences of commuting triangles of pointed maps.

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : Pointed-Type l1} {B : Pointed-Type l2}
{C : Pointed-Type l3} {D : Pointed-Type l4}
{E : Pointed-Type l5} {F : Pointed-Type l6}
(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)
(top-square : coherence-square-pointed-maps top top-left top-right middle)
(bottom-square :
coherence-square-pointed-maps middle bottom-left bottom-right bottom)
where

vertical-pasting-coherence-square-pointed-maps :
coherence-square-pointed-maps
( top)
( bottom-left ∘∗ top-left)
( bottom-right ∘∗ top-right)
( bottom)
vertical-pasting-coherence-square-pointed-maps =
concat-pointed-htpy
( right-whisker-comp-coherence-square-pointed-maps
( middle)
( bottom-left)
( bottom-right)
( bottom)
( bottom-square)
( top-left))
( concat-pointed-htpy
( inv-associative-comp-pointed-map bottom-right middle top-left)
( left-whisker-comp-coherence-square-pointed-maps
( bottom-right)
( top)
( top-left)
( top-right)
( middle)
( top-square)))