# Equivalences of cocones under sequential diagrams

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

Created on 2024-04-16.

module synthetic-homotopy-theory.equivalences-cocones-under-equivalences-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.equivalences
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.equivalences-sequential-diagrams
open import synthetic-homotopy-theory.morphisms-cocones-under-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 an equivalence of sequential diagrams e : A ≃ B. Then an equivalence of cocones under e 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

### Equivalences of cocones under equivalences 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)
(e : equiv-sequential-diagram A B)
where

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

coherence-equiv-cocone-equiv-sequential-diagram :
(u : X ≃ Y) →
coherence-map-cocone-equiv-cocone-equiv-sequential-diagram u →
UU (l1 ⊔ l4)
coherence-equiv-cocone-equiv-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-equiv-sequential-diagram B e n)
( map-equiv-sequential-diagram B e (succ-ℕ n))
( map-equiv u)
( coherence-cocone-sequential-diagram c n)
( H n)
( H (succ-ℕ n))
( naturality-equiv-sequential-diagram B e n)
( coherence-cocone-sequential-diagram c' n)

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

module _
(e' : equiv-cocone-equiv-sequential-diagram)
where

equiv-equiv-cocone-equiv-sequential-diagram : X ≃ Y
equiv-equiv-cocone-equiv-sequential-diagram = pr1 e'

map-equiv-cocone-equiv-sequential-diagram : X → Y
map-equiv-cocone-equiv-sequential-diagram =
map-equiv equiv-equiv-cocone-equiv-sequential-diagram

is-equiv-map-equiv-cocone-equiv-sequential-diagram :
is-equiv map-equiv-cocone-equiv-sequential-diagram
is-equiv-map-equiv-cocone-equiv-sequential-diagram =
is-equiv-map-equiv equiv-equiv-cocone-equiv-sequential-diagram

coh-map-cocone-equiv-cocone-equiv-sequential-diagram :
coherence-map-cocone-equiv-cocone-equiv-sequential-diagram
( equiv-equiv-cocone-equiv-sequential-diagram)
coh-map-cocone-equiv-cocone-equiv-sequential-diagram = pr1 (pr2 e')

coh-equiv-cocone-equiv-sequential-diagram :
coherence-equiv-cocone-equiv-sequential-diagram
( equiv-equiv-cocone-equiv-sequential-diagram)
( coh-map-cocone-equiv-cocone-equiv-sequential-diagram)
coh-equiv-cocone-equiv-sequential-diagram = pr2 (pr2 e')

hom-equiv-cocone-equiv-sequential-diagram :
hom-cocone-hom-sequential-diagram c c'
( hom-equiv-sequential-diagram B e)
pr1 hom-equiv-cocone-equiv-sequential-diagram =
map-equiv-cocone-equiv-sequential-diagram
pr1 (pr2 hom-equiv-cocone-equiv-sequential-diagram) =
coh-map-cocone-equiv-cocone-equiv-sequential-diagram
pr2 (pr2 hom-equiv-cocone-equiv-sequential-diagram) =
coh-equiv-cocone-equiv-sequential-diagram


### The predicate on morphisms of cocones under equivalences of sequential diagrams of being an equivalence

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)
(e : equiv-sequential-diagram A B)
where

is-equiv-hom-cocone-equiv-sequential-diagram :
hom-cocone-hom-sequential-diagram c c' (hom-equiv-sequential-diagram B e) →
UU (l2 ⊔ l4)
is-equiv-hom-cocone-equiv-sequential-diagram h =
is-equiv (map-hom-cocone-hom-sequential-diagram c c' h)

is-equiv-hom-equiv-cocone-equiv-sequential-diagram :
(e' : equiv-cocone-equiv-sequential-diagram c c' e) →
is-equiv-hom-cocone-equiv-sequential-diagram
( hom-equiv-cocone-equiv-sequential-diagram c c' e e')
is-equiv-hom-equiv-cocone-equiv-sequential-diagram e' =
is-equiv-map-equiv-cocone-equiv-sequential-diagram c c' e e'


## Properties

### Morphisms of cocones under equivalences of arrows which are equivalences are equivalences of cocones

To construct an equivalence of cocones under an equivalence e of sequential diagrams, it suffices to construct a morphism of cocones under the underlying morphism of sequential diagrams of e, and show that the map X → Y is an equivalence.

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)
(e : equiv-sequential-diagram A B)
where

equiv-hom-cocone-equiv-sequential-diagram :
(h :
hom-cocone-hom-sequential-diagram c c'
( hom-equiv-sequential-diagram B e)) →
is-equiv-hom-cocone-equiv-sequential-diagram c c' e h →
equiv-cocone-equiv-sequential-diagram c c' e
pr1 (equiv-hom-cocone-equiv-sequential-diagram h is-equiv-map-cocone) =
(map-hom-cocone-hom-sequential-diagram c c' h , is-equiv-map-cocone)
pr1 (pr2 (equiv-hom-cocone-equiv-sequential-diagram h _)) =
coh-map-cocone-hom-cocone-hom-sequential-diagram c c' h
pr2 (pr2 (equiv-hom-cocone-equiv-sequential-diagram h _)) =
coh-hom-cocone-hom-sequential-diagram c c' h