Cocartesian morphisms of arrows

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-30.
Last modified on 2024-04-25.

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)

See also

Recent changes