This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Representable functors between large precategories

module category-theory.representable-functors-large-precategories where
Imports 
open import category-theory.functors-large-precategories
open import category-theory.large-precategories
open import category-theory.natural-transformations-functors-large-precategories

open import foundation.category-of-sets
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

Idea

Given a large 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 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 precategory C.

Definition

module _
  {α : Level → Level} {β : Level → Level → Level}
  (C : Large-Precategory α β) {l1 : Level} (c : obj-Large-Precategory C l1)
  where

  obj-representable-functor-Large-Precategory :
    {l2 : Level} (x : obj-Large-Precategory C l2) → Set (β l1 l2)
  obj-representable-functor-Large-Precategory =
    hom-set-Large-Precategory C c

  hom-representable-functor-Large-Precategory :
    {l2 l3 : Level}
    {X : obj-Large-Precategory C l2} {Y : obj-Large-Precategory C l3} →
    hom-Large-Precategory C X Y →
    hom-Set
      ( obj-representable-functor-Large-Precategory X)
      ( obj-representable-functor-Large-Precategory Y)
  hom-representable-functor-Large-Precategory =
    postcomp-hom-Large-Precategory C c

  preserves-comp-representable-functor-Large-Precategory :
    {l2 l3 l4 : Level}
    {X : obj-Large-Precategory C l2}
    {Y : obj-Large-Precategory C l3}
    {Z : obj-Large-Precategory C l4}
    (g : hom-Large-Precategory C Y Z)
    (f : hom-Large-Precategory C X Y) →
    hom-representable-functor-Large-Precategory
      ( comp-hom-Large-Precategory C g f) ＝
    hom-representable-functor-Large-Precategory g ∘
    hom-representable-functor-Large-Precategory f
  preserves-comp-representable-functor-Large-Precategory g f =
    eq-htpy (associative-comp-hom-Large-Precategory C g f)

  preserves-id-representable-functor-Large-Precategory :
    {l2 : Level} {X : obj-Large-Precategory C l2} →
    hom-representable-functor-Large-Precategory
      ( id-hom-Large-Precategory C {X = X}) ＝
    id
  preserves-id-representable-functor-Large-Precategory =
    eq-htpy (left-unit-law-comp-hom-Large-Precategory C)

  representable-functor-Large-Precategory :
    functor-Large-Precategory (β l1) C (Set-Large-Precategory)
  obj-functor-Large-Precategory representable-functor-Large-Precategory =
    obj-representable-functor-Large-Precategory
  hom-functor-Large-Precategory representable-functor-Large-Precategory =
    hom-representable-functor-Large-Precategory
  preserves-comp-functor-Large-Precategory
    representable-functor-Large-Precategory =
    preserves-comp-representable-functor-Large-Precategory
  preserves-id-functor-Large-Precategory
    representable-functor-Large-Precategory =
    preserves-id-representable-functor-Large-Precategory

Natural transformations between representable functors

A morphism f : hom b c in a large 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 _
  {α : Level → Level} {β : Level → Level → Level} (C : Large-Precategory α β)
  {l1 l2 : Level}
  (b : obj-Large-Precategory C l1) (c : obj-Large-Precategory C l2)
  (f : hom-Large-Precategory C b c)
  where

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

  naturality-representable-natural-transformation-Large-Precategory :
    naturality-family-of-morphisms-functor-Large-Precategory C
      ( Set-Large-Precategory)
      ( representable-functor-Large-Precategory C c)
      ( representable-functor-Large-Precategory C b)
      ( hom-representable-natural-transformation-Large-Precategory)
  naturality-representable-natural-transformation-Large-Precategory h =
    inv (eq-htpy (λ g → associative-comp-hom-Large-Precategory C h g f))

  representable-natural-transformation-Large-Precategory :
    natural-transformation-Large-Precategory C Set-Large-Precategory
      ( representable-functor-Large-Precategory C c)
      ( representable-functor-Large-Precategory C b)
  hom-natural-transformation-Large-Precategory
    representable-natural-transformation-Large-Precategory =
    hom-representable-natural-transformation-Large-Precategory
  naturality-natural-transformation-Large-Precategory
    representable-natural-transformation-Large-Precategory =
    naturality-representable-natural-transformation-Large-Precategory