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