functor category

hom-set, hom-object, internal hom, exponential object, derived hom-space loop space object, free loop space object, derived loop space Given categories and , the functor category – written or – is the category whose morphisms are natural transformations between these functors. Discussion in homotopy type theory. Note: the HoTT book calls a internal category in HoTT a “precategory” and a univalent category a “category”, but here we shall refer to the standard terminology of “category” and...