This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The universal property of pointed equivalences

module structured-types.universal-property-pointed-equivalences where
Imports 
open import foundation.equivalences
open import foundation.universe-levels

open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.precomposition-pointed-maps

Idea

Analogous to the universal property of equivalences, the universal property of pointed equivalences asserts about a pointed map f : A →∗ B that the precomposition function

  - ∘∗ f : (B →∗ C) → (A →∗ C)

is an equivalence for every pointed type C.

Definitions

The universal property of pointed equivalences

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  universal-property-pointed-equiv : UUω
  universal-property-pointed-equiv =
    {l : Level} (C : Pointed-Type l) → is-equiv (precomp-pointed-map f C)