Extensions of double lifts of families of elements

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

Created on 2023-12-05.
Last modified on 2024-01-28.

module
  orthogonal-factorization-systems.extensions-double-lifts-families-of-elements
  where

Imports

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types

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

Idea

Consider a dependent lift b : (i : I) → B i (a i) of a family of elements a : I → A, a type family C over B and a double lift

  c : (i : I) → C i (a i) (b i)

of the lift b of a. An extension^¶ of b to A consists of a family of elements f : (i : I) (x : A i) (y : B i x) → C i x y equipped with a homotopy witnessing that the identification f i (a i) (b i) ＝ c i holds for every i : I.

Extensions of dependent double lifts play a role in the universal property of the family of fibers of a map

Definitions

Evaluating families of elements at dependent double lifts of families of elements

Any family of elements b : (i : I) → B i (a i) dependent over a family of elements a : (i : I) → A i induces an evaluation map

  ((i : I) (x : A i) (y : B i x) → C i x y) → ((i : I) → C i (a i) (b i))

given by c ↦ (λ i → c i (a i) (b i)).

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} (b : dependent-lift-family-of-elements B a)
  where

  ev-dependent-double-lift-family-of-elements :
    ((i : I) (x : A i) (y : B i x) → C i x y) →
    dependent-double-lift-family-of-elements C b
  ev-dependent-double-lift-family-of-elements h i = h i (a i) (b i)

Evaluating families of elements at double lifts of families of elements

Any family of elements b : (i : I) → B (a i) dependent over a family of elements a : I → A induces an evaluation map

  ((x : A) (y : B x) → C x y) → ((i : I) → C (a i) (b i))

given by c ↦ (λ i → c (a i) (b i)).

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} (b : lift-family-of-elements B a)
  where

  ev-double-lift-family-of-elements :
    ((x : A) (y : B x) → C x y) → double-lift-family-of-elements C b
  ev-double-lift-family-of-elements h i = h (a i) (b i)

Dependent extensions of double lifts of 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) (y : B i x) → UU l4)
  {a : (i : I) → A i} (b : dependent-lift-family-of-elements B a)
  (c : dependent-double-lift-family-of-elements C b)
  where

  is-extension-dependent-double-lift-family-of-elements :
    (f : (i : I) (x : A i) (y : B i x) → C i x y) → UU (l1 ⊔ l4)
  is-extension-dependent-double-lift-family-of-elements f =
    ev-dependent-double-lift-family-of-elements b f ~ c

  extension-dependent-double-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  extension-dependent-double-lift-family-of-elements =
    Σ ( (i : I) (x : A i) (y : B i x) → C i x y)
      ( is-extension-dependent-double-lift-family-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) (y : B i x) → UU l4}
  {a : (i : I) → A i} {b : dependent-lift-family-of-elements B a}
  {c : dependent-double-lift-family-of-elements C b}
  (f : extension-dependent-double-lift-family-of-elements C b c)
  where

  family-of-elements-extension-dependent-double-lift-family-of-elements :
    (i : I) (x : A i) (y : B i x) → C i x y
  family-of-elements-extension-dependent-double-lift-family-of-elements =
    pr1 f

  is-extension-extension-dependent-double-lift-family-of-elements :
    is-extension-dependent-double-lift-family-of-elements C b c
      ( family-of-elements-extension-dependent-double-lift-family-of-elements)
  is-extension-extension-dependent-double-lift-family-of-elements = pr2 f