# Commuting pentagons of identifications

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

Created on 2023-11-01.

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)