Lifts of families of elements

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

Created on 2023-12-05.
Last modified on 2024-04-25.

module orthogonal-factorization-systems.lifts-families-of-elements where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.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.precomposition-type-families
open import foundation.transport-along-homotopies
open import foundation.transport-along-identifications
open import foundation.universe-levels

Idea

Consider a type family

  B : (i : I) → A i → 𝒰

and a family of elements a : (i : I) → A i.

A dependent lift of the family of elements a to the type family B is a family of elements

  (i : I) → B i (a i).

An important special case occurs when a : I → A is a family of elements of a fixed type A, and B is a type family over A. In this case, a lift of the family of elements a is a family of elements

  (i : I) → B (a i).

A family of elements equipped with a dependent lift is a dependent lifted family of elements, and analogously a family of elements equipped with a lift is a lifted family of elements.

To see how these families relate to lifts of maps, consider the lifting diagram

      Σ (x : A) (B x)
            |
            | pr1
            |
            ∨
  I ------> A         .
       a

Then a lift of the map a against pr1 is a map b : I → Σ A B, such that the triangle commutes. Invoking the type theoretic principle of choice, we can show that this type is equivalent to the type of families of elements (i : I) → B (a i):

  Σ (b : I → Σ A B) ((i : I) → a i ＝ pr1 (b i))
    ≃ (i : I) → Σ ((x , b) : Σ A B) (a i ＝ x)
    ≃ (i : I) → Σ (x : A) (a i ＝ x × B x)
    ≃ (i : I) → B (a i) .

The first equivalence is the principle of choice, the second is associativity of dependent pair types, and the third is the left unit law of dependent pair types, since Σ (x : A) (a i ＝ x) is contractible.

Definitions

Dependent lifts of families of elements

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

  dependent-lift-family-of-elements : UU (l1 ⊔ l3)
  dependent-lift-family-of-elements = (i : I) → B i (a i)

Lifts of families of elements

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

  lift-family-of-elements : UU (l1 ⊔ l3)
  lift-family-of-elements = dependent-lift-family-of-elements (λ _ → B) a

Dependent lifted families of elements

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

  dependent-lifted-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
  dependent-lifted-family-of-elements =
    Σ ( (i : I) → A i)
      ( dependent-lift-family-of-elements B)

Lifted families of elements

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

  lifted-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
  lifted-family-of-elements =
    dependent-lifted-family-of-elements (λ (_ : I) → A) (λ _ → B)

Dependent lifts of binary families of elements

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
  (C : (i : I) (x : A i) → B i x → UU l4) (a : (i : I) → A i)
  where

  dependent-lift-binary-family-of-elements : UU (l1 ⊔ l3 ⊔ l4)
  dependent-lift-binary-family-of-elements =
    dependent-lift-family-of-elements (λ i x → (y : B i x) → C i x y) a

Lifts of binary families of elements

module _
  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
  {C : (x : A) → B x → UU l4} (a : I → A)
  where

  lift-binary-family-of-elements : UU (l1 ⊔ l3 ⊔ l4)
  lift-binary-family-of-elements =
    dependent-lift-binary-family-of-elements (λ _ → C) a

Properties

Transport in lifts of families of elements along homotopies of precompositions

Given a map a : I → A, and a homotopy H : f ~ g, where f, g : J → I, we know that there is an identification a ∘ f ＝ a ∘ g. Transporting along this identification in the type of lifts of families of elements into a type family B : A → 𝓤, we get a map

  ((j : J) → B (a (f j))) → ((j : J) → B (a (g j))) .

We show that this map is homotopic to transporting along H in the type family B ∘ a : I → 𝓤.

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-tr-lift-family-of-elements-precomp :
    {g : J → I} (H : f ~ g) → UU (l3 ⊔ l4)
  statement-tr-lift-family-of-elements-precomp H =
    tr (lift-family-of-elements B) (htpy-precomp H A a) ~
    tr-htpy (λ _ → precomp-family a B) H

  tr-lift-family-of-elements-precomp-refl-htpy :
    statement-tr-lift-family-of-elements-precomp refl-htpy
  tr-lift-family-of-elements-precomp-refl-htpy b =
    ap
      ( λ p → tr (lift-family-of-elements B) p b)
      ( compute-htpy-precomp-refl-htpy f A a)

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

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

See also

Recent changes