Representable functors between precategories
Content created by Fredrik Bakke, Egbert Rijke, Emily Riehl, Julian KG, fernabnor and louismntnu.
Created on 2023-05-27.
Last modified on 2023-09-26.
module category-theory.representable-functors-precategories where
Imports
open import category-theory.functors-precategories open import category-theory.natural-transformations-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.universe-levels
Idea
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
ofC
to the sethom c x
and - sends a morphism
g : hom x y
ofC
to the functionhom c x → hom c y
defined by postcomposition withg
.
The functoriality axioms follow, by
function extensionality, from
associativity and the left unit law for the precategory C
.
Definition
representable-functor-Precategory : {l1 l2 : Level} (C : Precategory l1 l2) (c : obj-Precategory C) → functor-Precategory C (Set-Precategory l2) pr1 (representable-functor-Precategory C c) = hom-set-Precategory C c pr1 (pr2 (representable-functor-Precategory C c)) g = postcomp-hom-Precategory C g c pr1 (pr2 (pr2 (representable-functor-Precategory C c))) h g = eq-htpy (associative-comp-hom-Precategory C h g) pr2 (pr2 (pr2 (representable-functor-Precategory C c))) _ = eq-htpy (left-unit-law-comp-hom-Precategory C)
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
.
rep-natural-transformation-Precategory : {l1 l2 : Level} (C : Precategory l1 l2) (b c : obj-Precategory C) (f : hom-Precategory C b c) → natural-transformation-Precategory ( C) ( Set-Precategory l2) ( representable-functor-Precategory C c) ( representable-functor-Precategory C b) pr1 (rep-natural-transformation-Precategory C b c f) = precomp-hom-Precategory C f pr2 (rep-natural-transformation-Precategory C b c f) h = eq-htpy (inv-htpy (λ g → associative-comp-hom-Precategory C h g f))
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-18. Fredrik Bakke. Yoneda's lemma for categories (#783).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-05-27. Emily Riehl, Emily Riehl and Fredrik Bakke. Yoneda (#632).