# Universal property of contractible types

Content created by Fredrik Bakke, Egbert Rijke, Tom de Jong and Vojtěch Štěpančík.

Created on 2023-12-21.

module foundation.universal-property-contractible-types where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.singleton-induction
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.function-types
open import foundation-core.identity-types


## Idea

The dependent universal property of contractible types states that, given a point a : A, the evaluating map

  ev-point a P : ((x : A) → P x) → P a


is an equivalence for every type family P : A → 𝒰.

The condition that ev-point has a section

  P a → ((x : A) → P x)


is another way of phrasing that the type satisfies singleton induction. Furthermore, the condition that ev-point has a retraction asserts that all dependent functions (x : A) → P x are fully determined by their value at a, thus, in particular, that the section of ev-point is unique.

## Definitions

### The dependent universal property of contractible types

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

dependent-universal-property-contr : UUω
dependent-universal-property-contr =
{l : Level} (P : A → UU l) → is-equiv (ev-point a {P})


### The universal property of contractible types

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

universal-property-contr : UUω
universal-property-contr = {l : Level} (X : UU l) → is-equiv (ev-point' a {X})


## Properties

### The universal property of contractible types follows from the dependent universal property

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

universal-property-dependent-universal-property-contr :
dependent-universal-property-contr a → universal-property-contr a
universal-property-dependent-universal-property-contr dup-contr {l} X =
dup-contr (λ _ → X)


### Types satisfying the universal property of contractible types are contractible

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

abstract
is-contr-is-equiv-ev-point :
is-equiv (ev-point' a {A}) → is-contr A
pr1 (is-contr-is-equiv-ev-point H) = a
pr2 (is-contr-is-equiv-ev-point H) =
htpy-eq
( ap
( pr1)
( eq-is-contr'
( is-contr-map-is-equiv H a)
( (λ _ → a) , refl)
( id , refl)))

abstract
is-contr-universal-property-contr :
universal-property-contr a → is-contr A
is-contr-universal-property-contr up-contr =
is-contr-is-equiv-ev-point (up-contr A)


### Types satisfying the dependent universal property of contractible types are contractible

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

abstract
is-contr-dependent-universal-property-contr :
dependent-universal-property-contr a → is-contr A
is-contr-dependent-universal-property-contr dup-contr =
is-contr-universal-property-contr a
( universal-property-dependent-universal-property-contr a dup-contr)


### Types that are contractible satisfy the dependent universal property

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

abstract
dependent-universal-property-contr-is-contr :
is-contr A → dependent-universal-property-contr a
dependent-universal-property-contr-is-contr H P =
is-equiv-is-invertible
( ind-singleton a H P)
( compute-ind-singleton a H P)
( λ f →
eq-htpy
( ind-singleton a H
( λ x → ind-singleton a H P (f a) x ＝ f x)
( compute-ind-singleton a H P (f a))))

equiv-dependent-universal-property-contr :
is-contr A → {l : Level} (B : A → UU l) → ((x : A) → B x) ≃ B a
pr1 (equiv-dependent-universal-property-contr H P) = ev-point a
pr2 (equiv-dependent-universal-property-contr H P) =
dependent-universal-property-contr-is-contr H P

apply-dependent-universal-property-contr :
is-contr A → {l : Level} (B : A → UU l) → (B a → ((x : A) → B x))
apply-dependent-universal-property-contr H P =
map-inv-equiv (equiv-dependent-universal-property-contr H P)


### Types that are contractible satisfy the universal property

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

abstract
universal-property-contr-is-contr :
is-contr A → universal-property-contr a
universal-property-contr-is-contr H =
universal-property-dependent-universal-property-contr a
( dependent-universal-property-contr-is-contr a H)

equiv-universal-property-contr :
is-contr A → {l : Level} (X : UU l) → (A → X) ≃ X
pr1 (equiv-universal-property-contr H X) = ev-point' a
pr2 (equiv-universal-property-contr H X) =
universal-property-contr-is-contr H X

apply-universal-property-contr :
is-contr A → {l : Level} (X : UU l) → X → (A → X)
apply-universal-property-contr H X =
map-inv-equiv (equiv-universal-property-contr H X)