# Precomposition of lifts of families of elements by maps ```agda module orthogonal-factorization-systems.precomposition-lifts-families-of-elements where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## 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](orthogonal-factorization-systems.lifts-families-of-elements.md) of `a` to a lift of `a ∘ f`. In other words, given a diagram ```text Σ (x : A) (B x) | | pr1 | ∨ J ------> I ------> A , f a ``` we get a map of lifts of families of elements ```text ((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 ```agda 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 ```agda 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](foundation.commuting-triangles-of-maps.md) with [transport](foundation.transport-along-identifications.md) in the type of lifts: ```text 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) ``` ```agda 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. ```agda 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](foundation.commuting-squares-of-maps.md) like this: ```text 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. ```agda 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 ```agda 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`: ```text 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`: ```text 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. ```agda 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) ```