Hexagons of identifications

module foundation.hexagons-of-identifications where

open import foundation-core.identity-types
open import foundation-core.universe-levels

Idea

A hexagon of identifications is an identification ((α ∙ β) ∙ γ) ＝ (δ ∙ (ε ∙ ζ)).

Definition

Hexagons of identifications

coherence-hexagon :
  {l : Level} {A : UU l} {x u u' v v' y : A}
  (α : x ＝ u) (β : u ＝ u') (γ : u' ＝ y)
  (δ : x ＝ v) (ε : v ＝ v') (ζ : v' ＝ y) → UU l
coherence-hexagon α β γ δ ε ζ = ((α ∙ β) ∙ γ) ＝ (δ ∙ (ε ∙ ζ))

Symmetries of hexagons of identifications

module _
  {l : Level} {A : UU l} {x u u' v v' y : A}
  where

  hexagon-rotate-120 :
    (α : x ＝ u) (β : u ＝ u') (γ : u' ＝ y)
    (δ : x ＝ v) (ε : v ＝ v') (ζ : v' ＝ y) →
    coherence-hexagon α β γ δ ε ζ →
    coherence-hexagon (inv ε) (inv δ) α ζ (inv γ) (inv β)
  hexagon-rotate-120 refl refl refl refl refl .refl refl = refl

  hexagon-rotate-240 :
    (α : x ＝ u) (β : u ＝ u') (γ : u' ＝ y)
    (δ : x ＝ v) (ε : v ＝ v') (ζ : v' ＝ y) →
    coherence-hexagon α β γ δ ε ζ →
    coherence-hexagon γ (inv ζ) (inv ε) (inv β) (inv α) δ
  hexagon-rotate-240 refl refl refl refl refl .refl refl = refl

  hexagon-mirror-A :
    (α : x ＝ u) (β : u ＝ u') (γ : u' ＝ y)
    (δ : x ＝ v) (ε : v ＝ v') (ζ : v' ＝ y) →
    coherence-hexagon α β γ δ ε ζ →
    coherence-hexagon ε ζ (inv γ) (inv δ) α β
  hexagon-mirror-A refl refl refl refl refl .refl refl = refl

  hexagon-mirror-B :
    (α : x ＝ u) (β : u ＝ u') (γ : u' ＝ y)
    (δ : x ＝ v) (ε : v ＝ v') (ζ : v' ＝ y) →
    coherence-hexagon α β γ δ ε ζ →
    coherence-hexagon (inv α) δ ε β γ (inv ζ)
  hexagon-mirror-B refl refl refl refl refl .refl refl = refl

  hexagon-mirror-C :
    (α : x ＝ u) (β : u ＝ u') (γ : u' ＝ y)
    (δ : x ＝ v) (ε : v ＝ v') (ζ : v' ＝ y) →
    coherence-hexagon α β γ δ ε ζ →
    coherence-hexagon (inv γ) (inv β) (inv α) (inv ζ) (inv ε) (inv δ)
  hexagon-mirror-C refl refl refl refl refl .refl refl = refl