# Lifting squares

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

Created on 2023-02-18.

module orthogonal-factorization-systems.lifting-squares where

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-3-simplices-of-homotopies
open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-homotopies
open import foundation.dependent-pair-types
open import foundation.fibered-maps
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.path-algebra
open import foundation.universe-levels
open import foundation.whiskering-homotopies

open import orthogonal-factorization-systems.extensions-of-maps
open import orthogonal-factorization-systems.lifts-of-maps


## Idea

A lifting square is a commuting square

       h
A ------> B
|         |
f|         |g
|         |
V         V
X ------> Y
i


together with a diagonal map j : X → B such that the complete diagram

       h
A ------> B
|       ^ |
f|   j  /  |g
|    /    |
V  /      V
X ------> Y
i


commutes. This we phrase as j being a simultaneous extension of h along f and lift of i along g, satisfying a higher coherence with the original commutativity proof.

## Definition

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

is-lifting-square : (j : X → B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-lifting-square j =
Σ ( is-extension f h j)
( λ E → Σ (is-lift g i j) (λ L → (L ·r f) ~ (H ∙h (g ·l E))))

lifting-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
lifting-square = Σ (X → B) (is-lifting-square)

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

map-diagonal-lifting-square : lifting-square h f g i H → (X → B)
map-diagonal-lifting-square = pr1

is-extension-is-lifting-square :
{j : X → B} → is-lifting-square h f g i H j → is-extension f h j
is-extension-is-lifting-square = pr1

is-extension-lifting-square :
(l : lifting-square h f g i H) →
is-extension f h (map-diagonal-lifting-square l)
is-extension-lifting-square = pr1 ∘ pr2

extension-lifting-square : lifting-square h f g i H → extension f h
pr1 (extension-lifting-square L) = map-diagonal-lifting-square L
pr2 (extension-lifting-square L) = is-extension-lifting-square L

is-lift-is-lifting-square :
{j : X → B} → is-lifting-square h f g i H j → is-lift g i j
is-lift-is-lifting-square = pr1 ∘ pr2

is-lift-lifting-square :
(l : lifting-square h f g i H) →
is-lift g i (map-diagonal-lifting-square l)
is-lift-lifting-square = pr1 ∘ (pr2 ∘ pr2)

lift-lifting-square : lifting-square h f g i H → lift g i
pr1 (lift-lifting-square L) = map-diagonal-lifting-square L
pr2 (lift-lifting-square L) = is-lift-lifting-square L

coherence-is-lifting-square :
{j : X → B} → (l : is-lifting-square h f g i H j) →
( is-lift-is-lifting-square l ·r f) ~
( H ∙h (g ·l is-extension-is-lifting-square l))
coherence-is-lifting-square = pr2 ∘ pr2

coherence-lifting-square :
(l : lifting-square h f g i H) →
(is-lift-lifting-square l ·r f) ~
(H ∙h (g ·l is-extension-lifting-square l))
coherence-lifting-square = pr2 ∘ (pr2 ∘ pr2)


## Properties

### Characterization of identifications of lifting squares

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

coherence-htpy-lifting-square :
(l l' : lifting-square h f g i H)
(K :
( map-diagonal-lifting-square l) ~
( map-diagonal-lifting-square l'))
(E :
( is-extension-lifting-square l') ~
( is-extension-lifting-square l ∙h (K ·r f)))
(L :
( is-lift-lifting-square l') ~
( is-lift-lifting-square l ∙h (g ·l K))) →
UU (l1 ⊔ l4)
coherence-htpy-lifting-square l l' K E L =
coherence-3-simplex-homotopies
( is-lift-lifting-square l ·r f)
( H)
( g ·l (K ·r f))
( g ·l is-extension-lifting-square l')
( g ·l is-extension-lifting-square l)
( is-lift-lifting-square l' ·r f)
( coherence-lifting-square l)
( left-whisk-coherence-triangle-homotopies (K ·r f) g E)
( right-whisk-coherence-triangle-homotopies (g ·l K) L f)
( coherence-lifting-square l')

htpy-lifting-square :
(l l' : lifting-square h f g i H) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
htpy-lifting-square l l' =
Σ ( ( map-diagonal-lifting-square l) ~
( map-diagonal-lifting-square l'))
( λ K →
Σ ( ( is-extension-lifting-square l') ~
( is-extension-lifting-square l ∙h (K ·r f)))
( λ E →
Σ ( ( is-lift-lifting-square l') ~
( is-lift-lifting-square l ∙h (g ·l K)))
( coherence-htpy-lifting-square l l' K E)))

refl-htpy-lifting-square :
(l : lifting-square h f g i H) → htpy-lifting-square l l
pr1 (refl-htpy-lifting-square l) = refl-htpy
pr1 (pr2 (refl-htpy-lifting-square l)) = inv-htpy-right-unit-htpy
pr1 (pr2 (pr2 (refl-htpy-lifting-square l))) = inv-htpy-right-unit-htpy
pr2 (pr2 (pr2 (refl-htpy-lifting-square l))) x =
( inv (assoc (inv right-unit) (β) (α))) ∙
( ( ap
( _∙ α)
( ( ap
( inv right-unit ∙_)
( ap-refl-concat (coherence-lifting-square l x))) ∙
( is-section-left-concat-inv
( right-unit)
( coherence-lifting-square l x ∙ inv right-unit)))) ∙
( ( assoc (coherence-lifting-square l x) (inv right-unit) (α)) ∙
( ( ap
( coherence-lifting-square l x ∙_)
( ( ap
( inv right-unit ∙_)
( right-unit-law-assoc
( H x)
( ap g (is-extension-lifting-square l x)))) ∙
( ( is-section-left-concat-inv
( right-unit)
( ap (H x ∙_) (inv right-unit))) ∙
( inv
( is-section-right-concat-inv
( ap (H x ∙_) (inv right-unit))
( α)))))) ∙
( ( inv
( assoc
( coherence-lifting-square l x)
( ap (H x ∙_) (inv right-unit) ∙ inv α)
( α))) ∙
( ap
( λ r →
( coherence-lifting-square l x ∙ (ap (H x ∙_) r ∙ inv α)) ∙ α)
( ap-concat-eq-inv-right-unit
( g)
( is-extension-lifting-square l x)))))))
where
α = assoc (H x) (ap g (is-extension-lifting-square l x)) refl
β = ap (_∙ refl) (coherence-lifting-square l x)

htpy-eq-lifting-square :
(l l' : lifting-square h f g i H) → l ＝ l' → htpy-lifting-square l l'
htpy-eq-lifting-square l .l refl = refl-htpy-lifting-square l


It remains to show that coherence-htpy-lifting-square indeed is a characterization of identifications of lifting squares.

### Diagonal maps give lifting squares

The diagram

  A         B
|       ^ |
f|   j  /  |g
|    /    |
V  /      V
X         Y


gives rise to a lifting square

     j ∘ f
A ------> B
|       ^ |
f|   j  /  |g
|    /    |
V  /      V
X ------> Y
g ∘ j

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → X) (g : B → Y)
where

is-lifting-square-diagonal :
(j : X → B) → is-lifting-square (j ∘ f) f g (g ∘ j) refl-htpy j
pr1 (is-lifting-square-diagonal j) = refl-htpy
pr1 (pr2 (is-lifting-square-diagonal j)) = refl-htpy
pr2 (pr2 (is-lifting-square-diagonal j)) = refl-htpy


### The lifting square associated to a fibered map

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y)
where

lifting-square-fibered-map :
(h : fibered-map f g) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
lifting-square-fibered-map h =
lifting-square
( map-total-fibered-map f g h)
( f)
( g)
( map-base-fibered-map f g h)
( is-map-over-map-total-fibered-map f g h)