# Double lifts of families of elements

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

Created on 2023-12-05.

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