# Transfinite cocomposition of maps

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-16.

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