Precomposition of lifts of families of elements by maps

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2024-01-27.
Last modified on 2024-02-06.

module orthogonal-factorization-systems.precomposition-lifts-families-of-elements where
Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.commuting-squares-of-homotopies
open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.precomposition-functions
open import foundation.transport-along-identifications
open import foundation.type-theoretic-principle-of-choice
open import foundation.universe-levels
open import foundation.whiskering-higher-homotopies-composition
open import foundation.whiskering-homotopies-composition
open import foundation.whiskering-identifications-concatenation

open import orthogonal-factorization-systems.lifts-families-of-elements

Idea

Consider a type family B : A → 𝓤 and a map a : I → A. Then, given a map f : J → I, we may pull back a lift of a to a lift of a ∘ f.

In other words, given a diagram

                Σ (x : A) (B x)
                      |
                      | pr1
                      |
                      v
  J ------> I ------> A         ,
       f         a

we get a map of lifts of families of elements

  ((i : I) → B (a i)) → ((j : J) → B (a (f j))) .

This map of lifts induces a map from lifted families of elements indexed by I to lifted families of elements indexed by J.

Definitions

Precomposition of lifts of families of elements by functions

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) {J : UU l4}
  (f : J  I)
  where

  precomp-lift-family-of-elements :
    (a : I  A) 
    lift-family-of-elements B a  lift-family-of-elements B (a  f)
  precomp-lift-family-of-elements a b i = b (f i)

Precomposition in lifted families of elements

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) {J : UU l4}
  (f : J  I)
  where

  precomp-lifted-family-of-elements :
    lifted-family-of-elements I B  lifted-family-of-elements J B
  precomp-lifted-family-of-elements =
    map-Σ
      ( lift-family-of-elements B)
      ( precomp f A)
      ( precomp-lift-family-of-elements B f)

Properties

Homotopies between maps induce commuting triangles of precompositions of lifts of families of elements

Consider two maps f, g : J → I and a homotopy H : f ~ g between them. The precomposition functions they induce on lifts of families of elements have different codomains, namely lift-family-of-elements B (a ∘ f) and lift-family-of-elements B (a ∘ g), but they fit into a commuting triangle with transport in the type of lifts:

                              precomp-lift B f a
  lift-family-of-elements B a ------------------> lift-family-of-elements B (a ∘ f)
                      \                                /
                         \                          /
                            \                    /
           precomp-lift B g a  \              / tr (lift-family-of-elements B) (htpy-precomp H A a)
                                  \        /
                                     V  V
                       lift-family-of-elements B (a ∘ g)
module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) (a : I  A)
  {J : UU l4} {f : J  I}
  where

  statement-triangle-precomp-lift-family-of-elements-htpy :
    {g : J  I} (H : f ~ g)  UU (l1  l3  l4)
  statement-triangle-precomp-lift-family-of-elements-htpy {g} H =
    coherence-triangle-maps'
      ( precomp-lift-family-of-elements B g a)
      ( tr (lift-family-of-elements B) (htpy-precomp H A a))
      ( precomp-lift-family-of-elements B f a)

  triangle-precomp-lift-family-of-elements-htpy-refl-htpy :
    statement-triangle-precomp-lift-family-of-elements-htpy refl-htpy
  triangle-precomp-lift-family-of-elements-htpy-refl-htpy b =
    tr-lift-family-of-elements-precomp B a refl-htpy (b  f)

  abstract
    triangle-precomp-lift-family-of-elements-htpy :
      {g : J  I} (H : f ~ g) 
      statement-triangle-precomp-lift-family-of-elements-htpy H
    triangle-precomp-lift-family-of-elements-htpy =
      ind-htpy f
        ( λ g  statement-triangle-precomp-lift-family-of-elements-htpy)
        ( triangle-precomp-lift-family-of-elements-htpy-refl-htpy)

    compute-triangle-precomp-lift-family-of-elements-htpy :
      triangle-precomp-lift-family-of-elements-htpy refl-htpy 
      triangle-precomp-lift-family-of-elements-htpy-refl-htpy
    compute-triangle-precomp-lift-family-of-elements-htpy =
      compute-ind-htpy f
        ( λ g  statement-triangle-precomp-lift-family-of-elements-htpy)
        ( triangle-precomp-lift-family-of-elements-htpy-refl-htpy)

