# Functors between categories

```agda
module category-theory.functors-categories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.categories
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-categories
open import category-theory.maps-categories

open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels
```

</details>

## Idea

A **functor** between two [categories](category-theory.categories.md) is a
[functor](category-theory.functors-precategories.md) between the underlying
[precategories](category-theory.precategories.md).

## Definition

### The predicate of being a functor on maps between categories

```agda
module _
  {l1 l2 l3 l4 : Level}
  (C : Category l1 l2)
  (D : Category l3 l4)
  (F : map-Category C D)
  where

  preserves-comp-hom-map-Category : UU (l1  l2  l4)
  preserves-comp-hom-map-Category =
    preserves-comp-hom-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  preserves-id-hom-map-Category : UU (l1  l4)
  preserves-id-hom-map-Category =
    preserves-id-hom-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  is-functor-map-Category : UU (l1  l2  l4)
  is-functor-map-Category =
    is-functor-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  preserves-comp-is-functor-map-Category :
    is-functor-map-Category  preserves-comp-hom-map-Category
  preserves-comp-is-functor-map-Category =
    preserves-comp-is-functor-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  preserves-id-is-functor-map-Category :
    is-functor-map-Category  preserves-id-hom-map-Category
  preserves-id-is-functor-map-Category =
    preserves-id-is-functor-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)
```

### functors between categories

```agda
module _
  {l1 l2 l3 l4 : Level}
  (C : Category l1 l2)
  (D : Category l3 l4)
  where

  functor-Category : UU (l1  l2  l3  l4)
  functor-Category =
    functor-Precategory (precategory-Category C) (precategory-Category D)

  obj-functor-Category : functor-Category  obj-Category C  obj-Category D
  obj-functor-Category =
    obj-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)

  hom-functor-Category :
    (F : functor-Category) 
    {x y : obj-Category C} 
    (f : hom-Category C x y) 
    hom-Category D
      ( obj-functor-Category F x)
      ( obj-functor-Category F y)
  hom-functor-Category =
    hom-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)

  map-functor-Category : functor-Category  map-Category C D
  map-functor-Category =
    map-functor-Precategory (precategory-Category C) (precategory-Category D)

  is-functor-functor-Category :
    (F : functor-Category) 
    is-functor-map-Category C D (map-functor-Category F)
  is-functor-functor-Category =
    is-functor-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)

  preserves-comp-functor-Category :
    ( F : functor-Category) {x y z : obj-Category C}
    ( g : hom-Category C y z) (f : hom-Category C x y) 
    ( hom-functor-Category F (comp-hom-Category C g f)) 
    ( comp-hom-Category D
      ( hom-functor-Category F g)
      ( hom-functor-Category F f))
  preserves-comp-functor-Category =
    preserves-comp-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)

  preserves-id-functor-Category :
    (F : functor-Category) (x : obj-Category C) 
    hom-functor-Category F (id-hom-Category C {x}) 
    id-hom-Category D {obj-functor-Category F x}
  preserves-id-functor-Category =
    preserves-id-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
```

## Examples

### The identity functor

There is an identity functor on any category.

```agda
id-functor-Category :
  {l1 l2 : Level} (C : Category l1 l2)  functor-Category C C
id-functor-Category C = id-functor-Precategory (precategory-Category C)
```

### Composition of functors

Any two compatible functors can be composed to a new functor.

```agda
comp-functor-Category :
  {l1 l2 l3 l4 l5 l6 : Level}
  (C : Category l1 l2) (D : Category l3 l4) (E : Category l5 l6) 
  functor-Category D E  functor-Category C D  functor-Category C E
comp-functor-Category C D E =
  comp-functor-Precategory
    ( precategory-Category C)
    ( precategory-Category D)
    ( precategory-Category E)
```

## Properties

### Respecting identities and compositions are propositions

This follows from the fact that the hom-types are
[sets](foundation-core.sets.md).

