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

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


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

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

extension-double-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
extension-double-lift-family-of-elements =
Σ ((x : A) (y : B x) → C x y) is-extension-double-lift-family-of-elements

module _
{l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
{C : (x : A) (y : B x) → UU l4}
{a : I → A} {b : lift-family-of-elements B a}
{c : double-lift-family-of-elements C b}
(f : extension-double-lift-family-of-elements C b c)
where

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

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


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

id-extension-dependent-double-lift-family-of-elements :
extension-dependent-double-lift-family-of-elements (λ i x y → B i x) b b
pr1 id-extension-dependent-double-lift-family-of-elements i x = id
pr2 id-extension-dependent-double-lift-family-of-elements = refl-htpy


### Identity extensions of double lifts of families of elements

module _
{l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
{a : I → A} (b : lift-family-of-elements B a)
where

id-extension-double-lift-family-of-elements :
extension-double-lift-family-of-elements (λ x (y : B x) → B x) b b
pr1 id-extension-double-lift-family-of-elements x = id
pr2 id-extension-double-lift-family-of-elements = refl-htpy


### Composition of extensions of dependent double lifts of families of elements

module _
{l1 l2 l3 l4 l5 : Level} {I : UU l1}
{A : I → UU l2} {B : (i : I) → A i → UU l3} {C : (i : I) → A i → UU l4}
{D : (i : I) → A i → UU l5}
{a : (i : I) → A i}
{b : dependent-lift-family-of-elements B a}
{c : dependent-lift-family-of-elements C a}
{d : dependent-lift-family-of-elements D a}
(g :
extension-dependent-double-lift-family-of-elements
( λ i x (_ : C i x) → D i x)
( c)
( d))
(f :
extension-dependent-double-lift-family-of-elements
( λ i x (_ : B i x) → C i x)
( b)
( c))
where

family-of-elements-comp-extension-dependent-double-lift-family-of-elements :
(i : I) (x : A i) → B i x → D i x
family-of-elements-comp-extension-dependent-double-lift-family-of-elements
i x =
family-of-elements-extension-dependent-double-lift-family-of-elements
g i x ∘
family-of-elements-extension-dependent-double-lift-family-of-elements
f i x

is-extension-comp-extension-dependent-double-lift-family-of-elements :
is-extension-dependent-double-lift-family-of-elements
( λ i x _ → D i x)
( b)
( d)
( family-of-elements-comp-extension-dependent-double-lift-family-of-elements)
is-extension-comp-extension-dependent-double-lift-family-of-elements i =
( ap
( family-of-elements-extension-dependent-double-lift-family-of-elements
g i (a i))
( is-extension-extension-dependent-double-lift-family-of-elements f i)) ∙
( is-extension-extension-dependent-double-lift-family-of-elements g i)

comp-extension-dependent-double-lift-family-of-elements :
extension-dependent-double-lift-family-of-elements
( λ i x (_ : B i x) → D i x)
( b)
( d)
pr1 comp-extension-dependent-double-lift-family-of-elements =
family-of-elements-comp-extension-dependent-double-lift-family-of-elements
pr2 comp-extension-dependent-double-lift-family-of-elements =
is-extension-comp-extension-dependent-double-lift-family-of-elements


### Composition of extensions of double lifts of families of elements

module _
{l1 l2 l3 l4 l5 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
{C : A → UU l4} {D : A → UU l5}
{a : I → A} {b : lift-family-of-elements B a}
{c : lift-family-of-elements C a} {d : lift-family-of-elements D a}
(g : extension-double-lift-family-of-elements (λ x (_ : C x) → D x) c d)
(f : extension-double-lift-family-of-elements (λ x (_ : B x) → C x) b c)
where

family-of-elements-comp-extension-double-lift-family-of-elements :
(x : A) → B x → D x
family-of-elements-comp-extension-double-lift-family-of-elements x =
family-of-elements-extension-double-lift-family-of-elements g x ∘
family-of-elements-extension-double-lift-family-of-elements f x

is-extension-comp-extension-double-lift-family-of-elements :
is-extension-double-lift-family-of-elements
( λ x _ → D x)
( b)
( d)
( family-of-elements-comp-extension-double-lift-family-of-elements)
is-extension-comp-extension-double-lift-family-of-elements i =
( ap
( family-of-elements-extension-double-lift-family-of-elements g (a i))
( is-extension-extension-double-lift-family-of-elements f i)) ∙
( is-extension-extension-double-lift-family-of-elements g i)

comp-extension-double-lift-family-of-elements :
extension-double-lift-family-of-elements (λ x (_ : B x) → D x) b d
pr1 comp-extension-double-lift-family-of-elements =
family-of-elements-comp-extension-double-lift-family-of-elements
pr2 comp-extension-double-lift-family-of-elements =
is-extension-comp-extension-double-lift-family-of-elements