Composite maps in inverse sequential diagrams

Content created by Fredrik Bakke.

Created on 2024-01-11.
Last modified 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

Recent changes