# Inverse sequential diagrams of types

Content created by Fredrik Bakke.

Created on 2024-01-11.

module foundation.inverse-sequential-diagrams where

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

open import foundation.dependent-pair-types
open import foundation.iterating-functions
open import foundation.unit-type
open import foundation.universe-levels


## Idea

An inverse sequential diagram of types A is a sequence of types together with maps between every two consecutive types

  fₙ : Aₙ₊₁ → Aₙ


giving a sequential diagram of maps that extend infinitely to the left:

     f₃      f₂      f₁      f₀
⋯ ---> A₃ ---> A₂ ---> A₁ ---> A₀.


This is in contrast to the notion of sequential diagram, which extend infinitely to the right, hence is the formal dual to inverse sequential diagrams.

## Definitions

### Inverse sequential diagrams of types

sequence-map-inverse-sequential-diagram : {l : Level} → (ℕ → UU l) → UU l
sequence-map-inverse-sequential-diagram A = (n : ℕ) → A (succ-ℕ n) → A n

inverse-sequential-diagram : (l : Level) → UU (lsuc l)
inverse-sequential-diagram l =
Σ (ℕ → UU l) (sequence-map-inverse-sequential-diagram)

family-inverse-sequential-diagram :
{l : Level} → inverse-sequential-diagram l → ℕ → UU l
family-inverse-sequential-diagram = pr1

map-inverse-sequential-diagram :
{l : Level} (A : inverse-sequential-diagram l) (n : ℕ) →
family-inverse-sequential-diagram A (succ-ℕ n) →
family-inverse-sequential-diagram A n
map-inverse-sequential-diagram = pr2


## Operations

### Right shifting an inverse sequential diagram

We can right shift an inverse sequential diagram of types by forgetting the first terms.

right-shift-inverse-sequential-diagram :
{l : Level} → inverse-sequential-diagram l → inverse-sequential-diagram l
pr1 (right-shift-inverse-sequential-diagram A) n =
family-inverse-sequential-diagram A (succ-ℕ n)
pr2 (right-shift-inverse-sequential-diagram A) n =
map-inverse-sequential-diagram A (succ-ℕ n)

iterated-right-shift-inverse-sequential-diagram :
{l : Level} (n : ℕ) →
inverse-sequential-diagram l → inverse-sequential-diagram l
iterated-right-shift-inverse-sequential-diagram n =
iterate n right-shift-inverse-sequential-diagram


### Left shifting an inverse sequential diagram

We can left shift an inverse sequential diagram of types by padding it with the terminal type unit.

left-shift-inverse-sequential-diagram :
{l : Level} → inverse-sequential-diagram l → inverse-sequential-diagram l
pr1 (left-shift-inverse-sequential-diagram {l} A) 0 = raise-unit l
pr1 (left-shift-inverse-sequential-diagram A) (succ-ℕ n) =
family-inverse-sequential-diagram A n
pr2 (left-shift-inverse-sequential-diagram A) 0 =
raise-terminal-map (family-inverse-sequential-diagram A 0)
pr2 (left-shift-inverse-sequential-diagram A) (succ-ℕ n) =
map-inverse-sequential-diagram A n

iterated-left-shift-inverse-sequential-diagram :
{l : Level} (n : ℕ) →
inverse-sequential-diagram l → inverse-sequential-diagram l
iterated-left-shift-inverse-sequential-diagram n =
iterate n left-shift-inverse-sequential-diagram


### Postcomposition inverse sequential diagrams

Given an inverse sequential diagram A and a type X there is an inverse sequential diagram X → A defined by levelwise postcomposition

                    (f₂ ∘ -)          (f₁ ∘ -)          (f₀ ∘ -)
⋯ -----> (X → A₃) -------> (X → A₂) -------> (X → A₁) -------> (X → A₀).

module _
{l1 l2 : Level} (X : UU l1) (A : inverse-sequential-diagram l2)
where

postcomp-inverse-sequential-diagram : inverse-sequential-diagram (l1 ⊔ l2)
pr1 postcomp-inverse-sequential-diagram n =
X → family-inverse-sequential-diagram A n
pr2 postcomp-inverse-sequential-diagram n g x =
map-inverse-sequential-diagram A n (g x)


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