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