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.double-lifts-families-of-elements where
Imports 
open import foundation.universe-levels

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

Idea

Consider a family of elements b : (i : I) → B i (a i) over a family of elements a : (i : I) → A i and consider a family of types

  C : (i : I) (x : A i) → B i x → 𝒰.

Recall that b is also a dependent lift of the family of elements a. The type of dependent double lifts of b and a to C is defined to be the type

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

Note that this is the type of double lifts in the sense that it simultaneously lifts a and b to the type family C.

The definition of (ordinary) double lifts is somewhat simpler: Given a lift b of a : I → A to a type family B : A → 𝒰, a double lift of a and b to a type family

  C : (x : A) → B x → 𝒰

is a family of elements

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

Note that this is the type of double lifts in the sense that it simultaneously lifts a and b to the type family C.

The type of double lifts plays a role in the universal property of the family of fibers of a map.

Definitions

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

  dependent-double-lift-family-of-elements : UU (l1 ⊔ l4)
  dependent-double-lift-family-of-elements =
    dependent-lift-family-of-elements (λ i → C i (a i)) b

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

  double-lift-family-of-elements : UU (l1 ⊔ l4)
  double-lift-family-of-elements =
    dependent-lift-family-of-elements (λ i → C (a i)) b

See also

Recent changes