The precategory of functors and natural transformations between two precategories

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke, Daniel Gratzer and Fernando Chu.

Created on 2023-01-16.
Last modified on 2024-09-01.

module category-theory.precategory-of-functors where
Imports 
open import category-theory.composition-operations-on-binary-families-of-sets
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.natural-isomorphisms-functors-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.precategories

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.strictly-involutive-identity-types
open import foundation.universe-levels

Idea

Functors between precategories and natural transformations between them introduce a new precategory whose identity map and composition structure are inherited pointwise from the codomain precategory. This is called the precategory of functors.

Definitions

The precategory of functors and natural transformations between precategories

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

  comp-hom-functor-precategory-Precategory :
    {F G H : functor-Precategory C D} →
    natural-transformation-Precategory C D G H →
    natural-transformation-Precategory C D F G →
    natural-transformation-Precategory C D F H
  comp-hom-functor-precategory-Precategory {F} {G} {H} =
    comp-natural-transformation-Precategory C D F G H

  associative-comp-hom-functor-precategory-Precategory :
    {F G H I : functor-Precategory C D}
    (h : natural-transformation-Precategory C D H I)
    (g : natural-transformation-Precategory C D G H)
    (f : natural-transformation-Precategory C D F G) →
    comp-natural-transformation-Precategory C D F G I
      ( comp-natural-transformation-Precategory C D G H I h g)
      ( f) ＝
    comp-natural-transformation-Precategory C D F H I
      ( h)
      ( comp-natural-transformation-Precategory C D F G H g f)
  associative-comp-hom-functor-precategory-Precategory {F} {G} {H} {I} h g f =
    associative-comp-natural-transformation-Precategory
      C D F G H I f g h

  involutive-eq-associative-comp-hom-functor-precategory-Precategory :
    {F G H I : functor-Precategory C D}
    (h : natural-transformation-Precategory C D H I)
    (g : natural-transformation-Precategory C D G H)
    (f : natural-transformation-Precategory C D F G) →
    comp-natural-transformation-Precategory C D F G I
      ( comp-natural-transformation-Precategory C D G H I h g)
      ( f) ＝ⁱ
    comp-natural-transformation-Precategory C D F H I
      ( h)
      ( comp-natural-transformation-Precategory C D F G H g f)
  involutive-eq-associative-comp-hom-functor-precategory-Precategory
    { F} {G} {H} {I} h g f =
    involutive-eq-associative-comp-natural-transformation-Precategory
      C D F G H I f g h

  associative-composition-operation-functor-precategory-Precategory :
    associative-composition-operation-binary-family-Set
      ( natural-transformation-set-Precategory C D)
  pr1 associative-composition-operation-functor-precategory-Precategory
    {F} {G} {H} =
    comp-hom-functor-precategory-Precategory {F} {G} {H}
  pr2
    associative-composition-operation-functor-precategory-Precategory
      { F} {G} {H} {I} h g f =
    involutive-eq-associative-comp-hom-functor-precategory-Precategory
      { F} {G} {H} {I} h g f

  id-hom-functor-precategory-Precategory :
    (F : functor-Precategory C D) → natural-transformation-Precategory C D F F
  id-hom-functor-precategory-Precategory =
    id-natural-transformation-Precategory C D

  left-unit-law-comp-hom-functor-precategory-Precategory :
    {F G : functor-Precategory C D}
    (α : natural-transformation-Precategory C D F G) →
    comp-natural-transformation-Precategory C D F G G
      ( id-natural-transformation-Precategory C D G) α ＝
    α
  left-unit-law-comp-hom-functor-precategory-Precategory {F} {G} =
    left-unit-law-comp-natural-transformation-Precategory C D F G

  right-unit-law-comp-hom-functor-precategory-Precategory :
    {F G : functor-Precategory C D}
    (α : natural-transformation-Precategory C D F G) →
    comp-natural-transformation-Precategory C D F F G
        α (id-natural-transformation-Precategory C D F) ＝
    α
  right-unit-law-comp-hom-functor-precategory-Precategory {F} {G} =
    right-unit-law-comp-natural-transformation-Precategory C D F G

  is-unital-composition-operation-functor-precategory-Precategory :
    is-unital-composition-operation-binary-family-Set
      ( natural-transformation-set-Precategory C D)
      ( λ {F} {G} {H} → comp-hom-functor-precategory-Precategory {F} {G} {H})
  pr1 is-unital-composition-operation-functor-precategory-Precategory =
    id-hom-functor-precategory-Precategory
  pr1
    ( pr2 is-unital-composition-operation-functor-precategory-Precategory)
    { F} {G} =
    left-unit-law-comp-hom-functor-precategory-Precategory {F} {G}
  pr2
    ( pr2 is-unital-composition-operation-functor-precategory-Precategory)
    { F} {G} =
    right-unit-law-comp-hom-functor-precategory-Precategory {F} {G}

  functor-precategory-Precategory :
    Precategory (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l2 ⊔ l4)
  pr1 functor-precategory-Precategory = functor-Precategory C D
  pr1 (pr2 functor-precategory-Precategory) =
    natural-transformation-set-Precategory C D
  pr1 (pr2 (pr2 functor-precategory-Precategory)) =
    associative-composition-operation-functor-precategory-Precategory
  pr2 (pr2 (pr2 functor-precategory-Precategory)) =
    is-unital-composition-operation-functor-precategory-Precategory

