Commuting pentagons of identifications

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2023-11-01.

module foundation.commuting-pentagons-of-identifications where
Imports
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.

Definition

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

Recent changes