From 010678433590ad230be28efb1df031ff31c5c082 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 17 Sep 2023 18:05:43 +0200
Subject: [PATCH] Moving file about hexagons of identifications (#782)

---
 src/foundation-core.lagda.md                  |   1 -
 .../commuting-cubes-of-maps.lagda.md          | 412 ------------------
 src/foundation-core/identity-types.lagda.md   |   2 +-
 src/foundation.lagda.md                       |   2 +-
 .../commuting-cubes-of-maps.lagda.md          | 384 ++++++++++++++--
 ...ting-hexagons-of-identifications.lagda.md} |   4 +-
 src/foundation/cones-over-cospans.lagda.md    |  24 +-
 src/foundation/identity-types.lagda.md        |   2 +-
 src/foundation/pullbacks.lagda.md             |  14 +-
 9 files changed, 361 insertions(+), 484 deletions(-)
 delete mode 100644 src/foundation-core/commuting-cubes-of-maps.lagda.md
 rename src/foundation/{hexagons-of-identifications.lagda.md => commuting-hexagons-of-identifications.lagda.md} (95%)

diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
index b62cb22a60..cd39ca220d 100644
--- a/src/foundation-core.lagda.md
+++ b/src/foundation-core.lagda.md
@@ -8,7 +8,6 @@ module foundation-core where
 open import foundation-core.1-types public
 open import foundation-core.cartesian-product-types public
 open import foundation-core.coherently-invertible-maps public
-open import foundation-core.commuting-cubes-of-maps public
 open import foundation-core.commuting-squares-of-maps public
 open import foundation-core.commuting-triangles-of-maps public
 open import foundation-core.constant-maps public
