# Functors between large categories

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-17.

module category-theory.functors-large-categories where
Imports
open import category-theory.functors-large-precategories
open import category-theory.large-categories

open import foundation.identity-types
open import foundation.universe-levels

## Idea

A functor from a large category C to a large category D is a functor between the underlying large precategories 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

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.

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.

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)