# The universal property of sequential limits

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

Created on 2023-10-16.

module foundation.universal-property-sequential-limits where

Imports
open import foundation.action-on-identifications-functions
open import foundation.cones-over-inverse-sequential-diagrams
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.inverse-sequential-diagrams
open import foundation.postcomposition-functions
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions


## Idea

               fₙ                     f₁      f₀
⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀


the sequential limit limₙ Aₙ is a universal type completing the diagram

                           fₙ                     f₁      f₀
limₙ Aₙ ---> ⋯ ---> Aₙ₊₁ ---> Aₙ ---> ⋯ ---> A₂ ---> A₁ ---> A₀.


The universal property of the sequential limit states that limₙ Aₙ is the terminal such type, by which we mean that given any cone over A with domain X, there is a unique map g : X → limₙ Aₙ exhibiting that cone as a composite of g with the cone of limₙ Aₙ over A.

## Definition

### The universal property of sequential limits

module _
{l1 l2 : Level} (A : inverse-sequential-diagram l1)
{X : UU l2} (c : cone-inverse-sequential-diagram A X)
where

universal-property-sequential-limit : UUω
universal-property-sequential-limit =
{l : Level} (Y : UU l) →
is-equiv (cone-map-inverse-sequential-diagram A {Y = Y} c)

module _
{l1 l2 l3 : Level} (A : inverse-sequential-diagram l1)
{X : UU l2} (c : cone-inverse-sequential-diagram A X)
where

