# Homotopies of natural transformations in large precategories

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Stenholm.

Created on 2022-03-11.

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 γF C D}
{G : functor-Large-Precategory γG C D}
where

htpy-natural-transformation-Large-Precategory :
(σ τ : natural-transformation-Large-Precategory C D F G) → UUω
htpy-natural-transformation-Large-Precategory σ τ =
{ l : Level} (X : obj-Large-Precategory C l) →
( hom-natural-transformation-Large-Precategory σ X) ＝
( hom-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 γF C D}
{G : functor-Large-Precategory γG C D}
where

refl-htpy-natural-transformation-Large-Precategory :
(α : natural-transformation-Large-Precategory C D F G) →
htpy-natural-transformation-Large-Precategory C D α α
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.

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 γF C D}
{G : functor-Large-Precategory γG C D}
where

concat-htpy-natural-transformation-Large-Precategory :
(σ τ υ : natural-transformation-Large-Precategory C D F G) →
htpy-natural-transformation-Large-Precategory C D σ τ →
htpy-natural-transformation-Large-Precategory C D τ υ →
htpy-natural-transformation-Large-Precategory C D σ υ
concat-htpy-natural-transformation-Large-Precategory σ τ υ H K = H ∙h K

associative-concat-htpy-natural-transformation-Large-Precategory :
(σ τ υ ϕ : natural-transformation-Large-Precategory C D F G)
(H : htpy-natural-transformation-Large-Precategory C D σ τ)
(K : htpy-natural-transformation-Large-Precategory C D τ υ)
(L : htpy-natural-transformation-Large-Precategory C D υ ϕ) →
{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