diff --git a/src/foundation-core/commuting-cubes-of-maps.lagda.md b/src/foundation-core/commuting-cubes-of-maps.lagda.md
deleted file mode 100644
index 492a3d2df5..0000000000
--- a/src/foundation-core/commuting-cubes-of-maps.lagda.md
+++ /dev/null
@@ -1,412 +0,0 @@
-# Commuting cubes of maps
-
-```agda
-module foundation-core.commuting-cubes-of-maps where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.action-on-identifications-functions
-open import foundation.cones-over-cospans
-open import foundation.dependent-pair-types
-open import foundation.hexagons-of-identifications
-open import foundation.universe-levels
-
-open import foundation-core.function-types
-open import foundation-core.homotopies
-open import foundation-core.identity-types
-open import foundation-core.whiskering-homotopies
-```
-
-</details>
-
-## Idea
-
-We specify the type of the homotopy witnessing that a cube commutes. Imagine
-that the cube is presented as a lattice
-
-```text
-            *
-          / | \
-         /  |  \
-        /   |   \
-       *    *    *
-       |\ /   \ /|
-       | \     ‌/ |
-       |/ \   / \|
-       *    *    *
-        \   |   /
-         \  |  /
-          \ | /
-            *
-```
-
-with all maps pointing in the downwards direction. Presented in this way, a cube
-of maps has a top face, a back-left face, a back-right face, a front-left face,
-a front-right face, and a bottom face, all of which are homotopies. An element
-of type `coherence-cube-maps` is a homotopy filling the cube.
-
-## Definition
-
-```agda
-coherence-cube-maps :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  UU (l4 ⊔ l1')
-coherence-cube-maps
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  (((h ·l back-left) ∙h (front-left ·r f')) ∙h (hD ·l top)) ~
-  ((bottom ·r hA) ∙h ((k ·l back-right) ∙h (front-right ·r g')))
-```
-
-### Symmetries of commuting cubes
-
-The symmetry group D₃ acts on a cube. However, the coherence filling a cube
-needs to be modified to show that the rotated/reflected cube again commutes. In
-the following definitions we provide the homotopies witnessing that the
-rotated/reflected cubes again commute.
-
-Note: although in principle it ought to be enough to show this for the
-generators of the symmetry group D₃, in practice it is more straightforward to
-just do the work for each of the symmetries separately. One reason is that some
-of the homotopies witnessing that the faces commute will be inverted as the
-result of an application of a symmetry. Inverting a homotopy twice results in a
-new homotopy that is only homotopic to the original homotopy.
-
-```agda
-module _
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g))
-  (c :
-    coherence-cube-maps
-      f g h k f' g' h' k' hA hB hC hD
-      top back-left back-right front-left front-right bottom)
-  where
-
-  coherence-cube-maps-rotate-120 :
-    coherence-cube-maps hC k' k hD hA f' f hB g' g h' h
-      ( back-left)
-      ( inv-htpy back-right)
-      ( inv-htpy top)
-      ( inv-htpy bottom)
-      ( inv-htpy front-left)
-      ( front-right)
-  coherence-cube-maps-rotate-120 a' =
-    ( ap (λ t → t ∙ (ap h (back-left a')))
-      ( ap (λ t' → t' ∙ inv (bottom (hA a')))
-        ( ap-inv k (back-right a')))) ∙
-    ( ( hexagon-rotate-120
-        ( ap h (back-left a'))
-        ( front-left (f' a'))
-        ( ap hD (top a'))
-        ( bottom (hA a'))
-        ( ap k (back-right a'))
-        ( front-right (g' a'))
-        ( c a')) ∙
-      ( inv
-        ( ap (λ t → (front-right (g' a')) ∙ t)
-          ( ap (λ t' → t' ∙ inv (front-left (f' a')))
-            ( ap-inv hD (top a'))))))
-
-  coherence-cube-maps-rotate-240 :
-    coherence-cube-maps h' hB hD h g' hA hC g f' k' f k
-      ( inv-htpy back-right)
-      ( top)
-      ( inv-htpy back-left)
-      ( inv-htpy front-right)
-      ( bottom)
-      ( inv-htpy front-left)
-  coherence-cube-maps-rotate-240 a' =
-    ( ap (λ t → _ ∙ t) (ap-inv k (back-right a'))) ∙
-    ( ( hexagon-rotate-240
-        ( ap h (back-left a'))
-        ( front-left (f' a'))
-        ( ap hD (top a'))
-        ( bottom (hA a'))
-        ( ap k (back-right a'))
-        ( front-right (g' a'))
-        ( c a')) ∙
-      ( inv
-        ( ap
-          ( λ t → inv (front-left (f' a')) ∙ t)
-          ( ap (λ t' → t' ∙ _) (ap-inv h (back-left a'))))))
-
-  coherence-cube-maps-mirror-A :
-    coherence-cube-maps g f k h g' f' k' h' hA hC hB hD
-      ( inv-htpy top)
-      ( back-right)
-      ( back-left)
-      ( front-right)
-      ( front-left)
-      ( inv-htpy bottom)
-  coherence-cube-maps-mirror-A a' =
-    ( ap (λ t → _ ∙ t) (ap-inv hD (top a'))) ∙
-    ( hexagon-mirror-A
-      ( ap h (back-left a'))
-      ( front-left (f' a'))
-      ( ap hD (top a'))
-      ( bottom (hA a'))
-      ( ap k (back-right a'))
-      ( front-right (g' a'))
-      ( c a'))
-
-  coherence-cube-maps-mirror-B :
-    coherence-cube-maps hB h' h hD hA g' g hC f' f k' k
-      ( back-right)
-      ( inv-htpy back-left)
-      ( top)
-      ( bottom)
-      ( inv-htpy front-right)
-      ( front-left)
-  coherence-cube-maps-mirror-B a' =
-    ( ap (λ t → t ∙ (ap k (back-right a')))
-      ( ap (λ t → t ∙ _) (ap-inv h (back-left a')))) ∙
-    ( hexagon-mirror-B
-      ( ap h (back-left a'))
-      ( front-left (f' a'))
-      ( ap hD (top a'))
-      ( bottom (hA a'))
-      ( ap k (back-right a'))
-      ( front-right (g' a'))
-      ( c a'))
-
-  coherence-cube-maps-mirror-C :
-    coherence-cube-maps k' hC hD k f' hA hB f g' h' g h
-      ( inv-htpy back-left)
-      ( inv-htpy top)
-      ( inv-htpy back-right)
-      ( inv-htpy front-left)
-      ( inv-htpy bottom)
-      ( inv-htpy front-right)
-  coherence-cube-maps-mirror-C a' =
-    ( ap
-      ( λ t → (t ∙ inv (front-left (f' a'))) ∙ (ap h (inv (back-left a'))))
-      ( ap-inv hD (top a'))) ∙
-    ( ( ap (λ t → _ ∙ t) (ap-inv h (back-left a'))) ∙
-      ( ( hexagon-mirror-C
-          ( ap h (back-left a'))
-          ( front-left (f' a'))
-          ( ap hD (top a'))
-          ( bottom (hA a'))
-          ( ap k (back-right a'))
-          ( front-right (g' a'))
-          ( c a')) ∙
-        ( inv
-          ( ap
-            ( λ t → inv (front-right (g' a')) ∙ t)
-            ( ap (λ t' → t' ∙ _) (ap-inv k (back-right a')))))))
-```
-
-### Rectangles in commuting cubes
-
-```agda
-rectangle-back-left-front-left-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  ((h ∘ f) ∘ hA) ~ (hD ∘ (h' ∘ f'))
-rectangle-back-left-front-left-cube f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  (h ·l back-left) ∙h (front-left ·r f')
-
-rectangle-back-right-front-right-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  ((k ∘ g) ∘ hA) ~ (hD ∘ (k' ∘ g'))
-rectangle-back-right-front-right-cube f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  (k ·l back-right) ∙h (front-right ·r g')
-
-coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g))
-  (c : coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
-    top back-left back-right front-left front-right bottom) →
-  coherence-htpy-parallel-cone
-    ( bottom)
-    ( refl-htpy' hD)
-    ( pair hA
-      ( pair
-        ( h' ∘ f')
-        ( rectangle-back-left-front-left-cube
-          f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom)))
-    ( pair hA
-      ( pair
-        ( k' ∘ g')
-        ( rectangle-back-right-front-right-cube
-          f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom)))
-    ( refl-htpy' hA)
-    ( top)
-coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom c =
-  ( λ a' →
-    ( ap
-      ( concat
-        ( rectangle-back-left-front-left-cube
-          f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom a')
-        ( hD (k' (g' a'))))
-      ( right-unit))) ∙h
-  ( c)
-
-rectangle-top-front-left-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  ((h ∘ hB) ∘ f') ~ ((hD ∘ k') ∘ g')
-rectangle-top-front-left-cube
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  (front-left ·r f') ∙h (hD ·l top)
-
-rectangle-back-right-bottom-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  ((h ∘ f) ∘ hA) ~ ((k ∘ hC) ∘ g')
-rectangle-back-right-bottom-cube
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  ( bottom ·r hA) ∙h (k ·l back-right)
-
-{-
-coherence-htpy-square-rectangle-top-fl-rectangle-br-bot-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g))
-  (c : coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
-    top back-left back-right front-left front-right bottom) →
-  coherence-htpy-square
-    ( inv-htpy front-right)
-    ( refl-htpy' h)
-    ( pair g' (pair (hB ∘ f')
-      ( inv-htpy (rectangle-top-front-left-cube f g h k f' g' h' k' hA hB hC hD
-        top back-left back-right front-left front-right bottom))))
-    ( pair g' (pair (f ∘ hA)
-      ( inv-htpy
-        ( rectangle-back-right-bottom-cube f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom))))
-    ( refl-htpy' g')
-    ( inv-htpy back-left)
-coherence-htpy-square-rectangle-top-fl-rectangle-br-bot-cube = {!!}
--}
-
-rectangle-top-front-right-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  ((hD ∘ h') ∘ f') ~ ((k ∘ hC) ∘ g')
-rectangle-top-front-right-cube
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  (hD ·l top) ∙h (inv-htpy (front-right) ·r g')
-
-rectangle-back-left-bottom-cube :
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
-  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
-  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
-  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
-  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
-  ((h ∘ hB) ∘ f') ~ ((k ∘ g) ∘ hA)
-rectangle-back-left-bottom-cube
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom =
-  (h ·l (inv-htpy back-left)) ∙h (bottom ·r hA)
-```
diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md
index abe72f3028..10ac24fd9f 100644
--- a/src/foundation-core/identity-types.lagda.md
+++ b/src/foundation-core/identity-types.lagda.md
@@ -55,11 +55,11 @@ identifications in arbitrary types.
 | Action on identifications of dependent functions  | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) |
 | Action on identifications of functions            | [`foundation.action-on-identifications-functions`](foundation.action-on-identifications-functions.md)                     |
 | Binary transport                                  | [`foundation.binary-transport`](foundation.binary-transport.md)                                                           |
