# 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.

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
|
∨
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)
\        /
∨  ∨
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-Π-Σ |
|                                                           |
∨                                                           ∨
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      \
/                                             ∨
Σ (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-Π-Σ |
∨                                                           ∨
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-Π-Σ |
|                                                           |
∨                           - ∘ g                           ∨
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)