# The dependent universal property of equivalences

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.

module foundation.dependent-universal-property-equivalences where

Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universe-levels

open import foundation-core.coherently-invertible-maps
open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.path-split-maps
open import foundation-core.precomposition-dependent-functions
open import foundation-core.transport-along-identifications


## Idea

The dependent universal property of equivalences states that, for a given map f : A → B, the precomposition of dependent functions by f

  - ∘ f : ((b : B) → C b) → ((a : A) → C (f a))


is an equivalence for every type family C over B. A map f : A → B satisfies the dependent universal property of equivalences if and only if it is an equivalence.

## Definitions

### The dependent universal property of equivalences

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

dependent-universal-property-equiv : UUω
dependent-universal-property-equiv =
{l : Level} (C : B → UU l) → is-equiv (precomp-Π f C)


## Properties

### If f is coherently invertible, then f satisfies the dependent universal property of equivalences

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

abstract
is-equiv-precomp-Π-is-coherently-invertible :
is-coherently-invertible f → dependent-universal-property-equiv f
is-equiv-precomp-Π-is-coherently-invertible
( g , is-section-g , is-retraction-g , coh) C =
is-equiv-is-invertible
( λ s y → tr C (is-section-g y) (s (g y)))
( λ s →
eq-htpy
( λ x →
( ap (λ t → tr C t (s (g (f x)))) (coh x)) ∙
( substitution-law-tr C f (is-retraction-g x)) ∙
( apd s (is-retraction-g x))))
( λ s → eq-htpy (λ y → apd s (is-section-g y)))


### If f is an equivalence, then f satisfies the dependent universal property of equivalences

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-equiv f)
where

abstract
is-equiv-precomp-Π-is-equiv :
dependent-universal-property-equiv f
is-equiv-precomp-Π-is-equiv =
is-equiv-precomp-Π-is-coherently-invertible f
( is-coherently-invertible-is-path-split f
( is-path-split-is-equiv f H))

map-inv-is-equiv-precomp-Π-is-equiv :
{l3 : Level} (C : B → UU l3) → ((a : A) → C (f a)) → ((b : B) → C b)
map-inv-is-equiv-precomp-Π-is-equiv C =
map-inv-is-equiv (is-equiv-precomp-Π-is-equiv C)

is-section-map-inv-is-equiv-precomp-Π-is-equiv :
{l3 : Level} (C : B → UU l3) →
(h : (a : A) → C (f a)) →
precomp-Π f C (map-inv-is-equiv-precomp-Π-is-equiv C h) ~ h
is-section-map-inv-is-equiv-precomp-Π-is-equiv C h =
htpy-eq (is-section-map-inv-is-equiv (is-equiv-precomp-Π-is-equiv C) h)

is-retraction-map-inv-is-equiv-precomp-Π-is-equiv :
{l3 : Level} (C : B → UU l3) →
(g : (b : B) → C b) →
map-inv-is-equiv-precomp-Π-is-equiv C (precomp-Π f C g) ~ g
is-retraction-map-inv-is-equiv-precomp-Π-is-equiv C g =
htpy-eq (is-retraction-map-inv-is-equiv (is-equiv-precomp-Π-is-equiv C) g)

equiv-precomp-Π :
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
(C : B → UU l3) → ((b : B) → C b) ≃ ((a : A) → C (map-equiv e a))
pr1 (equiv-precomp-Π e C) = precomp-Π (map-equiv e) C
pr2 (equiv-precomp-Π e C) = is-equiv-precomp-Π-is-equiv (is-equiv-map-equiv e) C