triangle-precomp-lift-family-of-elements-htpy factors through transport along a homotopy in the famiy B ∘ a

Instead of defining the homotopy triangle-precomp-lift-family-of-elements-htpy by homotopy induction, we could have defined it manually using the characterization of transport in the type of lifts of a family of elements.

We show that these two definitions are homotopic.

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) (a : I  A)
  {J : UU l4} {f : J  I}
  where

  statement-coherence-triangle-precomp-lift-family-of-elements :
    {g : J  I} (H : f ~ g)  UU (l1  l3  l4)
  statement-coherence-triangle-precomp-lift-family-of-elements H =
    ( triangle-precomp-lift-family-of-elements-htpy B a H) ~
    ( ( ( tr-lift-family-of-elements-precomp B a H) ·r
        ( precomp-lift-family-of-elements B f a)) ∙h
      ( λ b  eq-htpy  j  apd b (H j))))

  coherence-triangle-precomp-lift-family-of-elements-refl-htpy :
    statement-coherence-triangle-precomp-lift-family-of-elements
      ( refl-htpy)
  coherence-triangle-precomp-lift-family-of-elements-refl-htpy b =
    ( htpy-eq (compute-triangle-precomp-lift-family-of-elements-htpy B a) b) 
    ( inv right-unit) 
    ( left-whisker-concat
      ( triangle-precomp-lift-family-of-elements-htpy-refl-htpy B a b)
      ( inv (eq-htpy-refl-htpy (b  f))))

  abstract
    coherence-triangle-precomp-lift-family-of-elements :
      {g : J  I} (H : f ~ g) 
      statement-coherence-triangle-precomp-lift-family-of-elements H
    coherence-triangle-precomp-lift-family-of-elements =
      ind-htpy f
        ( λ g 
          statement-coherence-triangle-precomp-lift-family-of-elements)
        ( coherence-triangle-precomp-lift-family-of-elements-refl-htpy)

    compute-coherence-triangle-precomp-lift-family-of-elements :
      coherence-triangle-precomp-lift-family-of-elements refl-htpy 
      coherence-triangle-precomp-lift-family-of-elements-refl-htpy
    compute-coherence-triangle-precomp-lift-family-of-elements =
      compute-ind-htpy f
        ( λ g 
          statement-coherence-triangle-precomp-lift-family-of-elements)
        ( coherence-triangle-precomp-lift-family-of-elements-refl-htpy)

precomp-lifted-family-of-elements is homotopic to the precomposition map on functions up to equivalence

We have a commuting square like this:

                                     precomp-lifted-family f
  Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j))
                  |                                                           |
                  |                                                           |
                  | map-inv-distributive-Π-Σ    ⇗    map-inv-distributive-Π-Σ |
                  |                                                           |
                  V                                                           V
              I → Σ A B ------------------------------------------------> J → Σ A B ,
                                               - ∘ f

which shows that precomp-lifted-family-of-elements f is a good choice for a precomposition map in the type of lifted families of elements, since it's homotopic to the regular precomposition map up to equivalence.

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) {J : UU l4}
  (f : J  I)
  where

  coherence-square-precomp-map-inv-distributive-Π-Σ :
    coherence-square-maps
      ( precomp-lifted-family-of-elements B f)
      ( map-inv-distributive-Π-Σ)
      ( map-inv-distributive-Π-Σ)
      ( precomp f (Σ A B))
  coherence-square-precomp-map-inv-distributive-Π-Σ = refl-htpy

