# Morphisms of cocones under morphisms of sequential diagrams

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

Created on 2024-04-16.

module synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequential-diagrams where

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

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

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.morphisms-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams


## Idea

Consider two sequential diagrams (A, a) and (B, b), equipped with cocones c : A → X and c' : B → Y, respectively, and a morphism of sequential diagrams h : A → B. Then a morphism of cocones under h is a triple (u, H, K), with u : X → Y a map of vertices of the coforks, H a family of homotopies witnessing that the square

           iₙ
Aₙ -------> X
|           |
hₙ |           | u
|           |
∨           ∨
Bₙ -------> Y
i'ₙ


commutes for every n, and K a family of coherence data filling the insides of the resulting prism boundaries

            Aₙ₊₁
aₙ  ∧ |  \  iₙ₊₁
/   |    \
/     |      ∨
Aₙ -----------> X
|   iₙ  |       |
|       | hₙ₊₁  |
hₙ |       ∨       | u
|      Bₙ₊₁     |
|  bₙ ∧   \i'ₙ₊₁|
|   /       \   |
∨ /           ∨ ∨
Bₙ -----------> Y
i'ₙ


for every n.

## Definition

### Morphisms of cocones under morphisms of sequential diagrams

module _
{l1 l2 l3 l4 : Level}
{A : sequential-diagram l1} {X : UU l2} (c : cocone-sequential-diagram A X)
{B : sequential-diagram l3} {Y : UU l4} (c' : cocone-sequential-diagram B Y)
(h : hom-sequential-diagram A B)
where

coherence-map-cocone-hom-cocone-hom-sequential-diagram :
(X → Y) → UU (l1 ⊔ l4)
coherence-map-cocone-hom-cocone-hom-sequential-diagram u =
(n : ℕ) →
coherence-square-maps
( map-cocone-sequential-diagram c n)
( map-hom-sequential-diagram B h n)
( u)
( map-cocone-sequential-diagram c' n)

coherence-hom-cocone-hom-sequential-diagram :
(u : X → Y) →
coherence-map-cocone-hom-cocone-hom-sequential-diagram u →
UU (l1 ⊔ l4)
coherence-hom-cocone-hom-sequential-diagram u H =
(n : ℕ) →
vertical-coherence-prism-maps
( map-cocone-sequential-diagram c n)
( map-cocone-sequential-diagram c (succ-ℕ n))
( map-sequential-diagram A n)
( map-cocone-sequential-diagram c' n)
( map-cocone-sequential-diagram c' (succ-ℕ n))
( map-sequential-diagram B n)
( map-hom-sequential-diagram B h n)
( map-hom-sequential-diagram B h (succ-ℕ n))
( u)
( coherence-cocone-sequential-diagram c n)
( H n)
( H (succ-ℕ n))
( naturality-map-hom-sequential-diagram B h n)
( coherence-cocone-sequential-diagram c' n)

hom-cocone-hom-sequential-diagram : UU (l1 ⊔ l2 ⊔ l4)
hom-cocone-hom-sequential-diagram =
Σ ( X → Y)
( λ u →
Σ ( coherence-map-cocone-hom-cocone-hom-sequential-diagram u)
( coherence-hom-cocone-hom-sequential-diagram u))


### Components of a morphism of cocones under a morphism of sequential diagrams

module _
{l1 l2 l3 l4 : Level}
{A : sequential-diagram l1} {X : UU l2} (c : cocone-sequential-diagram A X)
{B : sequential-diagram l3} {Y : UU l4} (c' : cocone-sequential-diagram B Y)
{h : hom-sequential-diagram A B}
(m : hom-cocone-hom-sequential-diagram c c' h)
where

map-hom-cocone-hom-sequential-diagram : X → Y
map-hom-cocone-hom-sequential-diagram = pr1 m

coh-map-cocone-hom-cocone-hom-sequential-diagram :
coherence-map-cocone-hom-cocone-hom-sequential-diagram c c' h
( map-hom-cocone-hom-sequential-diagram)
coh-map-cocone-hom-cocone-hom-sequential-diagram = pr1 (pr2 m)

coh-hom-cocone-hom-sequential-diagram :
coherence-hom-cocone-hom-sequential-diagram c c' h
( map-hom-cocone-hom-sequential-diagram)
( coh-map-cocone-hom-cocone-hom-sequential-diagram)
coh-hom-cocone-hom-sequential-diagram = pr2 (pr2 m)