# Functors between large precategories

```agda
module category-theory.functors-large-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.large-precategories

open import foundation.action-on-identifications-functions
open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels
```

</details>

## Idea

A **functor** from a [large precategory](category-theory.large-precategories.md)
`C` to a large precategory `D` consists 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-Precategory αC βC) (D : Large-Precategory αD βD)
  where

  record functor-Large-Precategory : UUω
    where
    constructor make-functor
    field
      obj-functor-Large-Precategory :
        { l1 : Level} →
        obj-Large-Precategory C l1 → obj-Large-Precategory D (γ l1)
      hom-functor-Large-Precategory :
        { l1 l2 : Level}
        { X : obj-Large-Precategory C l1}
        { Y : obj-Large-Precategory C l2} →
        hom-Large-Precategory C X Y →
        hom-Large-Precategory D
          ( obj-functor-Large-Precategory X)
          ( obj-functor-Large-Precategory Y)
      preserves-comp-functor-Large-Precategory :
        { l1 l2 l3 : Level}
        { X : obj-Large-Precategory C l1}
        { Y : obj-Large-Precategory C l2}
        { Z : obj-Large-Precategory C l3}
        ( g : hom-Large-Precategory C Y Z)
        ( f : hom-Large-Precategory C X Y) →
        ( hom-functor-Large-Precategory
          ( comp-hom-Large-Precategory C g f)) ＝
        ( comp-hom-Large-Precategory D
          ( hom-functor-Large-Precategory g)
          ( hom-functor-Large-Precategory f))
      preserves-id-functor-Large-Precategory :
        { l1 : Level} {X : obj-Large-Precategory C l1} →
        ( hom-functor-Large-Precategory
          ( id-hom-Large-Precategory C {X = X})) ＝
        ( id-hom-Large-Precategory D {X = obj-functor-Large-Precategory X})

  open functor-Large-Precategory public
```

### The identity functor

```agda
id-functor-Large-Precategory :
  {αC : Level → Level} {βC : Level → Level → Level} →
  (C : Large-Precategory αC βC) →
  functor-Large-Precategory (λ l → l) C C
obj-functor-Large-Precategory
  ( id-functor-Large-Precategory C) =
  id
hom-functor-Large-Precategory
  ( id-functor-Large-Precategory C) =
  id
preserves-comp-functor-Large-Precategory
  ( id-functor-Large-Precategory C) g f =
  refl
preserves-id-functor-Large-Precategory
  ( id-functor-Large-Precategory C) =
  refl
```

### Composition of functors

```agda
module _
  {αC αD αE γG γF : Level → Level}
  {βC βD βE : Level → Level → Level}
  (C : Large-Precategory αC βC)
  (D : Large-Precategory αD βD)
  (E : Large-Precategory αE βE)
  (G : functor-Large-Precategory γG D E)
  (F : functor-Large-Precategory γF C D)
  where

  obj-comp-functor-Large-Precategory :
    {l1 : Level} →
    obj-Large-Precategory C l1 → obj-Large-Precategory E (γG (γF l1))
  obj-comp-functor-Large-Precategory =
    obj-functor-Large-Precategory G ∘ obj-functor-Large-Precategory F

  hom-comp-functor-Large-Precategory :
    {l1 l2 : Level}
    {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} →
    hom-Large-Precategory C X Y →
    hom-Large-Precategory E
      ( obj-comp-functor-Large-Precategory X)
      ( obj-comp-functor-Large-Precategory Y)
  hom-comp-functor-Large-Precategory =
    hom-functor-Large-Precategory G ∘ hom-functor-Large-Precategory F

  preserves-comp-comp-functor-Large-Precategory :
    {l1 l2 l3 : Level}
    {X : obj-Large-Precategory C l1}
    {Y : obj-Large-Precategory C l2}
    {Z : obj-Large-Precategory C l3}
    (g : hom-Large-Precategory C Y Z) (f : hom-Large-Precategory C X Y) →
    hom-comp-functor-Large-Precategory
      ( comp-hom-Large-Precategory C g f) ＝
    comp-hom-Large-Precategory E
      ( hom-comp-functor-Large-Precategory g)
      ( hom-comp-functor-Large-Precategory f)
  preserves-comp-comp-functor-Large-Precategory g f =
    ( ap
      ( hom-functor-Large-Precategory G)
      ( preserves-comp-functor-Large-Precategory F g f)) ∙
    ( preserves-comp-functor-Large-Precategory G
      ( hom-functor-Large-Precategory F g)
      ( hom-functor-Large-Precategory F f))

  preserves-id-comp-functor-Large-Precategory :
    {l1 : Level} {X : obj-Large-Precategory C l1} →
    hom-comp-functor-Large-Precategory (id-hom-Large-Precategory C {X = X}) ＝
    id-hom-Large-Precategory E
  preserves-id-comp-functor-Large-Precategory =
    ( ap
      ( hom-functor-Large-Precategory G)
      ( preserves-id-functor-Large-Precategory F)) ∙
    ( preserves-id-functor-Large-Precategory G)

  comp-functor-Large-Precategory :
    functor-Large-Precategory (λ l → γG (γF l)) C E
  obj-functor-Large-Precategory
    comp-functor-Large-Precategory =
    obj-comp-functor-Large-Precategory
  hom-functor-Large-Precategory
    comp-functor-Large-Precategory =
    hom-comp-functor-Large-Precategory
  preserves-comp-functor-Large-Precategory
    comp-functor-Large-Precategory =
    preserves-comp-comp-functor-Large-Precategory
  preserves-id-functor-Large-Precategory
    comp-functor-Large-Precategory =
    preserves-id-comp-functor-Large-Precategory
```