# Commuting squares of maps

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-02-18.

module foundation-core.commuting-squares-of-maps where

Imports
open import foundation.action-on-identifications-functions
open import foundation.transposition-identifications-along-equivalences
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.commuting-triangles-of-maps
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


## Idea

A square of maps

            top
A --------> X
|           |
left |           | right
∨           ∨
B --------> Y
bottom


is said to be a commuting square of maps if there is a homotopy

  bottom ∘ left ~ right ∘ top.


Such a homotopy is called the coherence of the commuting square.

## Definitions

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
(top : C → B) (left : C → A) (right : B → X) (bottom : A → X)
where

coherence-square-maps : UU (l3 ⊔ l4)
coherence-square-maps = bottom ∘ left ~ right ∘ top

coherence-square-maps' : UU (l3 ⊔ l4)
coherence-square-maps' = right ∘ top ~ bottom ∘ left


## Properties

### Pasting commuting squares horizontally

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
(top-left : A → B) (top-right : B → C)
(left : A → X) (mid : B → Y) (right : C → Z)
(bottom-left : X → Y) (bottom-right : Y → Z)
where

pasting-horizontal-coherence-square-maps :
coherence-square-maps top-left left mid bottom-left →
coherence-square-maps top-right mid right bottom-right →
coherence-square-maps
(top-right ∘ top-left) left right (bottom-right ∘ bottom-left)
pasting-horizontal-coherence-square-maps sq-left sq-right =
(bottom-right ·l sq-left) ∙h (sq-right ·r top-left)

pasting-horizontal-up-to-htpy-coherence-square-maps :
{top : A → C} (H : coherence-triangle-maps top top-right top-left)
{bottom : X → Z}
(K : coherence-triangle-maps bottom bottom-right bottom-left) →
coherence-square-maps top-left left mid bottom-left →
coherence-square-maps top-right mid right bottom-right →
coherence-square-maps top left right bottom
pasting-horizontal-up-to-htpy-coherence-square-maps H K sq-left sq-right =
( ( K ·r left) ∙h
( pasting-horizontal-coherence-square-maps sq-left sq-right)) ∙h
( inv-htpy (right ·l H))


### Pasting commuting squares vertically

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
(top : A → X)
(left-top : A → B) (right-top : X → Y)
(mid : B → Y)
(left-bottom : B → C) (right-bottom : Y → Z)
(bottom : C → Z)
where

pasting-vertical-coherence-square-maps :
coherence-square-maps top left-top right-top mid →
coherence-square-maps mid left-bottom right-bottom bottom →
coherence-square-maps
top (left-bottom ∘ left-top) (right-bottom ∘ right-top) bottom
pasting-vertical-coherence-square-maps sq-top sq-bottom =
(sq-bottom ·r left-top) ∙h (right-bottom ·l sq-top)

pasting-vertical-up-to-htpy-coherence-square-maps :
{left : A → C} (H : coherence-triangle-maps left left-bottom left-top)
{right : X → Z} (K : coherence-triangle-maps right right-bottom right-top) →
coherence-square-maps top left-top right-top mid →
coherence-square-maps mid left-bottom right-bottom bottom →
coherence-square-maps top left right bottom
pasting-vertical-up-to-htpy-coherence-square-maps H K sq-top sq-bottom =
( ( bottom ·l H) ∙h
( pasting-vertical-coherence-square-maps sq-top sq-bottom)) ∙h
( inv-htpy (K ·r top))


### Associativity of horizontal pasting

Proof: Consider a commuting diagram of the form

        α₀       β₀       γ₀
A -----> X -----> U -----> K
|        |        |        |
f |   α  g |   β  h |   γ    | i
∨        ∨        ∨        ∨
B -----> Y -----> V -----> L.
α₁       β₁       γ₁


Then we can make the following calculation, in which we write □ for horizontal pasting of squares:

  (α □ β) □ γ
＝ (γ₁ ·l ((β₁ ·l α) ∙h (β ·r α₀))) ∙h (γ ·r (β₀ ∘ α₀))
＝ ((γ₁ ·l (β₁ ·l α)) ∙h (γ₁ ·l (β ·r α₀))) ∙h (γ ·r (β₀ ∘ α₀))
＝ ((γ₁ ∘ β₁) ·l α) ∙h (((γ₁ ·l β) ·r α₀) ∙h ((γ ·r β₀) ·r α₀))
＝ ((γ₁ ∘ β₁) ·l α) ∙h (((γ₁ ·l β) ∙h (γ ·r β₀)) ·r α₀)
＝ α □ (β □ γ)

