Transfinite cocomposition of maps

Content created by Fredrik Bakke and Egbert Rijke.

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

module foundation.transfinite-cocomposition-of-maps where
Imports 
open import foundation.inverse-sequential-diagrams
open import foundation.sequential-limits
open import foundation.universe-levels

Idea

Given an inverse sequential diagram of types, i.e. a certain infinite sequence of maps fₙ:

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

we can form the transfinite cocomposition of f by taking the canonical map from the standard sequential limit limₙ Aₙ into A₀.

Definitions

The transfinite cocomposition of an inverse sequential diagram of maps

module _
  {l : Level} (f : inverse-sequential-diagram l)
  where

  transfinite-cocomp :
    standard-sequential-limit f → family-inverse-sequential-diagram f 0
  transfinite-cocomp x = sequence-standard-sequential-limit f x 0

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

Recent changes