Representable functors between categories

Content created by Fredrik Bakke

Created on 2023-09-18.
Last modified on 2023-09-18.

module category-theory.representable-functors-categories where
Imports 
open import category-theory.categories
open import category-theory.functors-categories
open import category-theory.natural-transformations-categories
open import category-theory.representable-functors-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 category C and an object c, there is a functor from C to the category of sets represented by c that:

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

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

Definition

rep-functor-Category :
  {l1 l2 : Level} (C : Category l1 l2) (c : obj-Category C) →
  functor-Category C (Set-Category l2)
rep-functor-Category C c = rep-functor-Precategory (precategory-Category C) c

Natural transformations between representable functors

A morphism f : hom b c in a category 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-Category :
  {l1 l2 : Level} (C : Category l1 l2) (b c : obj-Category C)
  (f : type-hom-Category C b c) →
  natural-transformation-Category
    ( C)
    ( Set-Category l2)
    ( rep-functor-Category C c)
    ( rep-functor-Category C b)
rep-natural-transformation-Category C =
  rep-natural-transformation-Precategory (precategory-Category C)

Recent changes