The pullback property of pushouts

Content created by Egbert Rijke, Fredrik Bakke and Vojtěch Štěpančík.

Created on 2023-06-10.
Last modified on 2023-09-12.

module synthetic-homotopy-theory.pullback-property-pushouts where
Imports 
open import foundation.commuting-squares-of-maps
open import foundation.cones-over-cospans
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.pullbacks
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans

Idea

The universal property of the pushout of a span S can also be stated as a pullback property: a cocone c ≐ (i , j , H) with vertex X satisfies the universal property of the pushout of S if and only if the square

  Y^X -----> Y^B
   |          |
   |          |
   V          V
  Y^A -----> Y^S

is a pullback square for every type Y. Below, we first define the cone of this commuting square, and then we introduce the type pullback-property-pushout, which states that the above square is a pullback.

Definition

The pullback property of pushouts

cone-pullback-property-pushout :
  {l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (Y : UU l) →
  cone (_∘ f) (_∘ g) (X → Y)
pr1 (cone-pullback-property-pushout f g c Y) =
  precomp (horizontal-map-cocone f g c) Y
pr1 (pr2 (cone-pullback-property-pushout f g c Y)) =
  precomp (vertical-map-cocone f g c) Y
pr2 (pr2 (cone-pullback-property-pushout f g c Y)) =
  precomp-coherence-square-maps
    ( g)
    ( f)
    ( vertical-map-cocone f g c)
    ( horizontal-map-cocone f g c)
    ( coherence-square-cocone f g c)
    ( Y)

pullback-property-pushout :
  {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
pullback-property-pushout l f g c =
  (Y : UU l) →
  is-pullback
    ( precomp f Y)
    ( precomp g Y)
    ( cone-pullback-property-pushout f g c Y)

Recent changes