# Functors between categories

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-03-11.

module category-theory.functors-categories where

Imports
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


## Idea

A functor between two categories is a functor between the underlying precategories.

## Definition

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

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

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.

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.

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.

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

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

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

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)