Commuting squares of homotopies

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

Created on 2024-02-06.
Last modified on 2024-07-23.

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)

Recent changes