Functorialty of pullbacks

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-16.
Last modified on 2024-03-02.

module foundation.functoriality-pullbacks where
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospan-diagrams
open import foundation.dependent-pair-types
open import foundation.morphisms-cospan-diagrams
open import foundation.standard-pullbacks
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.pullbacks


The construction of the standard pullback is functorial.


The functorial action on maps of pullbacks

module _
  {l1 l2 l3 l1' l2' l3' : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} (f : A  X) (g : B  X)
  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A'  X') (g' : B'  X')

  map-standard-pullback :
    hom-cospan-diagram f' g' f g 
    standard-pullback f' g'  standard-pullback f g
  pr1 (map-standard-pullback (hA , _) (a' , _)) = hA a'
  pr1 (pr2 (map-standard-pullback (hA , hB , _) (a' , b' , _))) = hB b'
  pr2 (pr2 (map-standard-pullback (hA , hB , hX , HA , HB) (a' , b' , p'))) =
    HA a'  ap hX p'  inv (HB b')

  map-is-pullback :
    {l4 l4' : Level} {C : UU l4} {C' : UU l4'} 
    (c : cone f g C) (c' : cone f' g' C') 
    is-pullback f g c  is-pullback f' g' c' 
    hom-cospan-diagram f' g' f g  C'  C
  map-is-pullback c c' is-pb-c is-pb-c' h x =
    map-inv-is-equiv is-pb-c (map-standard-pullback h (gap f' g' c' x))

Table of files about pullbacks

The following table lists files that are about pullbacks as a general concept.

Cospan diagramsfoundation.cospans
Morphisms of cospan diagramsfoundation.morphisms-cospans
Cones over cospan diagramsfoundation.cones-over-cospan-diagrams
The universal property of pullbacks (foundation-core)foundation-core.universal-property-pullbacks
The universal property of pullbacks (foundation)foundation.universal-property-pullbacks
The universal property of fiber productsfoundation.universal-property-fiber-products
Standard pullbacksfoundation.standard-pullbacks
Pullbacks (foundation-core)foundation-core.pullbacks
Pullbacks (foundation)foundation.pullbacks
Functoriality of pullbacksfoundation.functoriality-pullbacks
Cartesian morphisms of arrowsfoundation.cartesian-morphisms-arrows
Dependent products of pullbacksfoundation.dependent-products-pullbacks
Dependent sums of pullbacksfoundation.dependent-sums-pullbacks
Products of pullbacksfoundation.products-pullbacks
Coroducts of pullbacksfoundation.coproducts-pullbacks
Postcomposition of pullbacksfoundation.postcomposition-pullbacks
Pullbacks of subtypesfoundation.pullbacks-subtypes
The pullback-homorthogonal-factorization-systems.pullback-hom
Functoriality of the pullback-homorthogonal-factorization-systems.functoriality-pullback-hom
Pullbacks in precategoriescategory-theory.pullbacks-in-precategories

Recent changes