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
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).