# Functoriality of sequential limits

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-16.

module foundation.functoriality-sequential-limits where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.cones-over-inverse-sequential-diagrams
open import foundation.dependent-pair-types
open import foundation.inverse-sequential-diagrams
open import foundation.morphisms-inverse-sequential-diagrams
open import foundation.sequential-limits
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.identity-types


## Idea

The construction of the sequential limit is functorial.

## Definitions

### The functorial action on maps of standard sequential limits

module _
{l1 l2 : Level}
{A : inverse-sequential-diagram l1} {A' : inverse-sequential-diagram l2}
where

map-hom-standard-sequential-limit :
hom-inverse-sequential-diagram A' A →
standard-sequential-limit A' →
standard-sequential-limit A
pr1 (map-hom-standard-sequential-limit (f , F) (x , H)) n = f n (x n)
pr2 (map-hom-standard-sequential-limit (f , F) (x , H)) n =
ap (f n) (H n) ∙ F n (x (succ-ℕ n))

map-hom-is-sequential-limit :
{l4 l4' : Level} {C : UU l4} {C' : UU l4'} →
(c : cone-inverse-sequential-diagram A C)
(c' : cone-inverse-sequential-diagram A' C') →
is-sequential-limit A c → is-sequential-limit A' c' →
hom-inverse-sequential-diagram A' A → C' → C
map-hom-is-sequential-limit c c' is-lim-c is-lim-c' h x =
map-inv-is-equiv
( is-lim-c)
( map-hom-standard-sequential-limit h
( gap-inverse-sequential-diagram A' c' x))


## 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