Functoriality of the pullback-hom

Content created by Egbert Rijke and Fredrik Bakke.

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

module orthogonal-factorization-systems.functoriality-pullback-hom where
Imports
open import foundation.function-types
open import foundation.functoriality-pullbacks
open import foundation.morphisms-arrows
open import foundation.morphisms-cospan-diagrams
open import foundation.postcomposition-functions
open import foundation.precomposition-functions
open import foundation.universe-levels

open import orthogonal-factorization-systems.pullback-hom

Idea

The construction of the pullback-hom is functorial.

Definition

Functorial action on maps of the pullback-hom

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

  map-pullback-hom :
    hom-cospan-diagram
      ( precomp f' Y')
      ( postcomp A' g')
      ( precomp f Y)
      ( postcomp A g) 
    hom-arrow f' g'  hom-arrow f g
  map-pullback-hom =
    map-is-pullback
      ( precomp f Y)
      ( postcomp A g)
      ( precomp f' Y')
      ( postcomp A' g')
      ( cone-hom-arrow-pullback-hom f g)
      ( cone-hom-arrow-pullback-hom f' g')
      ( is-pullback-cone-hom-arrow-pullback-hom f g)
      ( is-pullback-cone-hom-arrow-pullback-hom f' g')

Table of files about pullbacks

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

ConceptFile
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