# Commuting tetrahedra of maps

```agda
module foundation.commuting-tetrahedra-of-maps where
```

<details><summary>Imports</summary>

```agda
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-triangles-of-maps
open import foundation-core.homotopies
```

</details>

## Idea

A {{#concept "commuting tetrahedron of maps" Agda=coherence-tetrahedron-maps}}
is a commuting diagram of the form

```text
  A ----------> B
  |  \       ∧  |
  |    \   /    |
  |      /      |
  |    /   \    |
  ∨  /       ∨  ∨
  X ----------> Y.
```

## Definition

```agda
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  (top : A → B) (left : A → X) (right : B → Y) (bottom : X → Y)
  (diagonal-up : X → B) (diagonal-down : A → Y)
  (upper-left : coherence-triangle-maps top diagonal-up left)
  (lower-right : coherence-triangle-maps bottom right diagonal-up)
  (upper-right : coherence-triangle-maps diagonal-down right top)
  (lower-left : coherence-triangle-maps diagonal-down bottom left)
  where

  coherence-tetrahedron-maps : UU (l1 ⊔ l4)
  coherence-tetrahedron-maps =
    ( upper-right ∙h (right ·l upper-left)) ~
    ( lower-left ∙h (lower-right ·r left))

  coherence-tetrahedron-maps' : UU (l1 ⊔ l4)
  coherence-tetrahedron-maps' =
    ( lower-left ∙h (lower-right ·r left)) ~
    ( upper-right ∙h (right ·l upper-left))
```