The dependent pullback property of pushouts

Content created by Fredrik Bakke and Egbert Rijke.

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

module synthetic-homotopy-theory.dependent-pullback-property-pushouts where
Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.cones-over-cospans
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.pullbacks
open import foundation.transport-along-identifications
open import foundation.universe-levels

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

Idea

The fact that the dependent pullback property of pushouts is logically equivalent to the dependent universal property of pushouts is shown in dependent-universal-property-pushouts.

Definition

cone-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S  A) (g : S  B) {X : UU l4} (c : cocone f g X) (P : X  UU l5) 
  let i = pr1 c
      j = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  cone
    ( λ (h : (a : A)  P (i a))  λ (s : S)  tr P (H s) (h (f s)))
    ( λ (h : (b : B)  P (j b))  λ s  h (g s))
    ( (x : X)  P x)
pr1 (cone-dependent-pullback-property-pushout f g (i , j , H) P) h a =
  h (i a)
pr1 (pr2 (cone-dependent-pullback-property-pushout f g (i , j , H) P)) h b =
  h (j b)
pr2 (pr2 (cone-dependent-pullback-property-pushout f g (i , j , H) P)) h =
  eq-htpy  s  apd h (H s))

dependent-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)
dependent-pullback-property-pushout l {S} {A} {B} f g {X} (i , j , H) =
  (P : X  UU l) 
  is-pullback
    ( λ (h : (a : A)  P (i a))  λ s  tr P (H s) (h (f s)))
    ( λ (h : (b : B)  P (j b))  λ s  h (g s))
    ( cone-dependent-pullback-property-pushout f g (i , j , H) P)

Recent changes