+| Commuting hexagons of identifications             | [`foundation.commuting-hexagons-of-identifications`](foundation.commuting-hexagons-of-identifications.md)                 |
 | Commuting squares of identifications              | [`foundation.commuting-squares-of-identifications`](foundation.commuting-squares-of-identifications.md)                   |
 | Dependent identifications (foundation)            | [`foundation.dependent-identifications`](foundation.dependent-identifications.md)                                         |
 | Dependent identifications (foundation-core)       | [`foundation-core.dependent-identifications`](foundation-core.dependent-identifications.md)                               |
 | The fundamental theorem of identity types         | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md)                 |
-| Hexagons of identifications                       | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md)                                     |
 | Identity systems                                  | [`foundation.identity-systems`](foundation.identity-systems.md)                                                           |
 | The identity type (foundation)                    | [`foundation.identity-types`](foundation.identity-types.md)                                                               |
 | The identity type (foundation-core)               | [`foundation-core.identity-types`](foundation-core.identity-types.md)                                                     |
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 4654e8fff8..20e65d33ce 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -44,6 +44,7 @@ open import foundation.coherently-invertible-maps public
 open import foundation.commuting-3-simplices-of-homotopies public
 open import foundation.commuting-3-simplices-of-maps public
 open import foundation.commuting-cubes-of-maps public
+open import foundation.commuting-hexagons-of-identifications public
 open import foundation.commuting-squares-of-identifications public
 open import foundation.commuting-squares-of-maps public
 open import foundation.commuting-triangles-of-homotopies public
@@ -136,7 +137,6 @@ open import foundation.functoriality-set-truncation public
 open import foundation.functoriality-truncation public
 open import foundation.fundamental-theorem-of-identity-types public
 open import foundation.global-choice public
-open import foundation.hexagons-of-identifications public
 open import foundation.hilberts-epsilon-operators public
 open import foundation.homotopies public
 open import foundation.homotopy-induction public
