The category of maps and natural transformations between two categories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-27.
Last modified on 2023-11-21.

module category-theory.category-of-maps-categories where
Imports 
open import category-theory.categories
open import category-theory.commuting-squares-of-morphisms-in-precategories
open import category-theory.isomorphisms-in-categories
open import category-theory.isomorphisms-in-precategories
open import category-theory.maps-categories
open import category-theory.maps-precategories
open import category-theory.natural-isomorphisms-maps-categories
open import category-theory.natural-isomorphisms-maps-precategories
open import category-theory.natural-transformations-maps-precategories
open import category-theory.precategories
open import category-theory.precategory-of-maps-precategories

open import foundation.action-on-identifications-binary-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence
open import foundation.universe-levels

Idea

Maps between categories and natural transformations between them form another category whose identity map and composition structure are inherited pointwise from the codomain category. This is called the category of maps between categories.

Lemmas

Extensionality of maps 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-map-is-category-Precategory :
    (F G : map-Precategory C D) →
    ( htpy-map-Precategory C D F G) ≃
    ( natural-isomorphism-map-Precategory C D F G)
  equiv-natural-isomorphism-htpy-map-is-category-Precategory F G =
      ( equiv-right-swap-Σ) ∘e
      ( equiv-Σ-equiv-base
        ( is-natural-transformation-map-Precategory C D F G ∘ pr1)
        ( ( distributive-Π-Σ) ∘e
          ( equiv-Π-equiv-family
            ( λ x →
              extensionality-obj-Category
                ( D , is-category-D)
                ( obj-map-Precategory C D F x)
                ( obj-map-Precategory C D G x)))))

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

When the codomain is a category the map 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-map-precategory-is-category-Precategory :
      is-category-Precategory (map-precategory-Precategory C D)
    is-category-map-precategory-is-category-Precategory F G =
      is-equiv-htpy-equiv
        ( ( equiv-iso-map-natural-isomorphism-map-Precategory C D F G) ∘e
          ( extensionality-map-is-category-Precategory C D is-category-D F G))
        ( λ where
          refl →
            compute-iso-map-natural-isomorphism-map-eq-Precategory C D F G refl)

Definitions

The category of maps and natural transformations between categories

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

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

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

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

Recent changes