map-universal-property-sequential-limit :
universal-property-sequential-limit A c →
{Y : UU l3} (c' : cone-inverse-sequential-diagram A Y) → Y → X
map-universal-property-sequential-limit up-c {Y} c' =
map-inv-is-equiv (up-c Y) c'

compute-map-universal-property-sequential-limit :
(up-c : universal-property-sequential-limit A c) →
{Y : UU l3} (c' : cone-inverse-sequential-diagram A Y) →
cone-map-inverse-sequential-diagram A c
( map-universal-property-sequential-limit up-c c') ＝
c'
compute-map-universal-property-sequential-limit up-c {Y} c' =
is-section-map-inv-is-equiv (up-c Y) c'


## Properties

### 3-for-2 property of sequential limits

module _
{l1 l2 l3 : Level}
{A : inverse-sequential-diagram l1} {X : UU l2} {Y : UU l3}
(c : cone-inverse-sequential-diagram A X)
(c' : cone-inverse-sequential-diagram A Y)
(h : Y → X)
(KLM :
htpy-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c h) c')
where

inv-triangle-cone-cone-inverse-sequential-diagram :
{l6 : Level} (D : UU l6) →
cone-map-inverse-sequential-diagram A c ∘ postcomp D h ~
cone-map-inverse-sequential-diagram A c'
inv-triangle-cone-cone-inverse-sequential-diagram D k =
ap
( λ t → cone-map-inverse-sequential-diagram A t k)
( eq-htpy-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c h) c' KLM)

triangle-cone-cone-inverse-sequential-diagram :
{l6 : Level} (D : UU l6) →
cone-map-inverse-sequential-diagram A c' ~
cone-map-inverse-sequential-diagram A c ∘ postcomp D h
triangle-cone-cone-inverse-sequential-diagram D k =
inv (inv-triangle-cone-cone-inverse-sequential-diagram D k)

abstract
is-equiv-universal-property-sequential-limit-universal-property-sequential-limit :
universal-property-sequential-limit A c →
universal-property-sequential-limit A c' →
is-equiv h
is-equiv-universal-property-sequential-limit-universal-property-sequential-limit
up up' =
is-equiv-is-equiv-postcomp h
( λ D →
is-equiv-top-map-triangle
( cone-map-inverse-sequential-diagram A c')
( cone-map-inverse-sequential-diagram A c)
( postcomp D h)
( triangle-cone-cone-inverse-sequential-diagram D)
( up D)
( up' D))

abstract
universal-property-sequential-limit-universal-property-sequential-limit-is-equiv :
is-equiv h →
universal-property-sequential-limit A c →
universal-property-sequential-limit A c'
universal-property-sequential-limit-universal-property-sequential-limit-is-equiv
is-equiv-h up D =
is-equiv-left-map-triangle
( cone-map-inverse-sequential-diagram A c')
( cone-map-inverse-sequential-diagram A c)
( postcomp D h)
( triangle-cone-cone-inverse-sequential-diagram D)
( is-equiv-postcomp-is-equiv h is-equiv-h D)
( up D)

abstract
universal-property-sequential-limit-is-equiv-universal-property-sequential-limit :
universal-property-sequential-limit A c' →
is-equiv h →
universal-property-sequential-limit A c
universal-property-sequential-limit-is-equiv-universal-property-sequential-limit
up' is-equiv-h D =
is-equiv-right-map-triangle
( cone-map-inverse-sequential-diagram A c')
( cone-map-inverse-sequential-diagram A c)
( postcomp D h)
( triangle-cone-cone-inverse-sequential-diagram D)
( up' D)
( is-equiv-postcomp-is-equiv h is-equiv-h D)


### Uniqueness of maps obtained via the universal property of sequential limits

module _
{l1 l2 : Level} (A : inverse-sequential-diagram l1)
{X : UU l2} (c : cone-inverse-sequential-diagram A X)
where

abstract
uniqueness-universal-property-sequential-limit :
universal-property-sequential-limit A c →
{l3 : Level} (Y : UU l3) (c' : cone-inverse-sequential-diagram A Y) →
is-contr
( Σ ( Y → X)
( λ h →
htpy-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c h)
(c')))
uniqueness-universal-property-sequential-limit up Y c' =
is-contr-equiv'
( Σ (Y → X) (λ h → cone-map-inverse-sequential-diagram A c h ＝ c'))
( equiv-tot
( λ h →
extensionality-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c h)
( c')))
( is-contr-map-is-equiv (up Y) c')


### The homotopy of cones obtained from the universal property of sequential limits

module _
{l1 l2 : Level} (A : inverse-sequential-diagram l1) {X : UU l2}
where

htpy-cone-map-universal-property-sequential-limit :
(c : cone-inverse-sequential-diagram A X)
(up : universal-property-sequential-limit A c) →
{l3 : Level} {Y : UU l3} (c' : cone-inverse-sequential-diagram A Y) →
htpy-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c
( map-universal-property-sequential-limit A c up c'))
( c')
htpy-cone-map-universal-property-sequential-limit c up c' =
htpy-eq-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c
( map-universal-property-sequential-limit A c up c'))
( c')
( compute-map-universal-property-sequential-limit A c up c')


### Unique uniqueness of sequential limits

module _
{l1 l2 l3 : Level} (A : inverse-sequential-diagram l1) {X : UU l2} {Y : UU l3}
where

abstract
uniquely-unique-sequential-limit :
( c' : cone-inverse-sequential-diagram A Y)
( c : cone-inverse-sequential-diagram A X) →
( up-c' : universal-property-sequential-limit A c') →
( up-c : universal-property-sequential-limit A c) →
is-contr
( Σ (Y ≃ X)
( λ e →
htpy-cone-inverse-sequential-diagram A
( cone-map-inverse-sequential-diagram A c (map-equiv e)) c'))
uniquely-unique-sequential-limit c' c up-c' up-c =
is-torsorial-Eq-subtype
( uniqueness-universal-property-sequential-limit A c up-c Y c')
( is-property-is-equiv)
( map-universal-property-sequential-limit A c up-c c')
( htpy-cone-map-universal-property-sequential-limit A c up-c c')
( is-equiv-universal-property-sequential-limit-universal-property-sequential-limit
( c)
( c')
( map-universal-property-sequential-limit A c up-c c')
( htpy-cone-map-universal-property-sequential-limit A c up-c c')
( up-c)
( up-c'))


## Table of files about sequential limits

The following table lists files that are about sequential limits as a general concept.

ConceptFile
Inverse sequential diagrams of typesfoundation.inverse-sequential-diagrams
Dependent inverse sequential diagrams of typesfoundation.dependent-inverse-sequential-diagrams
Composite maps in inverse sequential diagramsfoundation.composite-maps-in-inverse-sequential-diagrams
Morphisms of inverse sequential diagramsfoundation.morphisms-inverse-sequential-diagrams
Equivalences of inverse sequential diagramsfoundation.equivalences-inverse-sequential-diagrams
Cones over inverse sequential diagramsfoundation.cones-over-inverse-sequential-diagrams
The universal property of sequential limitsfoundation.universal-property-sequential-limits
Sequential limitsfoundation.sequential-limits
Functoriality of sequential limitsfoundation.functoriality-sequential-limits
Transfinite cocomposition of mapsfoundation.transfinite-cocomposition-of-maps