# Functors between large categories ```agda module category-theory.functors-large-categories where ``` <details><summary>Imports</summary> ```agda open import category-theory.functors-large-precategories open import category-theory.large-categories open import foundation.identity-types open import foundation.universe-levels ``` </details> ## Idea A **functor** from a [large category](category-theory.large-categories.md) `C` to a large category `D` is a [functor](category-theory.functors-large-precategories.md) between the underlying [large precategories](category-theory.large-precategories.md) of `C` and `D`. In other words, functors of large categories consist of: - a map `F₀ : C → D` on objects, - a map `F₁ : hom x y → hom (F₀ x) (F₀ y)` on morphisms, such that the following identities hold: - `F id_x = id_(F x)`, - `F (g ∘ f) = F g ∘ F f`. ## Definition ```agda module _ {αC αD : Level → Level} {βC βD : Level → Level → Level} (γ : Level → Level) (C : Large-Category αC βC) (D : Large-Category αD βD) where functor-Large-Category : UUω functor-Large-Category = functor-Large-Precategory γ ( large-precategory-Large-Category C) ( large-precategory-Large-Category D) module _ {αC αD : Level → Level} {βC βD : Level → Level → Level} {γ : Level → Level} (C : Large-Category αC βC) (D : Large-Category αD βD) (F : functor-Large-Category γ C D) where obj-functor-Large-Category : {l1 : Level} → obj-Large-Category C l1 → obj-Large-Category D (γ l1) obj-functor-Large-Category = obj-functor-Large-Precategory F hom-functor-Large-Category : {l1 l2 : Level} {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2} → hom-Large-Category C X Y → hom-Large-Category D ( obj-functor-Large-Category X) ( obj-functor-Large-Category Y) hom-functor-Large-Category = hom-functor-Large-Precategory F preserves-id-functor-Large-Category : {l1 : Level} {X : obj-Large-Category C l1} → hom-functor-Large-Category (id-hom-Large-Category C {X = X}) = id-hom-Large-Category D preserves-id-functor-Large-Category = preserves-id-functor-Large-Precategory F preserves-comp-functor-Large-Category : {l1 l2 l3 : Level} {X : obj-Large-Category C l1} {Y : obj-Large-Category C l2} {Z : obj-Large-Category C l3} (g : hom-Large-Category C Y Z) (f : hom-Large-Category C X Y) → hom-functor-Large-Category (comp-hom-Large-Category C g f) = comp-hom-Large-Category D ( hom-functor-Large-Category g) ( hom-functor-Large-Category f) preserves-comp-functor-Large-Category = preserves-comp-functor-Large-Precategory F ``` ### The identity functor There is an identity functor on any large category. ```agda id-functor-Large-Category : {αC : Level → Level} {βC : Level → Level → Level} → (C : Large-Category αC βC) → functor-Large-Category (λ l → l) C C id-functor-Large-Category C = id-functor-Large-Precategory (large-precategory-Large-Category C) ``` ### Composition of functors Any two compatible functors can be composed to a new functor. ```agda comp-functor-Large-Category : {αC αD αE γG γF : Level → Level} {βC βD βE : Level → Level → Level} → (C : Large-Category αC βC) (D : Large-Category αD βD) (E : Large-Category αE βE) → functor-Large-Category γG D E → functor-Large-Category γF C D → functor-Large-Category (λ l → γG (γF l)) C E comp-functor-Large-Category C D E = comp-functor-Large-Precategory ( large-precategory-Large-Category C) ( large-precategory-Large-Category D) ( large-precategory-Large-Category E) ```