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


The construction of the sequential limit is functorial.


The functorial action on maps of standard sequential limits

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

  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 =
      ( 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.

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

Recent changes