# Morphisms of coforks

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

Created on 2024-04-16.

module synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows where

Imports
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.double-arrows
open import foundation.homotopies
open import foundation.morphisms-arrows
open import foundation.morphisms-double-arrows
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import synthetic-homotopy-theory.coforks


## Idea

Consider two double arrows f, g : A → B and h, k : U → V, equipped with coforks c : B → X and c' : V → Y, respectively, and a morphism of double arrows e : (f, g) → (h, k).

Then a morphism of coforks under e is a triple (m, H, K), with m : X → Y a map of vertices of the coforks, H a homotopy witnessing that the bottom square in the diagram

           i
A --------> U
| |         | |
f | | g     h | | k
| |         | |
∨ ∨         ∨ ∨
B --------> V
|     j     |
c |           | c'
|           |
∨           ∨
X --------> Y
m


commutes, and K a coherence datum "filling the inside" --- we have two stacks of squares

           i                        i
A --------> U            A --------> U
|           |            |           |
f |           | h        g |           | k
|           |            |           |
∨           ∨            ∨           ∨
B --------> V            B --------> V
|     j     |            |     j     |
c |           | c'       c |           | c'
|           |            |           |
∨           ∨            ∨           ∨
X --------> Y            X --------> Y
m                        m


which share the top map i and the bottom square, and the coherences of c and c' filling the sides; that gives the homotopies

                                                i                 i
A                  A                 A --------> U     A --------> U
|                  |                             |                 |
f |                f |                             | h               | k
|                  |                             |                 |
∨                  ∨     j                       ∨                 ∨
B         ~        B --------> V       ~         V        ~        V
|                              |                 |                 |
c |                              | c'              | c'              | c'
|                              |                 |                 |
∨                              ∨                 ∨                 ∨
X --------> Y                  Y                 Y                 Y
m


and

                                                                  i
A                 A               A                    A --------> U
|                 |               |                                |
f |               g |             g |                                | k
|                 |               |                                |
∨                 ∨               ∨     j                          ∨
B         ~       B       ~       B --------> V           ~        V
|                 |                           |                    |
c |               c |                           | c'                 | c'
|                 |                           |                    |
∨                 ∨                           ∨                    ∨
X --------> Y     X --------> Y               Y                    Y ,
m                 m


which are required to be homotopic.

## Definitions

### Morphisms of coforks under morphisms of double arrows

module _
{l1 l2 l3 l4 l5 l6 : Level}
{a : double-arrow l1 l2} {X : UU l3} (c : cofork a X)
{a' : double-arrow l4 l5} {Y : UU l6} (c' : cofork a' Y)
(h : hom-double-arrow a a')
where

coherence-map-cofork-hom-cofork-hom-double-arrow : (X → Y) → UU (l2 ⊔ l6)
coherence-map-cofork-hom-cofork-hom-double-arrow u =
coherence-square-maps
( codomain-map-hom-double-arrow a a' h)
( map-cofork a c)
( map-cofork a' c')
( u)

coherence-hom-cofork-hom-double-arrow :
(u : X → Y) → coherence-map-cofork-hom-cofork-hom-double-arrow u →
UU (l1 ⊔ l6)
coherence-hom-cofork-hom-double-arrow u H =
( ( H ·r (left-map-double-arrow a)) ∙h
( ( map-cofork a' c') ·l
( left-square-hom-double-arrow a a' h)) ∙h
( (coh-cofork a' c') ·r (domain-map-hom-double-arrow a a' h))) ~
( ( u ·l (coh-cofork a c)) ∙h
( H ·r (right-map-double-arrow a)) ∙h
( (map-cofork a' c') ·l (right-square-hom-double-arrow a a' h)))

hom-cofork-hom-double-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l6)
hom-cofork-hom-double-arrow =
Σ ( X → Y)
( λ u →
Σ ( coherence-map-cofork-hom-cofork-hom-double-arrow u)
( coherence-hom-cofork-hom-double-arrow u))


### Components of a morphism of coforks under a morphism of double arrows

module _
{l1 l2 l3 l4 l5 l6 : Level}
{a : double-arrow l1 l2} {X : UU l3} (c : cofork a X)
{a' : double-arrow l4 l5} {Y : UU l6} (c' : cofork a' Y)
{h : hom-double-arrow a a'} (m : hom-cofork-hom-double-arrow c c' h)
where

map-hom-cofork-hom-double-arrow : X → Y
map-hom-cofork-hom-double-arrow = pr1 m

coh-map-cofork-hom-cofork-hom-double-arrow :
coherence-map-cofork-hom-cofork-hom-double-arrow c c' h
( map-hom-cofork-hom-double-arrow)
coh-map-cofork-hom-cofork-hom-double-arrow = pr1 (pr2 m)

hom-map-cofork-hom-cofork-hom-double-arrow :
hom-arrow (map-cofork a c) (map-cofork a' c')
pr1 hom-map-cofork-hom-cofork-hom-double-arrow =
codomain-map-hom-double-arrow a a' h
pr1 (pr2 hom-map-cofork-hom-cofork-hom-double-arrow) =
map-hom-cofork-hom-double-arrow
pr2 (pr2 hom-map-cofork-hom-cofork-hom-double-arrow) =
coh-map-cofork-hom-cofork-hom-double-arrow

coh-hom-cofork-hom-double-arrow :
coherence-hom-cofork-hom-double-arrow c c' h
( map-hom-cofork-hom-double-arrow)
( coh-map-cofork-hom-cofork-hom-double-arrow)
coh-hom-cofork-hom-double-arrow = pr2 (pr2 m)