Functoriality of sequential limits

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-16.
Last modified on 2024-01-11.

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.

Concept	File
Inverse sequential diagrams of types	`foundation.inverse-sequential-diagrams`
Dependent inverse sequential diagrams of types	`foundation.dependent-inverse-sequential-diagrams`
Composite maps in inverse sequential diagrams	`foundation.composite-maps-in-inverse-sequential-diagrams`
Morphisms of inverse sequential diagrams	`foundation.morphisms-inverse-sequential-diagrams`
Equivalences of inverse sequential diagrams	`foundation.equivalences-inverse-sequential-diagrams`
Cones over inverse sequential diagrams	`foundation.cones-over-inverse-sequential-diagrams`
The universal property of sequential limits	`foundation.universal-property-sequential-limits`
Sequential limits	`foundation.sequential-limits`
Functoriality of sequential limits	`foundation.functoriality-sequential-limits`
Transfinite cocomposition of maps	`foundation.transfinite-cocomposition-of-maps`

Recent changes

2024-01-11. Fredrik Bakke. Rename "towers" to "inverse sequential diagrams" (#990).
2023-11-01. Fredrik Bakke. Fun with functors (#886).
2023-10-16. Fredrik Bakke and Egbert Rijke. Sequential limits (#839).