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

Universal property of contractible types with respect to pointed types and maps

module structured-types.pointed-universal-property-contractible-types where

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universal-property-contractible-types
open import foundation.universe-levels

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

Idea

By definition, a contractible type is pointed. Moreover, they enjoy a universal property among the pointed types with respect to pointed maps:

A pointed type A is contractible if for all pointed types X, the type of pointed maps A →∗ X is contractible.

Definitions

The universal property of contractible types with respect to pointed types and maps

module _
  {l1 : Level} (A : Pointed-Type l1)
  where

  universal-property-contr-Pointed-Type : UUω
  universal-property-contr-Pointed-Type =
    {l : Level} (X : Pointed-Type l) → is-contr (A →∗ X)

Properties

A contractible type has the universal property of contractible types with respect to pointed types and maps

Proof: If A is contractible with a point a : A, then we have

   ((A , a) →∗ (X , x))
 ≃ Σ (A → X) (λ f → f a ＝ x)
 ≃ Σ X (λ y → y ＝ x)

where the last equivalence holds since (A → X) ≃ X by the universal property of contractible types.

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

  universal-property-contr-is-contr-Pointed-Type' :
    is-contr A → universal-property-contr-Pointed-Type (A , a)
  universal-property-contr-is-contr-Pointed-Type' c (X , x) =
    is-contr-equiv
      ( Σ X (λ y → y ＝ x))
      ( equiv-Σ-equiv-base _ (equiv-universal-property-contr a c X))
      ( is-torsorial-Id' x)

module _
  {l1 : Level} {A : UU l1}
  where

  universal-property-contr-is-contr-Pointed-Type :
    (c : is-contr A) → universal-property-contr-Pointed-Type (A , center c)
  universal-property-contr-is-contr-Pointed-Type c =
    universal-property-contr-is-contr-Pointed-Type' (center c) c

A pointed type with the universal property of contractible types with respect to pointed types and maps is contractible

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

  is-contr-universal-property-contr-Pointed-Type' :
    universal-property-contr-Pointed-Type (A , a) → is-contr A
  is-contr-universal-property-contr-Pointed-Type' up =
    is-contr-universal-property-contr a
      ( λ X →
        is-equiv-htpy-equiv
          ( equivalence-reasoning
              (A → X)
              ≃ Σ (A → X) (λ f → Σ X (λ x → f a ＝ x))
                by inv-right-unit-law-Σ-is-contr (λ f → is-torsorial-Id (f a))
              ≃ Σ X (λ x → (A , a) →∗ (X , x))
                by equiv-left-swap-Σ
              ≃ X
                by equiv-pr1 (λ x → up (X , x)))
            ( λ f →
              ap
                ( pr1)
                ( inv
                  ( contraction (is-torsorial-Id (f a)) (pair (f a) refl)))))

module _
  {l1 : Level} (A : Pointed-Type l1)
  where

  is-contr-universal-property-contr-Pointed-Type :
    universal-property-contr-Pointed-Type A → is-contr (type-Pointed-Type A)
  is-contr-universal-property-contr-Pointed-Type =
    is-contr-universal-property-contr-Pointed-Type' (point-Pointed-Type A)