# Commuting squares of pointed homotopies

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-04-25.

module structured-types.commuting-squares-of-pointed-homotopies where

Imports
open import foundation.universe-levels

open import structured-types.pointed-2-homotopies
open import structured-types.pointed-dependent-functions
open import structured-types.pointed-families-of-types
open import structured-types.pointed-homotopies
open import structured-types.pointed-types


## Idea

A square of pointed homotopies

          top
f ------> g
|         |
left |         | right
∨         ∨
h ------> i
bottom


is said to be a commuting square of pointed homotopies if there is a pointed homotopy left ∙h bottom ~∗ top ∙h right . Such a pointed homotopy is called a coherence of the square.

## Definitions

### Commuting squares of pointed homotopies

module _
{l1 l2 : Level}
{A : Pointed-Type l1} {B : Pointed-Fam l2 A} {f g h i : pointed-Π A B}
(top : f ~∗ g) (left : f ~∗ h) (right : g ~∗ i) (bottom : h ~∗ i)
where

coherence-square-pointed-homotopies : UU (l1 ⊔ l2)
coherence-square-pointed-homotopies =
pointed-2-htpy
( concat-pointed-htpy left bottom)
( concat-pointed-htpy top right)

coherence-square-pointed-homotopies' : UU (l1 ⊔ l2)
coherence-square-pointed-homotopies' =
pointed-2-htpy
( concat-pointed-htpy top right)
( concat-pointed-htpy left bottom)