Lifting squares

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

Created on 2023-02-18.
Last modified on 2023-09-12.

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)

Recent changes