Commuting pentagons of identifications

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

Created on 2023-11-01.
Last modified on 2024-04-16.

module foundation.commuting-pentagons-of-identifications where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.identity-types

Idea

A pentagon of identifications

               top
             x --- y
   top-left /       \ top-right
           /         \
          z           w
            \       /
  bottom-left \   / bottom-right
                v

is said to commute if there is an identification

  top-left ∙ bottom-left ＝ (top ∙ top-right) ∙ bottom-right.

Such an identification is called a coherence of the pentagon.

Definitions

Commuting pentagons of identifications

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

  coherence-pentagon-identifications :
    (top : x ＝ y)
    (top-left : x ＝ z) (top-right : y ＝ w)
    (bottom-left : z ＝ v) (bottom-right : w ＝ v) → UU l
  coherence-pentagon-identifications
    top top-left top-right bottom-left bottom-right =
    top-left ∙ bottom-left ＝ (top ∙ top-right) ∙ bottom-right

Reflections of commuting pentagons of identifications

A pentagon may be reflected along an axis connecting an edge with its opposing vertex. For example, we may reflect a pentagon

               top
             x --- y
   top-left /       \ top-right
           /         \
          z           w
            \       /
  bottom-left \   / bottom-right
                v

along the axis connecting top and v to get

               top⁻¹
              y --- x
   top-right /       \ top-left
            /         \
           w           z
             \       /
  bottom-right \   / bottom-left
                 v .

The reflections are named after the edge which the axis passes through, so the above example is reflect-top-coherence-pentagon-identifications.

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

  reflect-top-coherence-pentagon-identifications :
    (top : x ＝ y)
    (top-left : x ＝ z) (top-right : y ＝ w)
    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
    coherence-pentagon-identifications
      ( top)
      ( top-left)
      ( top-right)
      ( bottom-left)
      ( bottom-right) →
    coherence-pentagon-identifications
      ( inv top)
      ( top-right)
      ( top-left)
      ( bottom-right)
      ( bottom-left)
  reflect-top-coherence-pentagon-identifications
    refl top-left top-right bottom-left bottom-right H = inv H

  reflect-top-left-coherence-pentagon-identifications :
    (top : x ＝ y)
    (top-left : x ＝ z) (top-right : y ＝ w)
    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
    coherence-pentagon-identifications
      ( top)
      ( top-left)
      ( top-right)
      ( bottom-left)
      ( bottom-right) →
    coherence-pentagon-identifications
      ( bottom-left)
      ( inv top-left)
      ( inv bottom-right)
      ( top)
      ( inv top-right)
  reflect-top-left-coherence-pentagon-identifications
    refl refl refl bottom-left refl H =
    inv (right-unit ∙ right-unit ∙ H)

  reflect-top-right-coherence-pentagon-identifications :
    (top : x ＝ y)
    (top-left : x ＝ z) (top-right : y ＝ w)
    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
    coherence-pentagon-identifications
      ( top)
      ( top-left)
      ( top-right)
      ( bottom-left)
      ( bottom-right) →
    coherence-pentagon-identifications
      ( inv bottom-right)
      ( inv bottom-left)
      ( inv top-right)
      ( inv top-left)
      ( inv top)
  reflect-top-right-coherence-pentagon-identifications
    refl top-left refl refl refl H =
    ap inv (inv right-unit ∙ H)

  reflect-bottom-left-coherence-pentagon-identifications :
    (top : x ＝ y)
    (top-left : x ＝ z) (top-right : y ＝ w)
    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
    coherence-pentagon-identifications
      ( top)
      ( top-left)
      ( top-right)
      ( bottom-left)
      ( bottom-right) →
    coherence-pentagon-identifications
      ( inv top-right)
      ( bottom-right)
      ( inv top)
      ( inv bottom-left)
      ( top-left)
  reflect-bottom-left-coherence-pentagon-identifications
    refl refl refl refl bottom-right H = right-unit ∙ inv H

  reflect-bottom-right-coherence-pentagon-identifications :
    (top : x ＝ y)
    (top-left : x ＝ z) (top-right : y ＝ w)
    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
    coherence-pentagon-identifications
      ( top)
      ( top-left)
      ( top-right)
      ( bottom-left)
      ( bottom-right) →
    coherence-pentagon-identifications
      ( bottom-left)
      ( inv top-left)
      ( inv bottom-right)
      ( top)
      ( inv top-right)
  reflect-bottom-right-coherence-pentagon-identifications
    refl refl refl bottom-left refl H =
    inv (right-unit ∙ right-unit ∙ H)

Recent changes