module _
{l1 l2 l3 l4 l5 l6 l7 l8 : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
{K : UU l7} {L : UU l8}
(α₀ : A → X) (β₀ : X → U) (γ₀ : U → K)
(f : A → B) (g : X → Y) (h : U → V) (i : K → L)
(α₁ : B → Y) (β₁ : Y → V) (γ₁ : V → L)
(α : coherence-square-maps α₀ f g α₁)
(β : coherence-square-maps β₀ g h β₁)
(γ : coherence-square-maps γ₀ h i γ₁)
where

assoc-pasting-horizontal-coherence-square-maps :
pasting-horizontal-coherence-square-maps
( β₀ ∘ α₀)
( γ₀)
( f)
( h)
( i)
( β₁ ∘ α₁)
( γ₁)
( pasting-horizontal-coherence-square-maps α₀ β₀ f g h α₁ β₁ α β)
( γ) ~
pasting-horizontal-coherence-square-maps
( α₀)
( γ₀ ∘ β₀)
( f)
( g)
( i)
( α₁)
( γ₁ ∘ β₁)
( α)
( pasting-horizontal-coherence-square-maps β₀ γ₀ g h i β₁ γ₁ β γ)
assoc-pasting-horizontal-coherence-square-maps a =
( ap
( _∙ _)
( ( ap-concat γ₁ (ap β₁ (α a)) (β (α₀ a))) ∙
( inv (ap (_∙ _) (ap-comp γ₁ β₁ (α a)))))) ∙
( assoc (ap (γ₁ ∘ β₁) (α a)) (ap γ₁ (β (α₀ a))) (γ (β₀ (α₀ a))))


### The unit laws for horizontal pasting of commuting squares of maps

#### The left unit law

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(i : A → X) (f : A → B) (g : X → Y) (j : B → Y)
(α : coherence-square-maps i f g j)
where

left-unit-law-pasting-horizontal-coherence-square-maps :
pasting-horizontal-coherence-square-maps id i f f g id j refl-htpy α ~ α
left-unit-law-pasting-horizontal-coherence-square-maps = refl-htpy


### The right unit law

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(i : A → X) (f : A → B) (g : X → Y) (j : B → Y)
(α : coherence-square-maps i f g j)
where

right-unit-law-pasting-horizontal-coherence-square-maps :
pasting-horizontal-coherence-square-maps i id f g g j id α refl-htpy ~ α
right-unit-law-pasting-horizontal-coherence-square-maps a =
right-unit ∙ ap-id (α a)


### Inverting squares horizontally and vertically

If the horizontal/vertical maps in a commuting square are both equivalences, then the square remains commuting if we invert those equivalences.

horizontal-inv-equiv-coherence-square-maps :
{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) →
coherence-square-maps (map-equiv top) left right (map-equiv bottom) →
coherence-square-maps (map-inv-equiv top) right left (map-inv-equiv bottom)
horizontal-inv-equiv-coherence-square-maps top left right bottom H b =
map-eq-transpose-equiv-inv
( bottom)
( ( ap right (inv (is-section-map-inv-equiv top b))) ∙
( inv (H (map-inv-equiv top b))))

vertical-inv-equiv-coherence-square-maps :
{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) →
coherence-square-maps top (map-equiv left) (map-equiv right) bottom →
coherence-square-maps bottom (map-inv-equiv left) (map-inv-equiv right) top
vertical-inv-equiv-coherence-square-maps top left right bottom H x =
map-eq-transpose-equiv
( right)
( ( inv (H (map-inv-equiv left x))) ∙
( ap bottom (is-section-map-inv-equiv left x)))

coherence-square-maps-inv-equiv :
{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) →
coherence-square-maps
( map-equiv top)
( map-equiv left)
( map-equiv right)
( map-equiv bottom) →
coherence-square-maps
( map-inv-equiv bottom)
( map-inv-equiv right)
( map-inv-equiv left)
( map-inv-equiv top)
coherence-square-maps-inv-equiv top left right bottom H =
vertical-inv-equiv-coherence-square-maps
( map-inv-equiv top)
( right)
( left)
( map-inv-equiv bottom)
( horizontal-inv-equiv-coherence-square-maps
( top)
( map-equiv left)
( map-equiv right)
( bottom)
( H))