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.
Recent changes
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-28. Egbert Rijke. Span diagrams (#1007).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-10-16. Fredrik Bakke and Egbert Rijke. Sequential limits (#839).