Lifts of maps

module orthogonal-factorization-systems.lifts-of-maps where
Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.small-types
open import foundation.structure-identity-principle
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

Idea

A lift of a map f : X → B along a map i : A → B is a map g : X → A such that the composition i ∘ g is f.

           A
          ^|
        /  i
      g    |
    /      v
  X - f -> B

Definition

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A  B)
  where

  is-lift : {X : UU l3}  (X  B)  (X  A)  UU (l2  l3)
  is-lift f g = f ~ (i  g)

  lift : {X : UU l3}  (X  B)  UU (l1  l2  l3)
  lift {X} f = Σ (X  A) (is-lift f)

  total-lift : (X : UU l3)  UU (l1  l2  l3)
  total-lift X = Σ (X  B) lift

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A  B)
   {X : UU l3} {f : X  B}
  where

  map-lift : lift i f  X  A
  map-lift = pr1

  is-lift-map-lift : (l : lift i f)  is-lift i f (map-lift l)
  is-lift-map-lift = pr2

Operations

Vertical composition of lifts of maps

           A
          ^|
        /  i
      g    |
    /      v
  X - f -> B
    \      |
      h    j
       \   |
         v v
           C
module _
  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
  {i : A  B} {j : B  C} {f : X  B} {h : X  C} {g : X  A}
  where

  is-lift-comp-vertical : is-lift i f g  is-lift j h f  is-lift (j  i) h g
  is-lift-comp-vertical F H x = H x  ap j (F x)

Horizontal composition of lifts of maps

  A - f -> B - g -> C
    \      |      /
      h    i    j
        \  |  /
         v v v
           X
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
  {f : A  B} {g : B  C} {h : A  X} {i : B  X} {j : C  X}
  where

  is-lift-comp-horizontal :
    is-lift j i g  is-lift i h f  is-lift j h (g  f)
  is-lift-comp-horizontal J I x = I x  J (f x)

Left whiskering of lifts of maps

           A
          ^|
        /  i
      g    |
    /      v
  X - f -> B - h -> S
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {S : UU l4}
  {i : A  B} {f : X  B} {g : X  A}
  where

  is-lift-left-whisk : (h : B  S)  is-lift i f g  is-lift (h  i) (h  f) g
  is-lift-left-whisk h H x = ap h (H x)

Right whiskering of lifts of maps

                    A
                   ^|
                 /  i
               g    |
             /      v
  S - h -> X - f -> B
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {S : UU l4}
  {i : A  B} {f : X  B} {g : X  A}
  where

  is-lift-right-whisk : is-lift i f g  (h : S  X)  is-lift i (f  h) (g  h)
  is-lift-right-whisk H h s = H (h s)

Properties

Characterizing identification of lifts of maps

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A  B)
  {X : UU l3} (f : X  B)
  where

  coherence-htpy-lift :
    (l l' : lift i f)  map-lift i l ~ map-lift i l'  UU (l2  l3)
  coherence-htpy-lift l l' K =
    (is-lift-map-lift i l ∙h (i ·l K)) ~ is-lift-map-lift i l'

  htpy-lift : (l l' : lift i f)  UU (l1  l2  l3)
  htpy-lift l l' =
    Σ ( map-lift i l ~ map-lift i l')
      ( coherence-htpy-lift l l')

  refl-htpy-lift : (l : lift i f)  htpy-lift l l
  pr1 (refl-htpy-lift l) = refl-htpy
  pr2 (refl-htpy-lift l) = right-unit-htpy

  htpy-eq-lift : (l l' : lift i f)  l  l'  htpy-lift l l'
  htpy-eq-lift l .l refl = refl-htpy-lift l

  is-contr-total-htpy-lift :
    (l : lift i f)  is-contr (Σ (lift i f) (htpy-lift l))
  is-contr-total-htpy-lift l =
    is-contr-total-Eq-structure
       g G  coherence-htpy-lift l (g , G))
      (is-contr-total-htpy (map-lift i l))
      (map-lift i l , refl-htpy)
      (is-contr-total-htpy (is-lift-map-lift i l ∙h refl-htpy))

  is-equiv-htpy-eq-lift :
    (l l' : lift i f)  is-equiv (htpy-eq-lift l l')
  is-equiv-htpy-eq-lift l =
    fundamental-theorem-id (is-contr-total-htpy-lift l) (htpy-eq-lift l)

  extensionality-lift :
    (l l' : lift i f)  (l  l')  (htpy-lift l l')
  pr1 (extensionality-lift l l') = htpy-eq-lift l l'
  pr2 (extensionality-lift l l') = is-equiv-htpy-eq-lift l l'

  eq-htpy-lift : (l l' : lift i f)  htpy-lift l l'  l  l'
  eq-htpy-lift l l' = map-inv-equiv (extensionality-lift l l')

The total type of lifts of maps is equivalent to X → A

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A  B) (X : UU l3)
  where

  inv-compute-total-lift : total-lift i X  (X  A)
  inv-compute-total-lift =
    ( right-unit-law-Σ-is-contr ( λ f  is-contr-total-htpy' (i  f))) ∘e
    ( equiv-left-swap-Σ)

  compute-total-lift : (X  A)  total-lift i X
  compute-total-lift = inv-equiv inv-compute-total-lift

  is-small-total-lift : is-small (l1  l3) (total-lift i X)
  pr1 (is-small-total-lift) = X  A
  pr2 (is-small-total-lift) = inv-compute-total-lift

The truncation level of the type of lifts is bounded by the truncation level of the codomains

module _
  {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} (i : A  B)
  where

  is-trunc-is-lift :
    {X : UU l3} (f : X  B) 
    is-trunc (succ-𝕋 k) B  (g : X  A)  is-trunc k (is-lift i f g)
  is-trunc-is-lift f is-trunc-B g =
    is-trunc-Π k  x  is-trunc-B (f x) (i (g x)))

  is-trunc-lift :
    {X : UU l3} (f : X  B) 
    is-trunc k A  is-trunc (succ-𝕋 k) B  is-trunc k (lift i f)
  is-trunc-lift f is-trunc-A is-trunc-B =
    is-trunc-Σ
      ( is-trunc-function-type k is-trunc-A)
      ( is-trunc-is-lift f is-trunc-B)

  is-trunc-total-lift :
    (X : UU l3)  is-trunc k A  is-trunc k (total-lift i X)
  is-trunc-total-lift X is-trunc-A =
    is-trunc-equiv' k
      ( X  A)
      ( compute-total-lift i X)
      ( is-trunc-function-type k is-trunc-A)

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (i : A  B)
  where

  is-contr-is-lift :
    {X : UU l3} (f : X  B) 
    is-prop B  (g : X  A)  is-contr (is-lift i f g)
  is-contr-is-lift f is-prop-B g = is-contr-Π λ x  is-prop-B (f x) (i (g x))

  is-prop-is-lift :
    {X : UU l3} (f : X  B) 
    is-set B  (g : X  A)  is-prop (is-lift i f g)
  is-prop-is-lift f is-set-B g = is-prop-Π λ x  is-set-B (f x) (i (g x))

See also