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)

Recent changes