Morphisms of dependent sequential diagrams

Content created by Vojtěch Štěpančík.

Created on 2024-04-16.
Last modified on 2024-04-16.

module synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.dependent-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams

Idea

Consider two dependent sequential diagrams

     b₀      b₁      b₂            c₀      c₁      c₂
 B₀ ---> B₁ ---> B₂ ---> ⋯     C₀ ---> C₁ ---> C₂ ---> ⋯
 |       |       |             |       |       |
 |       |       |             |       |       |
 ↡       ↡       ↡             ↡       ↡       ↡
 A₀ ---> A₁ ---> A₂ ---> ⋯     A₀ ---> A₁ ---> A₂ ---> ⋯ .
     a₀      a₁      a₂            a₀      a₁      a₂

A morphism of dependent sequential diagrams between them is a family of fiberwise maps

hₙ : (a : Aₙ) → Bₙ a → Cₙ a

equipped with a family of fiberwise homotopies making the squares

                 hₙ a
     Bₙ a -----------------> Cₙ a
       |                       |
  bₙ a |                       | cₙ a
       |                       |
       ∨                       ∨
  Bₙ₊₁ (aₙ a) ----------> Cₙ₊₁ (aₙ a)
              hₙ₊₁ (aₙ a)

commute.

Definitions

Morphisms of dependent sequential diagrams

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  (B : dependent-sequential-diagram A l2)
  (C : dependent-sequential-diagram A l3)
  where

  coherence-hom-dependent-sequential-diagram :
    ( (n : ℕ) (a : family-sequential-diagram A n) →
      family-dependent-sequential-diagram B n a →
      family-dependent-sequential-diagram C n a) →
    UU (l1 ⊔ l2 ⊔ l3)
  coherence-hom-dependent-sequential-diagram h =
    (n : ℕ) (a : family-sequential-diagram A n) →
    coherence-square-maps
      ( h n a)
      ( map-dependent-sequential-diagram B n a)
      ( map-dependent-sequential-diagram C n a)
      ( h (succ-ℕ n) (map-sequential-diagram A n a))

  hom-dependent-sequential-diagram : UU (l1 ⊔ l2 ⊔ l3)
  hom-dependent-sequential-diagram =
    Σ ( (n : ℕ) (a : family-sequential-diagram A n) →
        family-dependent-sequential-diagram B n a →
        family-dependent-sequential-diagram C n a)
      ( coherence-hom-dependent-sequential-diagram)

Components of a morphism of sequential diagrams

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  {B : dependent-sequential-diagram A l2}
  (C : dependent-sequential-diagram A l3)
  (h : hom-dependent-sequential-diagram B C)
  where

  map-hom-dependent-sequential-diagram :
    (n : ℕ) (a : family-sequential-diagram A n) →
    family-dependent-sequential-diagram B n a →
    family-dependent-sequential-diagram C n a
  map-hom-dependent-sequential-diagram = pr1 h

  coh-hom-dependent-sequential-diagram :
    coherence-hom-dependent-sequential-diagram B C
      ( map-hom-dependent-sequential-diagram)
  coh-hom-dependent-sequential-diagram = pr2 h

Recent changes