# Functoriality of dependent function types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Raymond Baker, Elisabeth Stenholm and Vojtěch Štěpančík.

Created on 2022-05-16.

module foundation-core.functoriality-dependent-function-types where

Imports
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.implicit-function-types
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.families-of-equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.type-theoretic-principle-of-choice


## Properties

### The operation map-Π preserves homotopies

htpy-map-Π :
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
{f f' : (i : I) → A i → B i} (H : (i : I) → (f i) ~ (f' i)) →
map-Π f ~ map-Π f'
htpy-map-Π H h = eq-htpy (λ i → H i (h i))

htpy-map-Π' :
{l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
{J : UU l4} (α : J → I) {f f' : (i : I) → A i → B i} →
((i : I) → (f i) ~ (f' i)) → map-Π' α f ~ map-Π' α f'
htpy-map-Π' α H = htpy-map-Π (H ∘ α)


### The fibers of map-Π

compute-fiber-map-Π :
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
(f : (i : I) → A i → B i) (h : (i : I) → B i) →
((i : I) → fiber (f i) (h i)) ≃ fiber (map-Π f) h
compute-fiber-map-Π f h = equiv-tot (λ _ → equiv-eq-htpy) ∘e distributive-Π-Σ

compute-fiber-map-Π' :
{l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
{J : UU l4} (α : J → I) (f : (i : I) → A i → B i)
(h : (j : J) → B (α j)) →
((j : J) → fiber (f (α j)) (h j)) ≃ fiber (map-Π' α f) h
compute-fiber-map-Π' α f = compute-fiber-map-Π (f ∘ α)


### Families of equivalences induce equivalences of dependent function types

abstract
is-equiv-map-Π-is-fiberwise-equiv :
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
{f : (i : I) → A i → B i} → is-fiberwise-equiv f →
is-equiv (map-Π f)
is-equiv-map-Π-is-fiberwise-equiv is-equiv-f =
is-equiv-is-contr-map
( λ g →
is-contr-equiv' _
( compute-fiber-map-Π _ g)
( is-contr-Π (λ i → is-contr-map-is-equiv (is-equiv-f i) (g i))))

equiv-Π-equiv-family :
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
(e : (i : I) → A i ≃ B i) → ((i : I) → A i) ≃ ((i : I) → B i)
pr1 (equiv-Π-equiv-family e) =
map-Π (λ i → map-equiv (e i))
pr2 (equiv-Π-equiv-family e) =
is-equiv-map-Π-is-fiberwise-equiv (λ i → is-equiv-map-equiv (e i))


### Families of equivalences induce equivalences of implicit dependent function types

is-equiv-map-implicit-Π-is-fiberwise-equiv :
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
{f : (i : I) → A i → B i} → is-fiberwise-equiv f →
is-equiv (map-implicit-Π f)
is-equiv-map-implicit-Π-is-fiberwise-equiv is-equiv-f =
is-equiv-comp _ _
( is-equiv-explicit-implicit-Π)
( is-equiv-comp _ _
( is-equiv-map-Π-is-fiberwise-equiv is-equiv-f)
( is-equiv-implicit-explicit-Π))

equiv-implicit-Π-equiv-family :
{l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
(e : (i : I) → (A i) ≃ (B i)) → ({i : I} → A i) ≃ ({i : I} → B i)
equiv-implicit-Π-equiv-family e =
( equiv-implicit-explicit-Π) ∘e
( equiv-Π-equiv-family e) ∘e
( equiv-explicit-implicit-Π)

##### Computing the inverse of equiv-Π-equiv-family
module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
where

compute-inv-equiv-Π-equiv-family :
(e : (x : A) → B x ≃ C x) →
( map-inv-equiv (equiv-Π-equiv-family e)) ~
( map-equiv (equiv-Π-equiv-family (λ x → inv-equiv (e x))))
compute-inv-equiv-Π-equiv-family e f =
is-injective-equiv
( equiv-Π-equiv-family e)
( ( is-section-map-inv-equiv (equiv-Π-equiv-family e) f) ∙
( eq-htpy (λ x → inv (is-section-map-inv-equiv (e x) (f x)))))