Commuting prisms of maps

Content created by Fredrik Bakke, Vojtěch Štěpančík and Egbert Rijke.

Created on 2023-12-05.
Last modified on 2024-04-25.

module foundation-core.commuting-prisms-of-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.commuting-pentagons-of-identifications
open import foundation.identity-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import foundation-core.commuting-squares-of-maps
open import foundation-core.commuting-triangles-of-maps
open import foundation-core.homotopies

Idea

Consider an arrangment of maps composable into a diagram as follows:

          hA
    A ---------> A'
    |\           |\
    | \ h   ⇗    | \ h'
    |  \      f' |  \
    |   ∨        |   ∨
  f | ⇐ B ------ | -> B'
    |   /   hB   | ⇐ /
    |  / g       |  / g'
    | /     ⇗    | /
    ∨∨           ∨∨
    C ---------> C' ,
          hC

and homotopies filling its faces. Then a horizontal commuting prism of maps is a homotopy filling the shape. In other words, we may choose two homotopies from the composition hC ∘ g ∘ h to f' ∘ hA, namely following 1) the left triangle and then the front square, or 2) the two back squares and then the right triangle; the prism is then a homotopy between these two homotopies. In this way, a commuting prism may be viewed as a homotopy between a pasting of squares and their composite — that is the motivation for having the triangles go the unconventional way, from the composition to the composite.

We may also arrange the maps into a more vertical shape, like so:

          B
      h  ∧| \  g
       /  |   \
     /  f | ⇑   ∨
    A ---------> C
    |     | hB   |
    | ⇗   ∨   ⇗  |
 hA |     B'     | hC
    | h' ∧  \ g' |
    |  /  ⇑   \  |
    ∨/          ∨∨
    A' --------> C' .
          f'

Then, given homotopies for the faces, we call a homotopy filling this shape a vertical commuting prism of maps. This rotation of a prism may be viewed as a homotopy between two triangles with different but related sides.

It remains to be formalized that the type of vertical prisms is equivalent to the type of horizontal prisms.

Definitions

Horizontal commuting prisms of maps

