Commuting squares of identifications

Content created by Fredrik Bakke and Raymond Baker.

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

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

Recent changes