This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The category of functors and natural transformations between two categories

module category-theory.category-of-functors where
Imports 
open import category-theory.categories
open import category-theory.category-of-maps-categories
open import category-theory.functors-categories
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-categories
open import category-theory.natural-isomorphisms-functors-categories
open import category-theory.natural-isomorphisms-functors-precategories
open import category-theory.precategories
open import category-theory.precategory-of-functors

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels

Idea

Functors between categories and natural transformations between them assemble to a new category whose identity functor and composition structure are inherited pointwise from the codomain category. This is called the category of functors.

Definitons

Extensionality of functors of precategories when the codomain is a category

module _
  {l1 l2 l3 l4 : Level}
  (C : Precategory l1 l2)
  (D : Precategory l3 l4)
  (is-category-D : is-category-Precategory D)
  where

  equiv-natural-isomorphism-htpy-functor-is-category-Precategory :
    (F G : functor-Precategory C D) →
    htpy-functor-Precategory C D F G ≃ natural-isomorphism-Precategory C D F G
  equiv-natural-isomorphism-htpy-functor-is-category-Precategory F G =
    equiv-natural-isomorphism-htpy-map-is-category-Precategory C D
      ( is-category-D)
      ( map-functor-Precategory C D F)
      ( map-functor-Precategory C D G)

  extensionality-functor-is-category-Precategory :
    (F G : functor-Precategory C D) →
    ( F ＝ G) ≃
    ( natural-isomorphism-Precategory C D F G)
  extensionality-functor-is-category-Precategory F G =
    ( equiv-natural-isomorphism-htpy-functor-is-category-Precategory F G) ∘e
    ( equiv-htpy-eq-functor-Precategory C D F G)

When the codomain is a category the functor precategory is a category

module _
  {l1 l2 l3 l4 : Level}
  (C : Precategory l1 l2)
  (D : Precategory l3 l4)
  (is-category-D : is-category-Precategory D)
  where

  abstract
    is-category-functor-precategory-is-category-Precategory :
      is-category-Precategory (functor-precategory-Precategory C D)
    is-category-functor-precategory-is-category-Precategory F G =
      is-equiv-htpy-equiv
        ( ( equiv-iso-functor-natural-isomorphism-Precategory C D F G) ∘e
          ( extensionality-functor-is-category-Precategory
              C D is-category-D F G))
        ( λ where
          refl →
            compute-iso-functor-natural-isomorphism-eq-Precategory C D F G refl)

Definitions

The category of functors and natural transformations between categories

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

  functor-category-Category :
    Category (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l2 ⊔ l4)
  pr1 functor-category-Category =
    functor-precategory-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
  pr2 functor-category-Category =
    is-category-functor-precategory-is-category-Precategory
      ( precategory-Category C)
      ( precategory-Category D)
      ( is-category-Category D)

  extensionality-functor-Category :
    (F G : functor-Category C D) →
    (F ＝ G) ≃ natural-isomorphism-Category C D F G
  extensionality-functor-Category F G =
    ( equiv-natural-isomorphism-iso-functor-Precategory
      ( precategory-Category C)
      ( precategory-Category D) F G) ∘e
    ( extensionality-obj-Category functor-category-Category F G)

  eq-natural-isomorphism-functor-Category :
    (F G : functor-Category C D) →
    natural-isomorphism-Category C D F G → F ＝ G
  eq-natural-isomorphism-functor-Category F G =
    map-inv-equiv (extensionality-functor-Category F G)