module _
  { l1 l2 l3 l1' l2' l3' : Level}
  { A : UU l1} {B : UU l2} {C : UU l3}
  { A' : UU l1'} {B' : UU l2'} {C' : UU l3'}
  ( hA : A → A') (h : A → B) (h' : A' → B')
  ( hB : B → B') (g : B → C) (g' : B' → C')
  ( hC : C → C') (f : A → C) (f' : A' → C')
  ( left : coherence-triangle-maps' f g h)
  ( sq-top : coherence-square-maps hA h h' hB)
  ( sq-bottom : coherence-square-maps hB g g' hC)
  ( sq-front : coherence-square-maps hA f f' hC)
  ( right : coherence-triangle-maps' f' g' h')
  where

  horizontal-coherence-prism-maps : UU (l1 ⊔ l3')
  horizontal-coherence-prism-maps =
    ( ( hC ·l left) ∙h sq-front) ~
    ( ( pasting-vertical-coherence-square-maps hA h h' hB g g' hC
        ( sq-top)
        ( sq-bottom)) ∙h
      ( right ·r hA))

Vertical commuting prisms of maps

Because triangular prisms are less symmetric than, say, cubes, we have more than one natural formulation for where to draw the "seams" for the filler. Here, we present two choices, and show that they are equivalent in foundation.commuting-prisms-of-maps.

module _
  { l1 l2 l3 l1' l2' l3' : Level}
  { A : UU l1} {B : UU l2} {C : UU l3}
  ( f : A → C) (g : B → C) (h : A → B)
  { A' : UU l1'} {B' : UU l2'} {C' : UU l3'}
  ( f' : A' → C') (g' : B' → C') (h' : A' → B')
  ( hA : A → A') (hB : B → B') (hC : C → C')
  where

  module _
    ( top : coherence-triangle-maps f g h)
    ( front : coherence-square-maps f hA hC f')
    ( right : coherence-square-maps g hB hC g')
    ( left : coherence-square-maps h hA hB h')
    ( bottom : coherence-triangle-maps f' g' h')
    where

    vertical-coherence-prism-maps : UU (l1 ⊔ l3')
    vertical-coherence-prism-maps =
      ( ( bottom ·r hA) ∙h
        ( pasting-horizontal-coherence-square-maps h g hA hB hC h' g'
          ( left)
          ( right))) ~
      ( front ∙h (hC ·l top))

  module _
    ( top : coherence-triangle-maps f g h)
    ( inv-front : coherence-square-maps' f hA hC f')
    ( inv-right : coherence-square-maps' g hB hC g')
    ( left : coherence-square-maps h hA hB h')
    ( bottom : coherence-triangle-maps f' g' h')
    where

    vertical-coherence-prism-maps' : UU (l1 ⊔ l3')
    vertical-coherence-prism-maps' =
      ( inv-front ∙h ((bottom ·r hA) ∙h (g' ·l left))) ~
      ( (hC ·l top) ∙h (inv-right ·r h))

  module _
    ( top : coherence-triangle-maps f g h)
    ( inv-front : coherence-square-maps' f hA hC f')
    ( inv-right : coherence-square-maps' g hB hC g')
    ( inv-left : coherence-square-maps' h hA hB h')
    ( bottom : coherence-triangle-maps f' g' h')
    where

    vertical-coherence-prism-inv-squares-maps : UU (l1 ⊔ l3')
    vertical-coherence-prism-inv-squares-maps =
      ( inv-front ∙h (bottom ·r hA)) ~
      ( (hC ·l top) ∙h ((inv-right ·r h) ∙h (g' ·l inv-left)))

  module _
    ( inv-top : coherence-triangle-maps' f g h)
    ( front : coherence-square-maps f hA hC f')
    ( right : coherence-square-maps g hB hC g')
    ( left : coherence-square-maps h hA hB h')
    ( inv-bottom : coherence-triangle-maps' f' g' h')
    where

    vertical-coherence-prism-inv-triangles-maps : UU (l1 ⊔ l3')
    vertical-coherence-prism-inv-triangles-maps =
      ( (g' ·l left) ∙h (right ·r h) ∙h (hC ·l inv-top)) ~
      ( (inv-bottom ·r hA) ∙h front)

  module _
    ( inv-top : coherence-triangle-maps' f g h)
    ( inv-front : coherence-square-maps' f hA hC f')
    ( inv-right : coherence-square-maps' g hB hC g')
    ( inv-left : coherence-square-maps' h hA hB h')
    ( inv-bottom : coherence-triangle-maps' f' g' h')
    where

    vertical-coherence-prism-inv-boundary-maps : UU (l1 ⊔ l3')
    vertical-coherence-prism-inv-boundary-maps =
      ( (inv-right ·r h) ∙h (g' ·l inv-left) ∙h (inv-bottom ·r hA)) ~
      ( (hC ·l inv-top) ∙h inv-front)

Translations between coherences of prisms of maps

Our different formulations of commuting prisms of maps are of course all equivalent, although this remains to be formalized. Below, we record various translations between them.

module _
  { l1 l2 l3 l1' l2' l3' : Level}
  { A : UU l1} {B : UU l2} {C : UU l3}
  ( f : A → C) (g : B → C) (h : A → B)
  { A' : UU l1'} {B' : UU l2'} {C' : UU l3'}
  ( f' : A' → C') (g' : B' → C') (h' : A' → B')
  ( hA : A → A') (hB : B → B') (hC : C → C')
  where

  module _
    ( top : coherence-triangle-maps f g h)
    ( inv-front : coherence-square-maps' f hA hC f')
    ( inv-right : coherence-square-maps' g hB hC g')
    ( inv-left : coherence-square-maps' h hA hB h')
    ( bottom : coherence-triangle-maps f' g' h')
    where

    vertical-coherence-prism-maps-vertical-coherence-prism-inv-squares-maps :
      vertical-coherence-prism-inv-squares-maps f g h f' g' h' hA hB hC
        ( top)
        ( inv-front)
        ( inv-right)
        ( inv-left)
        ( bottom) →
      vertical-coherence-prism-maps f g h f' g' h' hA hB hC
        ( top)
        ( inv-htpy inv-front)
        ( inv-htpy inv-right)
        ( inv-htpy inv-left)
        ( bottom)
    vertical-coherence-prism-maps-vertical-coherence-prism-inv-squares-maps H =
      ( ap-concat-htpy
        ( bottom ·r hA)
        ( ( ap-concat-htpy'
            ( inv-htpy inv-right ·r h)
            ( left-whisker-inv-htpy g' inv-left)) ∙h
          ( inv-htpy-distributive-inv-concat-htpy
            ( inv-right ·r h)
            ( g' ·l inv-left)))) ∙h
      ( inv-htpy-right-transpose-htpy-concat
        ( inv-htpy inv-front ∙h (hC ·l top))
        ( inv-right ·r h ∙h (g' ·l inv-left))
        ( bottom ·r hA)
        ( ( assoc-htpy
            ( inv-htpy inv-front)
            ( hC ·l top)
            ( inv-right ·r h ∙h (g' ·l inv-left))) ∙h
          ( inv-htpy-left-transpose-htpy-concat
            ( inv-front)
            ( bottom ·r hA)
            ( (hC ·l top) ∙h (inv-right ·r h ∙h (g' ·l inv-left)))
            ( H))))

  module _
    ( top : coherence-triangle-maps f g h)
    ( inv-front : coherence-square-maps f hA hC f')
    ( inv-right : coherence-square-maps g hB hC g')
    ( inv-left : coherence-square-maps h hA hB h')
    ( bottom : coherence-triangle-maps f' g' h')
    where

    vertical-coherence-prism-inv-squares-maps-vertical-coherence-prism-maps :
      vertical-coherence-prism-maps f g h f' g' h' hA hB hC
        ( top)
        ( inv-front)
        ( inv-right)
        ( inv-left)
        ( bottom) →
      vertical-coherence-prism-inv-squares-maps f g h f' g' h' hA hB hC
        ( top)
        ( inv-htpy inv-front)
        ( inv-htpy inv-right)
        ( inv-htpy inv-left)
        ( bottom)
    vertical-coherence-prism-inv-squares-maps-vertical-coherence-prism-maps
      H a =
      ( reflect-top-left-coherence-pentagon-identifications
        ( bottom (hA a))
        ( inv-front a)
        ( ap g' (inv-left a))
        ( ap hC (top a))
        ( inv-right (h a))
        ( inv
          ( ( assoc (bottom (hA a)) (ap g' (inv-left a)) (inv-right (h a))) ∙
            ( H a)))) ∙
      ( left-whisker-concat
        ( ap hC (top a) ∙ inv (inv-right (h a)))
        ( inv (ap-inv g' (inv-left a)))) ∙
      ( assoc
        ( ap hC (top a))
        ( inv (inv-right (h a)))
        ( ap g' (inv (inv-left a))))

  module _
    ( inv-top : coherence-triangle-maps' f g h)
    ( inv-front : coherence-square-maps' f hA hC f')
    ( inv-right : coherence-square-maps' g hB hC g')
    ( inv-left : coherence-square-maps' h hA hB h')
    ( inv-bottom : coherence-triangle-maps' f' g' h')
    where

    vertical-coherence-prism-inv-triangles-maps-vertical-coherence-prism-inv-boundary-maps :
      vertical-coherence-prism-inv-boundary-maps f g h f' g' h' hA hB hC
        ( inv-top)
        ( inv-front)
        ( inv-right)
        ( inv-left)
        ( inv-bottom) →
      vertical-coherence-prism-inv-triangles-maps f g h f' g' h' hA hB hC
        ( inv-top)
        ( inv-htpy inv-front)
        ( inv-htpy inv-right)
        ( inv-htpy inv-left)
        ( inv-bottom)
    vertical-coherence-prism-inv-triangles-maps-vertical-coherence-prism-inv-boundary-maps
      H =
      ( ap-concat-htpy'
        ( hC ·l inv-top)
        ( ( ap-concat-htpy'
            ( inv-htpy inv-right ·r h)
            ( left-whisker-inv-htpy g' inv-left)) ∙h
          ( inv-htpy-distributive-inv-concat-htpy
            ( inv-right ·r h)
            ( g' ·l inv-left)))) ∙h
      ( right-transpose-htpy-concat
        ( ( inv-htpy (inv-right ·r h ∙h (g' ·l inv-left))) ∙h (hC ·l inv-top))
        ( inv-front)
        ( inv-bottom ·r hA)
        ( ( assoc-htpy
            ( inv-htpy (inv-right ·r h ∙h (g' ·l inv-left)))
            ( hC ·l inv-top)
            ( inv-front)) ∙h
          ( inv-htpy-left-transpose-htpy-concat
            ( inv-right ·r h ∙h (g' ·l inv-left))
            ( inv-bottom ·r hA)
            ( (hC ·l inv-top) ∙h inv-front)
            ( H))))

Recent changes