# Extensions 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-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.lifts-families-of-elements


## Idea

Consider a family of elements a : I → A, a type family B over A and a lift

  b : (i : I) → B (a i)


of the family of elements a. An extension of b to A consists of a family of elements f : (x : A) → B x equipped with a homotopy f ∘ a ~ b.

More generally, given a family of elements a : (i : I) → A i, a type family B over A, and a dependent lift

  b : (i : I) → B i (a i)


of the family of elements A, a dependent extension of b to A consists of a family of elements

  f : (i : I) (x : A i) → B i x


equipped with a homotopy (i : I) → f i (a i) ＝ b i.

## Definitions

### Evaluating families of elements at lifts of families of elements

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

  ((i : I) (x : A i) → B i x) → ((i : I) → B i (a i))


defined by b ↦ (λ i → b i (a i)).

module _
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
(a : (i : I) → A i)
where

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

module _
{l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3} (a : I → A)
where

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


### Dependent extensions of dependent 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

is-extension-dependent-lift-family-of-elements :
(f : (i : I) (x : A i) → B i x) → UU (l1 ⊔ l3)
is-extension-dependent-lift-family-of-elements f =
ev-dependent-lift-family-of-elements a f ~ b

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

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

is-extension-extension-dependent-lift-family-of-elements :
is-extension-dependent-lift-family-of-elements B a b
( family-of-elements-extension-dependent-lift-family-of-elements)
is-extension-extension-dependent-lift-family-of-elements = pr2 f


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

is-extension-lift-family-of-elements : (f : (x : A) → B x) → UU (l1 ⊔ l3)
is-extension-lift-family-of-elements f = ev-lift-family-of-elements a f ~ b

extension-lift-family-of-elements : UU (l1 ⊔ l2 ⊔ l3)
extension-lift-family-of-elements =
Σ ((x : A) → B x) is-extension-lift-family-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}
(f : extension-lift-family-of-elements B a b)
where

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

is-extension-extension-lift-family-of-elements :
is-extension-lift-family-of-elements B a b
( family-of-elements-extension-lift-family-of-elements)
is-extension-extension-lift-family-of-elements = pr2 f


### Identity extensions of dependent lifts of families of elements

module _
{l1 l2 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
where

id-extension-dependent-lift-family-of-elements :
extension-dependent-lift-family-of-elements (λ i _ → A i) a a
pr1 id-extension-dependent-lift-family-of-elements i = id
pr2 id-extension-dependent-lift-family-of-elements = refl-htpy


### Identity extensions of lifts of families of elements

module _
{l1 l2 : Level} {I : UU l1} {A : UU l2} (a : I → A)
where

id-extension-lift-family-of-elements :
extension-lift-family-of-elements (λ _ → A) a a
pr1 id-extension-lift-family-of-elements = id
pr2 id-extension-lift-family-of-elements = refl-htpy


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

Consider three type families A, B, and C over a type I equipped with sections

  a : (i : I) → A i
b : (i : I) → B i
c : (i : I) → C i.


Furthermore, suppose that g is an extension of c along b, and suppose that f is an extension of b along a. In other words, g consists of a family of maps

  g : (i : I) → B i → C i


equipped with a homotopy witnessing that g i (b i) ＝ c i for all i : I, and f consists of a family of maps

  f : (i : I) → A i → B i


equipped with a homotopy witnessing that f i (a i) ＝ b i for all i : I. Then we can compose g and f fiberwise, resulting in a family of maps

  λ i → g i ∘ f i : (i : I) → A i → C i


equipped with a homotopy witnessing that g i (f i (a i)) ＝ c i for all i : I. In other words, extensions of c along b can be composed with extensions of b along a to obtain extensions of c along a.

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

family-of-elements-comp-extension-dependent-lift-family-of-elements :
(i : I) → A i → C i
family-of-elements-comp-extension-dependent-lift-family-of-elements i =
family-of-elements-extension-dependent-lift-family-of-elements g i ∘
family-of-elements-extension-dependent-lift-family-of-elements f i

is-extension-comp-extension-dependent-lift-family-of-elements :
is-extension-dependent-lift-family-of-elements
( λ i _ → C i)
( a)
( c)
( family-of-elements-comp-extension-dependent-lift-family-of-elements)
is-extension-comp-extension-dependent-lift-family-of-elements i =
( ap
( family-of-elements-extension-dependent-lift-family-of-elements g i)
( is-extension-extension-dependent-lift-family-of-elements f i)) ∙
( is-extension-extension-dependent-lift-family-of-elements g i)

comp-extension-dependent-lift-family-of-elements :
extension-dependent-lift-family-of-elements (λ i _ → C i) a c
pr1 comp-extension-dependent-lift-family-of-elements =
family-of-elements-comp-extension-dependent-lift-family-of-elements
pr2 comp-extension-dependent-lift-family-of-elements =
is-extension-comp-extension-dependent-lift-family-of-elements


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

Consider three types A, B, and C equipped with maps

  a : I → A
b : I → B
c : I → C.


Furthermore, suppose that g is an extension of c along b, and suppose that f is an extension of b along a. In other words, we assume a commuting diagram

        I
/ | \
a/  |  \c
/   |b  \
∨    ∨    ∨
A --> B --> C
f     g


The composite g ∘ f is then an extension of c along a.

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

map-comp-extension-lift-family-of-elements : A → C
map-comp-extension-lift-family-of-elements =
family-of-elements-extension-lift-family-of-elements g ∘
family-of-elements-extension-lift-family-of-elements f

is-extension-comp-extension-lift-family-of-elements :
is-extension-lift-family-of-elements
( λ _ → C)
( a)
( c)
( map-comp-extension-lift-family-of-elements)
is-extension-comp-extension-lift-family-of-elements x =
( ap
( family-of-elements-extension-lift-family-of-elements g)
( is-extension-extension-lift-family-of-elements f x)) ∙
( is-extension-extension-lift-family-of-elements g x)

comp-extension-lift-family-of-elements :
extension-lift-family-of-elements (λ _ → C) a c
pr1 comp-extension-lift-family-of-elements =
map-comp-extension-lift-family-of-elements
pr2 comp-extension-lift-family-of-elements =
is-extension-comp-extension-lift-family-of-elements
`