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 large_category 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 as_hom 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 ulift_functor, 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,
isois bothisoandequivtoequiv(at least within a fixed universe),- every type level
is_lawful_functorgives a categorical functorType ⥤ Type(the corresponding fact about monads is insrc/category_theory/monad/types.lean).
Equations
- category_theory.types = {to_category_struct := {to_has_hom := {hom := λ (a b : Type u), a → b}, id := λ (a : Type u), id, comp := λ (_x _x_1 _x_2 : Type u) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), g ∘ f}, id_comp' := category_theory.types._proof_1, comp_id' := category_theory.types._proof_2, assoc' := category_theory.types._proof_3}
as_hom f helps Lean type check a function as a morphism in the category Type.
The sections of a functor 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.
The isomorphism between a Type which has been ulifted to the same universe,
and the original type.
Equations
- category_theory.ulift_trivial V = {hom := id (λ (a : ulift V), a.cases_on (λ (a : V), a)), inv := ulift.up V, hom_inv_id' := _, inv_hom_id' := _}
The functor embedding Type u into Type (max u v).
Write this as ulift_functor.{5 2} to get Type 2 ⥤ Type 5.
Equations
- category_theory.ulift_functor_full = {preimage := λ (X Y : Type u) (f : category_theory.ulift_functor.obj X ⟶ category_theory.ulift_functor.obj Y) (x : X), (f {down := x}).down, witness' := category_theory.ulift_functor_full._proof_1}
Any term x of a type X corresponds to a morphism punit ⟶ X.
Equations
- category_theory.hom_of_element x = λ (_x : punit), x
of_type_functor m converts from Lean's Type-based category to category_theory. This
allows us to use these functors in category theory.
Equations
- category_theory.of_type_functor m = {obj := m, map := λ (α β : Type u), functor.map, map_id' := _, map_comp' := _}
Any equivalence between types in the same universe gives a categorical isomorphism between those types.
Equations
- e.to_iso = {hom := e.to_fun, inv := e.inv_fun, hom_inv_id' := _, inv_hom_id' := _}
equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms of types
Equations
- equiv_iso_iso = {hom := λ (e : X ≃ Y), e.to_iso, inv := λ (i : X ≅ Y), i.to_equiv, hom_inv_id' := _, inv_hom_id' := _}
equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms of types