# Total sequential diagrams of dependent sequential diagrams

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

Created on 2024-04-10.

module synthetic-homotopy-theory.total-sequential-diagrams where

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

open import foundation.dependent-pair-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.dependent-sequential-diagrams
open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams
open import synthetic-homotopy-theory.equivalences-sequential-diagrams
open import synthetic-homotopy-theory.functoriality-sequential-colimits
open import synthetic-homotopy-theory.morphisms-sequential-diagrams
open import synthetic-homotopy-theory.sequential-colimits
open import synthetic-homotopy-theory.sequential-diagrams
open import synthetic-homotopy-theory.universal-property-sequential-colimits


## Idea

The total diagram of a dependent sequential diagram B : (A, a) → 𝒰 is the sequential diagram consisting of total spaces Σ Aₙ Bₙ and total maps.

## Definitions

### The total sequential diagram of a dependent sequential diagram

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

family-total-sequential-diagram : ℕ → UU (l1 ⊔ l2)
family-total-sequential-diagram n =
Σ (family-sequential-diagram A n)
(family-dependent-sequential-diagram B n)

map-total-sequential-diagram :
(n : ℕ) → family-total-sequential-diagram n →
family-total-sequential-diagram (succ-ℕ n)
map-total-sequential-diagram n =
map-Σ
( family-dependent-sequential-diagram B (succ-ℕ n))
( map-sequential-diagram A n)
( map-dependent-sequential-diagram B n)

total-sequential-diagram : sequential-diagram (l1 ⊔ l2)
pr1 total-sequential-diagram = family-total-sequential-diagram
pr2 total-sequential-diagram = map-total-sequential-diagram


### The projection morphism onto the base of the total sequential diagram

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

pr1-total-sequential-diagram :
hom-sequential-diagram
( total-sequential-diagram B)
( A)
pr1 pr1-total-sequential-diagram n = pr1
pr2 pr1-total-sequential-diagram n = refl-htpy


### The induced projection map on sequential colimits

module _
{l1 l2 l3 l4 : Level}
{A : sequential-diagram l1} (B : dependent-sequential-diagram A l2)
{X : UU l3} {c : cocone-sequential-diagram (total-sequential-diagram B) X}
(up-c : universal-property-sequential-colimit c)
{Y : UU l4} (c' : cocone-sequential-diagram A Y)
where

pr1-sequential-colimit-total-sequential-diagram : X → Y
pr1-sequential-colimit-total-sequential-diagram =
map-sequential-colimit-hom-sequential-diagram
( up-c)
( c')
( pr1-total-sequential-diagram B)


### The induced projection map on standard sequential colimits

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

pr1-standard-sequential-colimit-total-sequential-diagram :
standard-sequential-colimit (total-sequential-diagram B) →
standard-sequential-colimit A
pr1-standard-sequential-colimit-total-sequential-diagram =
map-hom-standard-sequential-colimit A
( pr1-total-sequential-diagram B)


## Properties

### Equivalences of dependent sequential diagrams induce equivalences on the total sequential diagrams

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

equiv-total-sequential-diagram-equiv-dependent-sequential-diagram :
equiv-sequential-diagram
( total-sequential-diagram B)
( total-sequential-diagram C)
pr1 equiv-total-sequential-diagram-equiv-dependent-sequential-diagram n =
equiv-tot (equiv-equiv-dependent-sequential-diagram C e n)
pr2 equiv-total-sequential-diagram-equiv-dependent-sequential-diagram n =
coherence-square-maps-Σ
( family-dependent-sequential-diagram C (succ-ℕ n))
( map-dependent-sequential-diagram B n)
( map-equiv-dependent-sequential-diagram C e n)
( map-equiv-dependent-sequential-diagram C e (succ-ℕ n))
( map-dependent-sequential-diagram C n)
{ refl-htpy}
( λ a → inv-htpy (coh-equiv-dependent-sequential-diagram C e n a))