Properties

Isomorphisms in the functor precategory are natural isomorphisms

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

  is-iso-functor-is-natural-isomorphism-Precategory :
    (f : natural-transformation-Precategory C D F G) →
    is-natural-isomorphism-Precategory C D F G f →
    is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f
  pr1 (is-iso-functor-is-natural-isomorphism-Precategory f is-iso-f) =
    natural-transformation-inv-is-natural-isomorphism-Precategory
      C D F G f is-iso-f
  pr1 (pr2 (is-iso-functor-is-natural-isomorphism-Precategory f is-iso-f)) =
    is-section-natural-transformation-inv-is-natural-isomorphism-Precategory
      C D F G f is-iso-f
  pr2 (pr2 (is-iso-functor-is-natural-isomorphism-Precategory f is-iso-f)) =
    is-retraction-natural-transformation-inv-is-natural-isomorphism-Precategory
      C D F G f is-iso-f

  is-natural-isomorphism-is-iso-functor-Precategory :
    (f : natural-transformation-Precategory C D F G) →
    is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f →
    is-natural-isomorphism-Precategory C D F G f
  pr1 (is-natural-isomorphism-is-iso-functor-Precategory f is-iso-f x) =
    hom-family-natural-transformation-Precategory C D G F
      ( hom-inv-is-iso-Precategory
        ( functor-precategory-Precategory C D) {F} {G} is-iso-f)
      ( x)
  pr1 (pr2 (is-natural-isomorphism-is-iso-functor-Precategory f is-iso-f x)) =
    htpy-eq
      ( ap
        ( hom-family-natural-transformation-Precategory C D G G)
        ( is-section-hom-inv-is-iso-Precategory
          ( functor-precategory-Precategory C D) {F} {G} is-iso-f))
      ( x)
  pr2 (pr2 (is-natural-isomorphism-is-iso-functor-Precategory f is-iso-f x)) =
    htpy-eq
      ( ap
        ( hom-family-natural-transformation-Precategory C D F F)
        ( is-retraction-hom-inv-is-iso-Precategory
          ( functor-precategory-Precategory C D) {F} {G} is-iso-f))
      ( x)

  is-equiv-is-iso-functor-is-natural-isomorphism-Precategory :
    (f : natural-transformation-Precategory C D F G) →
    is-equiv (is-iso-functor-is-natural-isomorphism-Precategory f)
  is-equiv-is-iso-functor-is-natural-isomorphism-Precategory f =
    is-equiv-has-converse-is-prop
      ( is-prop-is-natural-isomorphism-Precategory C D F G f)
      ( is-prop-is-iso-Precategory
        ( functor-precategory-Precategory C D) {F} {G} f)
      ( is-natural-isomorphism-is-iso-functor-Precategory f)

  is-equiv-is-natural-isomorphism-is-iso-functor-Precategory :
    (f : natural-transformation-Precategory C D F G) →
    is-equiv (is-natural-isomorphism-is-iso-functor-Precategory f)
  is-equiv-is-natural-isomorphism-is-iso-functor-Precategory f =
    is-equiv-has-converse-is-prop
      ( is-prop-is-iso-Precategory
        ( functor-precategory-Precategory C D) {F} {G} f)
      ( is-prop-is-natural-isomorphism-Precategory C D F G f)
      ( is-iso-functor-is-natural-isomorphism-Precategory f)

  equiv-is-iso-functor-is-natural-isomorphism-Precategory :
    (f : natural-transformation-Precategory C D F G) →
    is-natural-isomorphism-Precategory C D F G f ≃
    is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f
  pr1 (equiv-is-iso-functor-is-natural-isomorphism-Precategory f) =
    is-iso-functor-is-natural-isomorphism-Precategory f
  pr2 (equiv-is-iso-functor-is-natural-isomorphism-Precategory f) =
    is-equiv-is-iso-functor-is-natural-isomorphism-Precategory f

  equiv-is-natural-isomorphism-is-iso-functor-Precategory :
    (f : natural-transformation-Precategory C D F G) →
    is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f ≃
    is-natural-isomorphism-Precategory C D F G f
  pr1 (equiv-is-natural-isomorphism-is-iso-functor-Precategory f) =
    is-natural-isomorphism-is-iso-functor-Precategory f
  pr2 (equiv-is-natural-isomorphism-is-iso-functor-Precategory f) =
    is-equiv-is-natural-isomorphism-is-iso-functor-Precategory f

  iso-functor-natural-isomorphism-Precategory :
    natural-isomorphism-Precategory C D F G →
    iso-Precategory (functor-precategory-Precategory C D) F G
  iso-functor-natural-isomorphism-Precategory =
    tot is-iso-functor-is-natural-isomorphism-Precategory

  natural-isomorphism-iso-functor-Precategory :
    iso-Precategory (functor-precategory-Precategory C D) F G →
    natural-isomorphism-Precategory C D F G
  natural-isomorphism-iso-functor-Precategory =
    tot is-natural-isomorphism-is-iso-functor-Precategory

  is-equiv-iso-functor-natural-isomorphism-Precategory :
    is-equiv iso-functor-natural-isomorphism-Precategory
  is-equiv-iso-functor-natural-isomorphism-Precategory =
    is-equiv-tot-is-fiberwise-equiv
      is-equiv-is-iso-functor-is-natural-isomorphism-Precategory

  is-equiv-natural-isomorphism-iso-functor-Precategory :
    is-equiv natural-isomorphism-iso-functor-Precategory
  is-equiv-natural-isomorphism-iso-functor-Precategory =
    is-equiv-tot-is-fiberwise-equiv
      is-equiv-is-natural-isomorphism-is-iso-functor-Precategory

  equiv-iso-functor-natural-isomorphism-Precategory :
    natural-isomorphism-Precategory C D F G ≃
    iso-Precategory (functor-precategory-Precategory C D) F G
  equiv-iso-functor-natural-isomorphism-Precategory =
    equiv-tot equiv-is-iso-functor-is-natural-isomorphism-Precategory

  equiv-natural-isomorphism-iso-functor-Precategory :
    iso-Precategory (functor-precategory-Precategory C D) F G ≃
    natural-isomorphism-Precategory C D F G
  equiv-natural-isomorphism-iso-functor-Precategory =
    equiv-tot equiv-is-natural-isomorphism-is-iso-functor-Precategory

Computing with the equivalence that isomorphisms are natural isomorphisms

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

  compute-iso-functor-natural-isomorphism-eq-Precategory :
    (p : F ＝ G) →
    iso-eq-Precategory (functor-precategory-Precategory C D) F G p ＝
    iso-functor-natural-isomorphism-Precategory C D F G
      ( natural-isomorphism-eq-Precategory C D F G p)
  compute-iso-functor-natural-isomorphism-eq-Precategory refl =
    eq-iso-eq-hom-Precategory
      ( functor-precategory-Precategory C D)
      { F} {G} _ _ refl

The evaluation functor

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

  ev-functor-Precategory :
    (c : obj-Precategory C) →
    functor-Precategory (functor-precategory-Precategory C D) D
  pr1 (ev-functor-Precategory c) F = obj-functor-Precategory C D F c
  pr1 (pr2 (ev-functor-Precategory c)) {F} {G} φ =
    hom-family-natural-transformation-Precategory C D F G φ c
  pr1 (pr2 (pr2 (ev-functor-Precategory c))) φ Ψ = refl
  pr2 (pr2 (pr2 (ev-functor-Precategory c))) F = refl

Recent changes