# Composite maps in inverse sequential diagrams

Content created by Fredrik Bakke.

Created on 2024-01-11.

module foundation.composite-maps-in-inverse-sequential-diagrams where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-inverse-sequential-diagrams
open import foundation.inverse-sequential-diagrams
open import foundation.universe-levels

open import foundation-core.function-types


## Idea

Given a (dependent) inverse sequential diagram A, we can extract the composite map from Aₙ₊ᵣ to Aₙ.

## Definitions

### Composite maps in inverse sequential diagrams

comp-map-inverse-sequential-diagram :
{l : Level} (A : inverse-sequential-diagram l) (n r : ℕ) →
family-inverse-sequential-diagram A (n +ℕ r) →
family-inverse-sequential-diagram A n
comp-map-inverse-sequential-diagram A n zero-ℕ = id
comp-map-inverse-sequential-diagram A n (succ-ℕ r) =
comp-map-inverse-sequential-diagram A n r ∘
map-inverse-sequential-diagram A (n +ℕ r)


### Composite maps in dependent inverse sequential diagrams

comp-map-dependent-inverse-sequential-diagram :
{l1 l2 : Level} {A : inverse-sequential-diagram l1}
(B : dependent-inverse-sequential-diagram l2 A)
(n r : ℕ) (x : family-inverse-sequential-diagram A (n +ℕ r)) →
family-dependent-inverse-sequential-diagram B (n +ℕ r) x →
family-dependent-inverse-sequential-diagram B n
( comp-map-inverse-sequential-diagram A n r x)
comp-map-dependent-inverse-sequential-diagram B n zero-ℕ x y = y
comp-map-dependent-inverse-sequential-diagram {A = A} B n (succ-ℕ r) x y =
comp-map-dependent-inverse-sequential-diagram B n r
( map-inverse-sequential-diagram A (n +ℕ r) x)
( map-dependent-inverse-sequential-diagram B (n +ℕ r) x y)


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