```agda
module _
  {l1 l2 l3 l4 : Level}
  (C : Category l1 l2)
  (D : Category l3 l4)
  (F : map-Category C D)
  where

  is-prop-preserves-comp-hom-map-Category :
    is-prop (preserves-comp-hom-map-Category C D F)
  is-prop-preserves-comp-hom-map-Category =
    is-prop-preserves-comp-hom-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  preserves-comp-hom-prop-map-Category : Prop (l1  l2  l4)
  preserves-comp-hom-prop-map-Category =
    preserves-comp-hom-prop-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  is-prop-preserves-id-hom-map-Category :
    is-prop (preserves-id-hom-map-Category C D F)
  is-prop-preserves-id-hom-map-Category =
    is-prop-preserves-id-hom-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  preserves-id-hom-prop-map-Category : Prop (l1  l4)
  preserves-id-hom-prop-map-Category =
    preserves-id-hom-prop-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  is-prop-is-functor-map-Category :
    is-prop (is-functor-map-Category C D F)
  is-prop-is-functor-map-Category =
    is-prop-is-functor-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  is-functor-prop-map-Category : Prop (l1  l2  l4)
  is-functor-prop-map-Category =
    is-functor-prop-map-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)
```

### Extensionality of functors between categories

#### Equality of functors is equality of underlying maps

```agda
module _
  {l1 l2 l3 l4 : Level}
  (C : Category l1 l2)
  (D : Category l3 l4)
  (F G : functor-Category C D)
  where

  equiv-eq-map-eq-functor-Category :
    (F  G)  (map-functor-Category C D F  map-functor-Category C D G)
  equiv-eq-map-eq-functor-Category =
    equiv-eq-map-eq-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)
      ( G)

  eq-map-eq-functor-Category :
    (F  G)  (map-functor-Category C D F  map-functor-Category C D G)
  eq-map-eq-functor-Category =
    map-equiv equiv-eq-map-eq-functor-Category

  eq-eq-map-functor-Category :
    (map-functor-Category C D F  map-functor-Category C D G)  (F  G)
  eq-eq-map-functor-Category =
    map-inv-equiv equiv-eq-map-eq-functor-Category

  is-section-eq-eq-map-functor-Category :
    eq-map-eq-functor-Category  eq-eq-map-functor-Category ~ id
  is-section-eq-eq-map-functor-Category =
    is-section-map-inv-equiv equiv-eq-map-eq-functor-Category

  is-retraction-eq-eq-map-functor-Category :
    eq-eq-map-functor-Category  eq-map-eq-functor-Category ~ id
  is-retraction-eq-eq-map-functor-Category =
    is-retraction-map-inv-equiv equiv-eq-map-eq-functor-Category
```

#### Equality of functors is homotopy of underlying maps

```agda
module _
  {l1 l2 l3 l4 : Level}
  (C : Category l1 l2)
  (D : Category l3 l4)
  (F G : functor-Category C D)
  where

  htpy-functor-Category : UU (l1  l2  l3  l4)
  htpy-functor-Category =
    htpy-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)
      ( G)

  equiv-htpy-eq-functor-Category : (F  G)  htpy-functor-Category
  equiv-htpy-eq-functor-Category =
    equiv-htpy-eq-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)
      ( G)

  htpy-eq-functor-Category : F  G  htpy-functor-Category
  htpy-eq-functor-Category =
    map-equiv equiv-htpy-eq-functor-Category

  eq-htpy-functor-Category : htpy-functor-Category  F  G
  eq-htpy-functor-Category =
    map-inv-equiv equiv-htpy-eq-functor-Category

  is-section-eq-htpy-functor-Category :
    htpy-eq-functor-Category  eq-htpy-functor-Category ~ id
  is-section-eq-htpy-functor-Category =
    is-section-map-inv-equiv equiv-htpy-eq-functor-Category

  is-retraction-eq-htpy-functor-Category :
    eq-htpy-functor-Category  htpy-eq-functor-Category ~ id
  is-retraction-eq-htpy-functor-Category =
    is-retraction-map-inv-equiv equiv-htpy-eq-functor-Category
```

### Functors preserve isomorphisms

```agda
module _
  {l1 l2 l3 l4 : Level}
  (C : Category l1 l2)
  (D : Category l3 l4)
  (F : functor-Category C D)
  {x y : obj-Category C}
  where

  preserves-is-iso-functor-Category :
    (f : hom-Category C x y) 
    is-iso-Category C f 
    is-iso-Category D (hom-functor-Category C D F f)
  preserves-is-iso-functor-Category =
    preserves-is-iso-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)

  preserves-iso-functor-Category :
    iso-Category C x y 
    iso-Category D
      ( obj-functor-Category C D F x)
      ( obj-functor-Category C D F y)
  preserves-iso-functor-Category =
    preserves-iso-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( F)
```

## See also

- [The category of functors and natural transformations between categories](category-theory.category-of-functors.md)