Homotopies of natural transformations in large precategories
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Bonnevier.
Created on 2022-03-11.
Last modified on 2023-09-27.
module category-theory.homotopies-natural-transformations-large-precategories where
Imports
open import category-theory.functors-large-precategories open import category-theory.large-precategories open import category-theory.natural-transformations-functors-large-precategories open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels
Idea
Two
natural transformations
α β : F ⇒ G
are homotopic if for every object x
there is an
identification α x = β x
.
In UUω
the usual identity type is not available. If it were, we would be able
to characterize the identity type of natural transformations from F
to G
as
the type of homotopies of natural transformations.
Definitions
Homotopies of natural transformations
module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} {F : functor-Large-Precategory C D γF} {G : functor-Large-Precategory C D γG} where htpy-natural-transformation-Large-Precategory : (α β : natural-transformation-Large-Precategory F G) → UUω htpy-natural-transformation-Large-Precategory α β = { l : Level} (X : obj-Large-Precategory C l) → ( hom-family-natural-transformation-Large-Precategory α X) = ( hom-family-natural-transformation-Large-Precategory β X)
The reflexivity homotopy
module _ {αC αD γF γG : Level → Level} {βC βD : Level → Level → Level} {C : Large-Precategory αC βC} {D : Large-Precategory αD βD} {F : functor-Large-Precategory C D γF} {G : functor-Large-Precategory C D γG} where refl-htpy-natural-transformation-Large-Precategory : (α : natural-transformation-Large-Precategory F G) → htpy-natural-transformation-Large-Precategory α α refl-htpy-natural-transformation-Large-Precategory α = refl-htpy
Concatenation of homotopies
A homotopy from α
to β
can be concatenated with a homotopy from β
to γ
to form a homotopy from α
to γ
. The concatenation is associative.
concat-htpy-natural-transformation-Large-Precategory : (α β γ : natural-transformation-Large-Precategory F G) → htpy-natural-transformation-Large-Precategory α β → htpy-natural-transformation-Large-Precategory β γ → htpy-natural-transformation-Large-Precategory α γ concat-htpy-natural-transformation-Large-Precategory α β γ H K = H ∙h K associative-concat-htpy-natural-transformation-Large-Precategory : (α β γ δ : natural-transformation-Large-Precategory F G) (H : htpy-natural-transformation-Large-Precategory α β) (K : htpy-natural-transformation-Large-Precategory β γ) (L : htpy-natural-transformation-Large-Precategory γ δ) → {l : Level} (X : obj-Large-Precategory C l) → ( concat-htpy-natural-transformation-Large-Precategory α γ δ ( concat-htpy-natural-transformation-Large-Precategory α β γ H K) ( L) ( X)) = ( concat-htpy-natural-transformation-Large-Precategory α β δ ( H) ( concat-htpy-natural-transformation-Large-Precategory β γ δ K L) ( X)) associative-concat-htpy-natural-transformation-Large-Precategory α β γ δ H K L = assoc-htpy H K L
Recent changes
- 2023-09-27. Fredrik Bakke. Presheaf categories (#801).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-05-06. Egbert Rijke. Big cleanup continued (#597).
- 2023-03-23. Fredrik Bakke. Some additions to and refactoring large types (#529).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).