# Cocartesian morphisms of arrows

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-30.

module synthetic-homotopy-theory.cocartesian-morphisms-arrows where

Imports
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.morphisms-arrows
open import foundation.propositions
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.universal-property-pushouts


## Idea

A morphism of arrows h : f → g is said to be cocartesian if the commuting square

        i
A -----> X
|        |
f |   h    | g
∨        ∨
B -----> Y
j


is a pushout square. In this instance, we also say that g is a cobase change of f.

## Definitions

### The predicate of being a cocartesian morphism of arrows

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (h : hom-arrow f g)
where

is-cocartesian-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-cocartesian-hom-arrow =
is-pushout f (map-domain-hom-arrow f g h) (cocone-hom-arrow f g h)

is-prop-is-cocartesian-hom-arrow : is-prop is-cocartesian-hom-arrow
is-prop-is-cocartesian-hom-arrow =
is-prop-is-pushout f (map-domain-hom-arrow f g h) (cocone-hom-arrow f g h)

is-cocartesian-hom-arrow-Prop : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
pr1 is-cocartesian-hom-arrow-Prop = is-cocartesian-hom-arrow
pr2 is-cocartesian-hom-arrow-Prop = is-prop-is-cocartesian-hom-arrow


### The type of cocartesian morphisms of arrows

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y)
where

cocartesian-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
cocartesian-hom-arrow = Σ (hom-arrow f g) (is-cocartesian-hom-arrow f g)

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
(f : A → B) (g : X → Y) (h : cocartesian-hom-arrow f g)
where

hom-arrow-cocartesian-hom-arrow : hom-arrow f g
hom-arrow-cocartesian-hom-arrow = pr1 h

is-cocartesian-cocartesian-hom-arrow :
is-cocartesian-hom-arrow f g hom-arrow-cocartesian-hom-arrow
is-cocartesian-cocartesian-hom-arrow = pr2 h

map-domain-cocartesian-hom-arrow : A → X
map-domain-cocartesian-hom-arrow =
map-domain-hom-arrow f g hom-arrow-cocartesian-hom-arrow

map-codomain-cocartesian-hom-arrow : B → Y
map-codomain-cocartesian-hom-arrow =
map-codomain-hom-arrow f g hom-arrow-cocartesian-hom-arrow

coh-cocartesian-hom-arrow :
coherence-square-maps
( map-domain-cocartesian-hom-arrow)
( f)
( g)
( map-codomain-cocartesian-hom-arrow)
coh-cocartesian-hom-arrow =
coh-hom-arrow f g hom-arrow-cocartesian-hom-arrow

cocone-cocartesian-hom-arrow :
cocone f map-domain-cocartesian-hom-arrow Y
cocone-cocartesian-hom-arrow =
cocone-hom-arrow f g hom-arrow-cocartesian-hom-arrow

universal-property-cocartesian-hom-arrow :
universal-property-pushout
( f)
( map-domain-cocartesian-hom-arrow)
( cocone-cocartesian-hom-arrow)
universal-property-cocartesian-hom-arrow =
universal-property-pushout-is-pushout
( f)
( map-domain-cocartesian-hom-arrow)
( cocone-cocartesian-hom-arrow)
( is-cocartesian-cocartesian-hom-arrow)