# The universal property of equivalences

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-24.

module foundation.universal-property-equivalences where

Imports
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
open import foundation.precomposition-functions-into-subuniverses
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.precomposition-functions


## Idea

Consider a map f : A → B. We say that f satisfies the universal property of equivalences if precomposition by f

  - ∘ f : (B → X) → (A → X)


is an equivalence for every type X.

## Definition

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

universal-property-equiv : UUω
universal-property-equiv = {l : Level} (X : UU l) → is-equiv (precomp f X)


## Properties

### Precomposition and equivalences

#### If dependent precomposition by f is an equivalence, then precomposition by f is an equivalence

abstract
is-equiv-precomp-is-equiv-precomp-Π :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
dependent-universal-property-equiv f →
universal-property-equiv f
is-equiv-precomp-is-equiv-precomp-Π f H C = H (λ _ → C)


#### If f is an equivalence, then precomposition by f is an equivalence

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

abstract
is-equiv-precomp-is-equiv :
is-equiv f → universal-property-equiv f
is-equiv-precomp-is-equiv H =
is-equiv-precomp-is-equiv-precomp-Π f
( is-equiv-precomp-Π-is-equiv H)

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
where

abstract
is-equiv-precomp-equiv :
universal-property-equiv (map-equiv e)
is-equiv-precomp-equiv =
is-equiv-precomp-is-equiv (map-equiv e) (is-equiv-map-equiv e)

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


#### If precomposing by f is an equivalence, then f is an equivalence

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

abstract
is-equiv-is-equiv-precomp :
universal-property-equiv f → is-equiv f
is-equiv-is-equiv-precomp H =
is-equiv-is-equiv-precomp-structured-type
( λ l → l1 ⊔ l2)
( λ X → A → B)
( A , f)
( B , f)
( f)
( λ C → H (pr1 C))


#### If dependent precomposition by f is an equivalence, then f is an equivalence

abstract
is-equiv-is-equiv-precomp-Π :
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
dependent-universal-property-equiv f →
is-equiv f
is-equiv-is-equiv-precomp-Π f H =
is-equiv-is-equiv-precomp f (is-equiv-precomp-is-equiv-precomp-Π f H)