The category Type
. #
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 \upr
.)
We provide various simplification lemmas for functors and natural transformations valued in Type
.
We define uliftFunctor
, from 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 Type
:
- epimorphisms are surjections and monomorphisms are injections,
Iso
is bothIso
andEquiv
toEquiv
(at least within a fixed universe),- every type level
IsLawfulFunctor
gives a categorical functorType ⥤ Type
(the corresponding fact about monads is inMathlib/CategoryTheory/Monad/Types.lean
).
asHom f
helps Lean type check a function as a morphism in the category Type
.
Equations
Instances For
asHom f
helps Lean type check a function as a morphism in the category Type
.
Equations
- CategoryTheory.«term↾_» = Lean.ParserDescr.node `CategoryTheory.«term↾_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 200))
Instances For
The sections of a functor F : J ⥤ Type
are
the choices of a point u j : F.obj j
for each j
,
such that 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.
Instances For
The functor which sends a functor to types to its sections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The isomorphism between a Type
which has been ULift
ed to the same universe,
and the original type.
Equations
- CategoryTheory.uliftTrivial V = { hom := fun (a : ULift.{?u.16, ?u.16} V) => a.down, inv := fun (a : V) => { down := a }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
The functor embedding Type u
into Type (max u v)
.
Write this as uliftFunctor.{5, 2}
to get Type 2 ⥤ Type 5
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
The functor embedding Type u
into Type u
via ULift
is isomorphic to the identity functor.
Equations
Instances For
Any term x
of a type X
corresponds to a morphism PUnit ⟶ X
.
Equations
- CategoryTheory.homOfElement x✝ x = x✝
Instances For
A morphism in Type
is a monomorphism if and only if it is injective.
A morphism in Type
is an epimorphism if and only if it is surjective.
ofTypeFunctor m
converts from Lean's Type
-based Category
to CategoryTheory
. This
allows us to use these functors in category theory.
Equations
- CategoryTheory.ofTypeFunctor m = { obj := m, map := fun {X Y : Type ?u.28} (f : X ⟶ Y) => Functor.map f, map_id := ⋯, map_comp := ⋯ }
Instances For
A morphism in Type u
is an isomorphism if and only if it is bijective.
Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms of types.