In this section we set up the theory so that Lean's types and functions between them
can be viewed as a
LargeCategory in our framework.
Lean can not transparently view a function as a morphism in this category, and needs a hint in
order to be able to type check. We provide the abbreviation
asHom f to guide type checking,
as well as a corresponding notation
↾ f. (Entered as
We provide various simplification lemmas for functors and natural transformations valued in
Type u to
Type (max u v), and show that it is fully faithful
(but not, of course, essentially surjective).
We prove some basic facts about the category
The sections of a functor
J ⥤ Type are
the choices of a point
u j : F.obj j for each
F.map f (u j) = u j for every morphism
f : j ⟶ j'.
We later use these to define limits in
Type and in many concrete categories.