# Equivalences of coforks

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

Created on 2024-04-16.

module synthetic-homotopy-theory.equivalences-coforks-under-equivalences-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.equivalences
open import foundation.equivalences-arrows
open import foundation.equivalences-double-arrows
open import foundation.homotopies
open import foundation.morphisms-arrows
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import synthetic-homotopy-theory.coforks
open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows


## 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 an equivalence of double arrows e : (f, g) ≃ (h, k).

Then an equivalence of coforks under e is a triple (m, H, K), with m : X ≃ Y an equivalence 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

### Equivalences of coforks

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)
(e : equiv-double-arrow a a')
where

coherence-map-cofork-equiv-cofork-equiv-double-arrow : (X ≃ Y) → UU (l2 ⊔ l6)
coherence-map-cofork-equiv-cofork-equiv-double-arrow m =
coherence-square-maps
( codomain-map-equiv-double-arrow a a' e)
( map-cofork a c)
( map-cofork a' c')
( map-equiv m)

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

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

module _
(e' : equiv-cofork-equiv-double-arrow)
where

equiv-equiv-cofork-equiv-double-arrow : X ≃ Y
equiv-equiv-cofork-equiv-double-arrow = pr1 e'

map-equiv-cofork-equiv-double-arrow : X → Y
map-equiv-cofork-equiv-double-arrow =
map-equiv equiv-equiv-cofork-equiv-double-arrow

is-equiv-map-equiv-cofork-equiv-double-arrow :
is-equiv map-equiv-cofork-equiv-double-arrow
is-equiv-map-equiv-cofork-equiv-double-arrow =
is-equiv-map-equiv equiv-equiv-cofork-equiv-double-arrow

coh-map-cofork-equiv-cofork-equiv-double-arrow :
coherence-map-cofork-equiv-cofork-equiv-double-arrow
( equiv-equiv-cofork-equiv-double-arrow)
coh-map-cofork-equiv-cofork-equiv-double-arrow = pr1 (pr2 e')

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

hom-map-cofork-equiv-cofork-equiv-double-arrow :
hom-arrow (map-cofork a c) (map-cofork a' c')
hom-map-cofork-equiv-cofork-equiv-double-arrow =
hom-equiv-arrow
( map-cofork a c)
( map-cofork a' c')
( equiv-map-cofork-equiv-cofork-equiv-double-arrow)

coh-equiv-cofork-equiv-double-arrow :
coherence-equiv-cofork-equiv-double-arrow
( equiv-equiv-cofork-equiv-double-arrow)
( coh-map-cofork-equiv-cofork-equiv-double-arrow)
coh-equiv-cofork-equiv-double-arrow = pr2 (pr2 e')

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


### The predicate on morphisms of coforks under equivalences of double arrows of being an equivalence

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)
(e : equiv-double-arrow a a')
where

is-equiv-hom-cofork-equiv-double-arrow :
hom-cofork-hom-double-arrow c c' (hom-equiv-double-arrow a a' e) →
UU (l3 ⊔ l6)
is-equiv-hom-cofork-equiv-double-arrow h =
is-equiv
( map-hom-cofork-hom-double-arrow c c' h)

is-equiv-hom-equiv-cofork-equiv-double-arrow :
(e' : equiv-cofork-equiv-double-arrow c c' e) →
is-equiv-hom-cofork-equiv-double-arrow
( hom-equiv-cofork-equiv-double-arrow c c' e e')
is-equiv-hom-equiv-cofork-equiv-double-arrow e' =
is-equiv-map-equiv-cofork-equiv-double-arrow c c' e e'


## Properties

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

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

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)
(e : equiv-double-arrow a a')
where

equiv-hom-cofork-equiv-double-arrow :
(h : hom-cofork-hom-double-arrow c c' (hom-equiv-double-arrow a a' e)) →
is-equiv-hom-cofork-equiv-double-arrow c c' e h →
equiv-cofork-equiv-double-arrow c c' e
pr1 (equiv-hom-cofork-equiv-double-arrow h is-equiv-map-cofork) =
(map-hom-cofork-hom-double-arrow c c' h , is-equiv-map-cofork)
pr1 (pr2 (equiv-hom-cofork-equiv-double-arrow h _)) =
coh-map-cofork-hom-cofork-hom-double-arrow c c' h
pr2 (pr2 (equiv-hom-cofork-equiv-double-arrow h _)) =
coh-hom-cofork-hom-double-arrow c c' h