diff --git a/src/foundation/commuting-cubes-of-maps.lagda.md b/src/foundation/commuting-cubes-of-maps.lagda.md
index 3643bdd449..0d236aab08 100644
--- a/src/foundation/commuting-cubes-of-maps.lagda.md
+++ b/src/foundation/commuting-cubes-of-maps.lagda.md
@@ -2,81 +2,373 @@
 
 ```agda
 module foundation.commuting-cubes-of-maps where
-
-open import foundation-core.commuting-cubes-of-maps public
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-hexagons-of-identifications
+open import foundation.commuting-squares-of-maps
 open import foundation.cones-over-cospans
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.function-types
 open import foundation-core.homotopies
+open import foundation-core.identity-types
 open import foundation-core.whiskering-homotopies
 ```
 
 </details>
 
-## Properties
+## Idea
 
-### Any coherence of commuting cubes induces a coherence of parallel cones
+We specify the type of the homotopy witnessing that a cube commutes. Imagine
+that the cube is presented as a lattice
+
+```text
+            *
+          / | \
+         /  |  \
+        /   |   \
+       *    *    *
+       |\ /   \ /|
+       | \     ‌/ |
+       |/ \   / \|
+       *    *    *
+        \   |   /
+         \  |  /
+          \ | /
+            *
+```
+
+with all maps pointing in the downwards direction. Presented in this way, a cube
+of maps has a top face, a back-left face, a back-right face, a front-left face,
+a front-right face, and a bottom face, all of which are homotopies. An element
+of type `coherence-cube-maps` is a homotopy filling the cube.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
+  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
+  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
+  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
+  where
+
+  coherence-cube-maps :
+    (top : (h' ∘ f') ~ (k' ∘ g'))
+    (back-left : (f ∘ hA) ~ (hB ∘ f'))
+    (back-right : (g ∘ hA) ~ (hC ∘ g'))
+    (front-left : (h ∘ hB) ~ (hD ∘ h'))
+    (front-right : (k ∘ hC) ~ (hD ∘ k'))
+    (bottom : (h ∘ f) ~ (k ∘ g)) →
+    UU (l4 ⊔ l1')
+  coherence-cube-maps top back-left back-right front-left front-right bottom =
+    (a' : A') →
+    coherence-hexagon
+      ( ap h (back-left a'))
+      ( front-left (f' a'))
+      ( ap hD (top a'))
+      ( bottom (hA a'))
+      ( ap k (back-right a'))
+      ( front-right (g' a'))
+```
+
+### Symmetries of commuting cubes
+
+The symmetry group D₃ acts on a cube. However, the coherence filling a cube
+needs to be modified to show that the rotated/reflected cube again commutes. In
+the following definitions we provide the homotopies witnessing that the
+rotated/reflected cubes again commute.
+
+Note: although in principle it ought to be enough to show this for the
+generators of the symmetry group D₃, in practice it is more straightforward to
+just do the work for each of the symmetries separately. One reason is that some
+of the homotopies witnessing that the faces commute will be inverted as the
+result of an application of a symmetry. Inverting a homotopy twice results in a
+new homotopy that is only homotopic to the original homotopy.
 
 ```agda
-coherence-htpy-parallel-cone-coherence-cube-maps :
+module _
   {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
   {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
   (f : A → B) (g : A → C) (h : B → D) (k : C → D)
   {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
   (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
   (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
-  (top : (h' ∘ f') ~ (k' ∘ g'))
-  (back-left : (f ∘ hA) ~ (hB ∘ f'))
-  (back-right : (g ∘ hA) ~ (hC ∘ g'))
-  (front-left : (h ∘ hB) ~ (hD ∘ h'))
-  (front-right : (k ∘ hC) ~ (hD ∘ k'))
-  (bottom : (h ∘ f) ~ (k ∘ g)) →
+  (top : coherence-square-maps g' f' k' h')
+  (back-left : coherence-square-maps f' hA hB f)
+  (back-right : coherence-square-maps g' hA hC g)
+  (front-left : coherence-square-maps h' hB hD h)
+  (front-right : coherence-square-maps k' hC hD k)
+  (bottom : coherence-square-maps g f k h)
   (c :
-    coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
-    top back-left back-right front-left front-right bottom) →
-  coherence-htpy-parallel-cone
-    ( front-left)
-    ( refl-htpy' k)
-    ( pair f'
-      ( pair
-        ( g ∘ hA)
+    coherence-cube-maps
+      f g h k f' g' h' k' hA hB hC hD
+      top back-left back-right front-left front-right bottom)
+  where
+
+  coherence-cube-maps-rotate-120 :
+    coherence-cube-maps hC k' k hD hA f' f hB g' g h' h
+      ( back-left)
+      ( inv-htpy back-right)
+      ( inv-htpy top)
+      ( inv-htpy bottom)
+      ( inv-htpy front-left)
+      ( front-right)
+  coherence-cube-maps-rotate-120 a' =
+    ( ap (λ t → t ∙ (ap h (back-left a')))
+      ( ap (λ t' → t' ∙ inv (bottom (hA a')))
+        ( ap-inv k (back-right a')))) ∙
+    ( ( hexagon-rotate-120
+        ( ap h (back-left a'))
+        ( front-left (f' a'))
+        ( ap hD (top a'))
+        ( bottom (hA a'))
+        ( ap k (back-right a'))
+        ( front-right (g' a'))
+        ( c a')) ∙
+      ( inv
+        ( ap (λ t → (front-right (g' a')) ∙ t)
+          ( ap (λ t' → t' ∙ inv (front-left (f' a')))
+            ( ap-inv hD (top a'))))))
+
+  coherence-cube-maps-rotate-240 :
+    coherence-cube-maps h' hB hD h g' hA hC g f' k' f k
+      ( inv-htpy back-right)
+      ( top)
+      ( inv-htpy back-left)
+      ( inv-htpy front-right)
+      ( bottom)
+      ( inv-htpy front-left)
+  coherence-cube-maps-rotate-240 a' =
+    ( ap (λ t → _ ∙ t) (ap-inv k (back-right a'))) ∙
+    ( ( hexagon-rotate-240
+        ( ap h (back-left a'))
+        ( front-left (f' a'))
+        ( ap hD (top a'))
+        ( bottom (hA a'))
+        ( ap k (back-right a'))
+        ( front-right (g' a'))
+        ( c a')) ∙
+      ( inv
+        ( ap
+          ( λ t → inv (front-left (f' a')) ∙ t)
+          ( ap (λ t' → t' ∙ _) (ap-inv h (back-left a'))))))
+
+  coherence-cube-maps-mirror-A :
+    coherence-cube-maps g f k h g' f' k' h' hA hC hB hD
+      ( inv-htpy top)
+      ( back-right)
+      ( back-left)
+      ( front-right)
+      ( front-left)
+      ( inv-htpy bottom)
+  coherence-cube-maps-mirror-A a' =
+    ( ap (λ t → _ ∙ t) (ap-inv hD (top a'))) ∙
+    ( hexagon-mirror-A
+      ( ap h (back-left a'))
+      ( front-left (f' a'))
+      ( ap hD (top a'))
+      ( bottom (hA a'))
+      ( ap k (back-right a'))
+      ( front-right (g' a'))
+      ( c a'))
+
+  coherence-cube-maps-mirror-B :
+    coherence-cube-maps hB h' h hD hA g' g hC f' f k' k
+      ( back-right)
+      ( inv-htpy back-left)
+      ( top)
+      ( bottom)
+      ( inv-htpy front-right)
+      ( front-left)
+  coherence-cube-maps-mirror-B a' =
+    ( ap (λ t → t ∙ (ap k (back-right a')))
+      ( ap (λ t → t ∙ _) (ap-inv h (back-left a')))) ∙
+    ( hexagon-mirror-B
+      ( ap h (back-left a'))
+      ( front-left (f' a'))
+      ( ap hD (top a'))
+      ( bottom (hA a'))
+      ( ap k (back-right a'))
+      ( front-right (g' a'))
+      ( c a'))
+
+  coherence-cube-maps-mirror-C :
+    coherence-cube-maps k' hC hD k f' hA hB f g' h' g h
+      ( inv-htpy back-left)
+      ( inv-htpy top)
+      ( inv-htpy back-right)
+      ( inv-htpy front-left)
+      ( inv-htpy bottom)
+      ( inv-htpy front-right)
+  coherence-cube-maps-mirror-C a' =
+    ( ap
+      ( λ t → (t ∙ inv (front-left (f' a'))) ∙ (ap h (inv (back-left a'))))
+      ( ap-inv hD (top a'))) ∙
+    ( ( ap (λ t → _ ∙ t) (ap-inv h (back-left a'))) ∙
+      ( ( hexagon-mirror-C
+          ( ap h (back-left a'))
+          ( front-left (f' a'))
+          ( ap hD (top a'))
+          ( bottom (hA a'))
+          ( ap k (back-right a'))
+          ( front-right (g' a'))
+          ( c a')) ∙
+        ( inv
+          ( ap
+            ( λ t → inv (front-right (g' a')) ∙ t)
+            ( ap (λ t' → t' ∙ _) (ap-inv k (back-right a')))))))
+```
+
+### Rectangles in commuting cubes
+
+```agda
+module _
+  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
+  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
+  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
+  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
+  (top : coherence-square-maps g' f' k' h')
+  (back-left : coherence-square-maps f' hA hB f)
+  (back-right : coherence-square-maps g' hA hC g)
+  (front-left : coherence-square-maps h' hB hD h)
+  (front-right : coherence-square-maps k' hC hD k)
+  (bottom : coherence-square-maps g f k h)
+  where
+
+  rectangle-left-cube :
+    ((h ∘ f) ∘ hA) ~ (hD ∘ (h' ∘ f'))
+  rectangle-left-cube =
+    pasting-horizontal-coherence-square-maps
+      f' h' hA hB hD f h back-left front-left
+
+  rectangle-right-cube :
+    ((k ∘ g) ∘ hA) ~ (hD ∘ (k' ∘ g'))
+  rectangle-right-cube =
+    pasting-horizontal-coherence-square-maps
+      g' k' hA hC hD g k back-right front-right
+
+  coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube :
+    (c : coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+      top back-left back-right front-left front-right bottom) →
+    coherence-htpy-parallel-cone
+      ( bottom)
+      ( refl-htpy' hD)
+      ( hA , h' ∘ f' , rectangle-left-cube)
+      ( hA , k' ∘ g' , rectangle-right-cube)
+      ( refl-htpy' hA)
+      ( top)
+  coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube c =
+    ( λ a' →
+      ( ap
+        ( concat
+          ( rectangle-left-cube a')
+          ( hD (k' (g' a'))))
+        ( right-unit))) ∙h
+    ( c)
+
+  rectangle-top-front-left-cube :
+    ((h ∘ hB) ∘ f') ~ ((hD ∘ k') ∘ g')
+  rectangle-top-front-left-cube =
+    ( front-left ·r f') ∙h (hD ·l top)
+
+  rectangle-back-right-bottom-cube :
+    ((h ∘ f) ∘ hA) ~ ((k ∘ hC) ∘ g')
+  rectangle-back-right-bottom-cube =
+    ( bottom ·r hA) ∙h (k ·l back-right)
+
+  rectangle-top-front-right-cube :
+    ((hD ∘ h') ∘ f') ~ ((k ∘ hC) ∘ g')
+  rectangle-top-front-right-cube =
+    (hD ·l top) ∙h (inv-htpy (front-right) ·r g')
+
+  rectangle-back-left-bottom-cube :
+    ((h ∘ hB) ∘ f') ~ ((k ∘ g) ∘ hA)
+  rectangle-back-left-bottom-cube =
+    (h ·l (inv-htpy back-left)) ∙h (bottom ·r hA)
+```
+
+In analogy to the coherence
+`coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube` we also
+expect to be able to construct a coherence
+
+```text
+  coherence-htpy-parallel-cone-rectangle-top-fl-rectangle-br-bot-cube :
+    (c : coherence-cube-maps f g h k f' g' h' k' hA hB hC hD
+      top back-left back-right front-left front-right bottom) →
+    coherence-htpy-parallel-cone
+      ( inv-htpy front-right)
+      ( refl-htpy' h)
+      ( g' , hB ∘ f' , inv-htpy (rectangle-top-front-left-cube))
+      ( g' , f ∘ hA , inv-htpy (rectangle-back-right-bottom-cube))
+      ( refl-htpy' g')
+      ( inv-htpy back-left)
+```
+
+### Any coherence of commuting cubes induces a coherence of parallel cones
+
+```agda
+module _
+  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
+  {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
+  (f : A → B) (g : A → C) (h : B → D) (k : C → D)
+  {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'}
+  (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D')
+  (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D)
+  (top : coherence-square-maps g' f' k' h')
+  (back-left : coherence-square-maps f' hA hB f)
+  (back-right : coherence-square-maps g' hA hC g)
+  (front-left : coherence-square-maps h' hB hD h)
+  (front-right : coherence-square-maps k' hC hD k)
+  (bottom : coherence-square-maps g f k h)
+  where
+
+  coherence-htpy-parallel-cone-coherence-cube-maps :
+    ( c :
+      coherence-cube-maps
+        f g h k f' g' h' k' hA hB hC hD
+        top back-left back-right front-left front-right bottom) →
+    coherence-htpy-parallel-cone
+      ( front-left)
+      ( refl-htpy' k)
+      ( ( f') ,
+        ( g ∘ hA) ,
         ( rectangle-back-left-bottom-cube
           f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom)))
-    ( pair f'
-      ( pair
-        ( hC ∘ g')
+          top back-left back-right front-left front-right bottom))
+      ( ( f') ,
+        ( hC ∘ g') ,
         ( rectangle-top-front-right-cube
           f g h k f' g' h' k' hA hB hC hD
-          top back-left back-right front-left front-right bottom)))
-    ( refl-htpy' f')
-    ( back-right)
-coherence-htpy-parallel-cone-coherence-cube-maps
-  f g h k f' g' h' k' hA hB hC hD
-  top back-left back-right front-left front-right bottom c =
-  ( assoc-htpy
-    ( h ·l (inv-htpy back-left))
-    ( bottom ·r hA)
-    ( (k ·l back-right) ∙h (refl-htpy' (k ∘ (hC ∘ g'))))) ∙h
-  ( ( ap-concat-htpy'
+          top back-left back-right front-left front-right bottom))
+      ( refl-htpy' f')
+      ( back-right)
+  coherence-htpy-parallel-cone-coherence-cube-maps c =
+    ( assoc-htpy
       ( h ·l (inv-htpy back-left))
-      ( inv-htpy (h ·l back-left))
-      ( _)
-      ( left-whisk-inv-htpy h back-left)) ∙h
-    ( inv-htpy-left-transpose-htpy-concat (h ·l back-left) _ _
-      ( ( (inv-htpy-assoc-htpy (h ·l back-left) (front-left ·r f') _) ∙h
-          ( ( inv-htpy-assoc-htpy
-              ( (h ·l back-left) ∙h (front-left ·r f'))
-              ( hD ·l top)
-              ( (inv-htpy front-right) ·r g')) ∙h
-            ( inv-htpy-right-transpose-htpy-concat _ (front-right ·r g') _
-              ( (assoc-htpy (bottom ·r hA) _ _) ∙h (inv-htpy c))))) ∙h
-        ( ap-concat-htpy (bottom ·r hA) _ _ inv-htpy-right-unit-htpy))))
+      ( bottom ·r hA)
+      ( (k ·l back-right) ∙h (refl-htpy' (k ∘ (hC ∘ g'))))) ∙h
+    ( ( ap-concat-htpy'
+        ( h ·l (inv-htpy back-left))
+        ( inv-htpy (h ·l back-left))
+        ( _)
+        ( left-whisk-inv-htpy h back-left)) ∙h
+      ( inv-htpy-left-transpose-htpy-concat (h ·l back-left) _ _
+        ( ( (inv-htpy-assoc-htpy (h ·l back-left) (front-left ·r f') _) ∙h
+            ( ( inv-htpy-assoc-htpy
+                ( (h ·l back-left) ∙h (front-left ·r f'))
+                ( hD ·l top)
+                ( (inv-htpy front-right) ·r g')) ∙h
+              ( inv-htpy-right-transpose-htpy-concat _ (front-right ·r g') _
+                ( (assoc-htpy (bottom ·r hA) _ _) ∙h (inv-htpy c))))) ∙h
+          ( ap-concat-htpy (bottom ·r hA) _ _ inv-htpy-right-unit-htpy))))
 ```
diff --git a/src/foundation/hexagons-of-identifications.lagda.md b/src/foundation/commuting-hexagons-of-identifications.lagda.md
similarity index 95%
rename from src/foundation/hexagons-of-identifications.lagda.md
rename to src/foundation/commuting-hexagons-of-identifications.lagda.md
index 3f5290432c..d7b0dc191f 100644
--- a/src/foundation/hexagons-of-identifications.lagda.md
+++ b/src/foundation/commuting-hexagons-of-identifications.lagda.md
@@ -1,7 +1,7 @@
-# Hexagons of identifications
+# Commuting hexagons of identifications
 
 ```agda
-module foundation.hexagons-of-identifications where
+module foundation.commuting-hexagons-of-identifications where
 ```
 
 <details><summary>Imports</summary>
diff --git a/src/foundation/cones-over-cospans.lagda.md b/src/foundation/cones-over-cospans.lagda.md
index d509e11b5c..8ba8badbec 100644
--- a/src/foundation/cones-over-cospans.lagda.md
+++ b/src/foundation/cones-over-cospans.lagda.md
@@ -100,8 +100,8 @@ cone-family {C = C} PX {f = f} {g} f' g' c PC =
 Next we characterize the identity type of the type of cones with a given vertex
 C. Note that in the definition of htpy-cone we do not use pattern matching on
 the cones c and c'. This is to ensure that the type htpy-cone f g c c' is a
-Σ-type for any c and c', not just for c and c' of the form (pair p (pair q H))
-and (pair p' (pair q' H')) respectively.
+Σ-type for any c and c', not just for c and c' of the form (p , q , H) and (p' ,
+q' , H') respectively.
 
 ```agda
 module _
@@ -137,16 +137,16 @@ module _
     is-contr-total-Eq-structure
       ( λ p qH K →
         Σ ( horizontal-map-cone f g c ~ pr1 qH)
-          ( coherence-htpy-cone c (pair p qH) K))
+          ( coherence-htpy-cone c (p , qH) K))
       ( is-contr-total-htpy (vertical-map-cone f g c))
-      ( pair (vertical-map-cone f g c) refl-htpy)
+      ( vertical-map-cone f g c , refl-htpy)
       ( is-contr-total-Eq-structure
         ( λ q H →
           coherence-htpy-cone c
-            ( pair (vertical-map-cone f g c) (pair q H))
+            ( vertical-map-cone f g c , q , H)
             ( refl-htpy))
         ( is-contr-total-htpy (horizontal-map-cone f g c))
-        ( pair (horizontal-map-cone f g c) refl-htpy)
+        ( horizontal-map-cone f g c , refl-htpy)
         ( is-contr-total-htpy (coherence-square-cone f g c ∙h refl-htpy)))
 
   is-equiv-htpy-eq-cone : (c c' : cone f g C) → is-equiv (htpy-eq-cone c c')
@@ -188,10 +188,10 @@ module _
 
   pasting-horizontal-cone :
     (c : cone j h B) → cone i (vertical-map-cone j h c) A → cone (j ∘ i) h A
-  pr1 (pasting-horizontal-cone c (pair f (pair p H))) = f
-  pr1 (pr2 (pasting-horizontal-cone c (pair f (pair p H)))) =
+  pr1 (pasting-horizontal-cone c (f , p , H)) = f
+  pr1 (pr2 (pasting-horizontal-cone c (f , p , H))) =
     (horizontal-map-cone j h c) ∘ p
-  pr2 (pr2 (pasting-horizontal-cone c (pair f (pair p H)))) =
+  pr2 (pr2 (pasting-horizontal-cone c (f , p , H))) =
     pasting-horizontal-coherence-square-maps p
       ( horizontal-map-cone j h c)
       ( f)
@@ -214,10 +214,10 @@ module _
 
   pasting-vertical-cone :
     (c : cone f g B) → cone (horizontal-map-cone f g c) h A → cone f (g ∘ h) A
-  pr1 (pasting-vertical-cone c (pair p' (pair q' H'))) =
+  pr1 (pasting-vertical-cone c (p' , q' , H')) =
     ( vertical-map-cone f g c) ∘ p'
-  pr1 (pr2 (pasting-vertical-cone c (pair p' (pair q' H')))) = q'
-  pr2 (pr2 (pasting-vertical-cone c (pair p' (pair q' H')))) =
+  pr1 (pr2 (pasting-vertical-cone c (p' , q' , H'))) = q'
+  pr2 (pr2 (pasting-vertical-cone c (p' , q' , H'))) =
     pasting-vertical-coherence-square-maps q' p' h
       ( horizontal-map-cone f g c)
       ( vertical-map-cone f g c)
diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md
index 08c1deac5e..31442cd1fe 100644
--- a/src/foundation/identity-types.lagda.md
+++ b/src/foundation/identity-types.lagda.md
@@ -43,11 +43,11 @@ identifications in arbitrary types.
 | Action on identifications of dependent functions  | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) |
 | Action on identifications of functions            | [`foundation.action-on-identifications-functions`](foundation.action-on-identifications-functions.md)                     |
 | Binary transport                                  | [`foundation.binary-transport`](foundation.binary-transport.md)                                                           |
+| Commuting hexagons of identifications             | [`foundation.commuting-hexagons-of-identifications`](foundation.commuting-hexagons-of-identifications.md)                 |
 | Commuting squares of identifications              | [`foundation.commuting-squares-of-identifications`](foundation.commuting-squares-of-identifications.md)                   |
 | Dependent identifications (foundation)            | [`foundation.dependent-identifications`](foundation.dependent-identifications.md)                                         |
 | Dependent identifications (foundation-core)       | [`foundation-core.dependent-identifications`](foundation-core.dependent-identifications.md)                               |
 | The fundamental theorem of identity types         | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md)                 |
-| Hexagons of identifications                       | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md)                                     |
 | Identity systems                                  | [`foundation.identity-systems`](foundation.identity-systems.md)                                                           |
 | The identity type (foundation)                    | [`foundation.identity-types`](foundation.identity-types.md)                                                               |
 | The identity type (foundation-core)               | [`foundation-core.identity-types`](foundation-core.identity-types.md)                                                     |
diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
index 0c2b9a0953..500327e68c 100644
--- a/src/foundation/pullbacks.lagda.md
+++ b/src/foundation/pullbacks.lagda.md
@@ -731,17 +731,17 @@ is-pullback-back-left-is-pullback-back-right-cube
       -- ( hD)
       ( refl-htpy)
       { c = pair hA (pair (h' ∘ f')
-        ( rectangle-back-left-front-left-cube
+        ( rectangle-left-cube
           f g h k f' g' h' k' hA hB hC hD
           top back-left back-right front-left front-right bottom))}
       ( pair hA (pair (k' ∘ g')
-        ( rectangle-back-right-front-right-cube
+        ( rectangle-right-cube
           f g h k f' g' h' k' hA hB hC hD
           top back-left back-right front-left front-right bottom)))
       ( pair
         ( refl-htpy)
         ( pair top
-          ( coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube
+          ( coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube
             f g h k f' g' h' k' hA hB hC hD
             top back-left back-right front-left front-right bottom c)))
       ( is-pullback-rectangle-is-pullback-left-square g k hD
@@ -778,24 +778,22 @@ is-pullback-back-right-is-pullback-back-left-cube
     ( pair hA (pair g' back-right))
     ( is-pb-front-right)
     ( is-pullback-htpy'
-      -- ( h ∘ f)
       { f' = k ∘ g}
       ( bottom)
-      -- ( hD)
       { g' = hD}
       ( refl-htpy)
       ( pair hA (pair (h' ∘ f')
-        ( rectangle-back-left-front-left-cube
+        ( rectangle-left-cube
           f g h k f' g' h' k' hA hB hC hD
           top back-left back-right front-left front-right bottom)))
       { c' = pair hA (pair (k' ∘ g')
-        ( rectangle-back-right-front-right-cube
+        ( rectangle-right-cube
           f g h k f' g' h' k' hA hB hC hD
           top back-left back-right front-left front-right bottom))}
       ( pair
         ( refl-htpy)
         ( pair top
-          ( coherence-htpy-square-rectangle-bl-fl-rectangle-br-fr-cube
+          ( coherence-htpy-parallel-cone-rectangle-left-rectangle-right-cube
             f g h k f' g' h' k' hA hB hC hD
             top back-left back-right front-left front-right bottom c)))
       ( is-pullback-rectangle-is-pullback-left-square f h hD