Precomposition of lifted families of elements preserves homotopies

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) {J : UU l4}
  {f : J  I}
  where

  htpy-precomp-lifted-family-of-elements :
    {g : J  I} (H : f ~ g) 
    ( precomp-lifted-family-of-elements B f) ~
    ( precomp-lifted-family-of-elements B g)
  htpy-precomp-lifted-family-of-elements H =
    htpy-map-Σ
      ( lift-family-of-elements B)
      ( htpy-precomp H A)
      ( precomp-lift-family-of-elements B f)
      ( λ a  triangle-precomp-lift-family-of-elements-htpy B a H)

  abstract
    compute-htpy-precomp-lifted-family-of-elements :
      htpy-precomp-lifted-family-of-elements refl-htpy ~
      refl-htpy
    compute-htpy-precomp-lifted-family-of-elements =
      htpy-htpy-map-Σ-refl-htpy
        ( lift-family-of-elements B)
        ( compute-htpy-precomp-refl-htpy f A)
        ( λ a 
          ( htpy-eq
            ( compute-triangle-precomp-lift-family-of-elements-htpy B a)) ∙h
          ( λ b 
            htpy-eq (compute-tr-lift-family-of-elements-precomp B a) (b  f)))

coherence-square-precomp-map-inv-distributive-Π-Σ commutes with induced homotopies between precompositions maps

Diagrammatically, we have two ways of composing homotopies to connect - ∘ f and precomp-lifted-family-of-elements g. One factors through precomp-lifted-family-of-elements f:

                                     precomp-lifted-family g
                               -----------------------------------
                             /                                     \
                           /     ⇗ htpy-precomp-lifted-family H      \
                         /                                             V
  Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j))
                  |                  precomp-lifted-family f                  |
                  |                                                           |
                  |                             ⇗                             |
                  | map-inv-distributive-Π-Σ         map-inv-distributive-Π-Σ |
                  V                                                           V
              I → Σ A B ------------------------------------------------> J → Σ A B ,
                                              - ∘ f

while the other factors through - ∘ g:

                                     precomp-lifted-family g
  Σ (a : I → A) ((i : I) → B (a i)) ------------------------> Σ (a : J → A) ((j : J) → B (a j))
                  |                                                           |
                  |                                                           |
                  | map-inv-distributive-Π-Σ    ⇗    map-inv-distributive-Π-Σ |
                  |                                                           |
                  V                           - ∘ g                           V
              I → Σ A B ------------------------------------------------> J → Σ A B .
                        \                                               >
                          \             ⇗  htpy-precomp H             /
                            \                                       /
                              -------------------------------------
                                              - ∘ f

We show that these homotopies are themselves homotopic, filling the cylinder.

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (B : A  UU l3) {J : UU l4}
  {f : J  I}
  where

  statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ :
    {g : J  I} (H : f ~ g)  UU (l1  l2  l3  l4)
  statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ
    {g} H =
    coherence-square-homotopies
      ( htpy-precomp H (Σ A B) ·r map-inv-distributive-Π-Σ)
      ( coherence-square-precomp-map-inv-distributive-Π-Σ B f)
      ( coherence-square-precomp-map-inv-distributive-Π-Σ B g)
      ( ( map-inv-distributive-Π-Σ) ·l
        ( htpy-precomp-lifted-family-of-elements B H))

  coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ-refl-htpy :
    statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ
      ( refl-htpy)
  coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ-refl-htpy =
    ( left-whisker-comp²
      ( map-inv-distributive-Π-Σ)
      ( compute-htpy-precomp-lifted-family-of-elements B)) ∙h
    ( inv-htpy
      ( λ h 
        compute-htpy-precomp-refl-htpy f
          ( Σ A B)
          ( map-inv-distributive-Π-Σ h))) ∙h
    ( inv-htpy-right-unit-htpy)

  coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ :
    {g : J  I} (H : f ~ g) 
    statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ
      ( H)
  coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ =
    ind-htpy f
      ( λ g 
        statement-coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ)
      ( coherence-htpy-precomp-coherence-square-precomp-map-inv-distributive-Π-Σ-refl-htpy)

Recent changes