Representable functors between precategories

Content created by Fredrik Bakke, Egbert Rijke, Emily Riehl, Daniel Gratzer, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2023-05-27.
Last modified on 2023-11-27.

module category-theory.representable-functors-precategories where
open import category-theory.copresheaf-categories
open import category-theory.functors-precategories
open import category-theory.maps-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.opposite-precategories
open import category-theory.precategories

open import foundation.category-of-sets
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.sets
open import foundation.universe-levels


Given a precategory C and an object c, there is a functor from C to the precategory of sets represented by c that:

  • sends an object x of C to the set hom c x and
  • sends a morphism f : hom x y of C to the function hom c x → hom c y defined by postcomposition with f.

The functoriality axioms follow, by function extensionality, from associativity and the left unit law for the precategory C.


module _
  {l1 l2 : Level} (C : Precategory l1 l2) (c : obj-Precategory C)

  obj-representable-functor-Precategory : obj-Precategory C  Set l2
  obj-representable-functor-Precategory = hom-set-Precategory C c

  hom-representable-functor-Precategory :
    {x y : obj-Precategory C} (f : hom-Precategory C x y) 
    hom-Precategory C c x  hom-Precategory C c y
  hom-representable-functor-Precategory f = postcomp-hom-Precategory C f c

  representable-map-Precategory : map-Precategory C (Set-Precategory l2)
  pr1 representable-map-Precategory = obj-representable-functor-Precategory
  pr2 representable-map-Precategory = hom-representable-functor-Precategory

  preserves-comp-representable-functor-Precategory :
      ( C)
      ( Set-Precategory l2)
      ( representable-map-Precategory)
  preserves-comp-representable-functor-Precategory g f =
    eq-htpy (associative-comp-hom-Precategory C g f)

  preserves-id-representable-functor-Precategory :
      ( C)
      ( Set-Precategory l2)
      ( representable-map-Precategory)
  preserves-id-representable-functor-Precategory x =
    eq-htpy (left-unit-law-comp-hom-Precategory C)

  representable-functor-Precategory : functor-Precategory C (Set-Precategory l2)
  pr1 representable-functor-Precategory =
  pr1 (pr2 representable-functor-Precategory) =
  pr1 (pr2 (pr2 representable-functor-Precategory)) =
  pr2 (pr2 (pr2 representable-functor-Precategory)) =

Natural transformations between representable functors

A morphism f : hom b c in a precategory C defines a natural transformation from the functor represented by c to the functor represented by b. Its components hom c x → hom b x are defined by precomposition with f.

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  {b c : obj-Precategory C} (f : hom-Precategory C b c)

  hom-family-representable-natural-transformation-Precategory :
      ( C)
      ( Set-Precategory l2)
      ( representable-functor-Precategory C c)
      ( representable-functor-Precategory C b)
  hom-family-representable-natural-transformation-Precategory =
    precomp-hom-Precategory C f

  is-natural-transformation-representable-natural-transformation-Precategory :
      ( C)
      ( Set-Precategory l2)
      ( representable-functor-Precategory C c)
      ( representable-functor-Precategory C b)
      ( hom-family-representable-natural-transformation-Precategory)
  is-natural-transformation-representable-natural-transformation-Precategory h =
    eq-htpy (inv-htpy  g  associative-comp-hom-Precategory C h g f))

  representable-natural-transformation-Precategory :
      ( C)
      ( Set-Precategory l2)
      ( representable-functor-Precategory C c)
      ( representable-functor-Precategory C b)
  pr1 (representable-natural-transformation-Precategory) =
  pr2 (representable-natural-transformation-Precategory) =


Taking representable functors defines a functor into the presheaf category

module _
  {l1 l2 : Level} (C : Precategory l1 l2)

  map-representable-functor-copresheaf-Precategory :
      ( opposite-Precategory C)
      ( copresheaf-precategory-Precategory C l2)
  pr1 map-representable-functor-copresheaf-Precategory =
    representable-functor-Precategory C
  pr2 map-representable-functor-copresheaf-Precategory =
    representable-natural-transformation-Precategory C

It remains to show that this map is functorial.

Recent changes