# Double lifts of families of elements

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

<details><summary>Imports</summary>

```agda
open import foundation.universe-levels

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

</details>

## 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

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

Recall that `b` is also a
[dependent lift](orthogonal-factorization-systems.lifts-families-of-elements.md)
of the family of elements `a`. The type of
{{#concept "dependent double lifts" Disambiguation="family of elements" Agda=dependent-double-lift-family-of-elements}}
of `b` and `a` to `C` is defined to be the type

```text
  (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
{{#concept "double lift" Disambiguation="families of elements" Agda=double-lift-family-of-elements}}
of `a` and `b` to a type family

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

is a family of elements

```text
  (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](foundation.universal-property-family-of-fibers-of-maps.md).

## Definitions

### Dependent double lifts of families of elements

```agda
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

```agda
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

- [Lifts of families of elements](orthogonal-factorization-systems.lifts-families-of-elements.md)
- [Lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md)
- [The universal property of the family of fibers of a map](foundation.universal-property-family-of-fibers-of-maps.md)