The category Type. #
In this section we define a LargeCategory structure on Type u, in such a way that it becomes a
ConcreteCategory.
Implementation #
We define the one-field structure TypeCat.Fun to wrap a function between types, and a FunLike
instance on it. Then we define a one-field structure TypeCat.Hom which wraps a Fun. The
morphisms in the category Type u are defined to be TypeCat.Hom, and the FC parameter of
the ConcreteCategory instance is TypeCat.Fun. TypeCat.Fun serves as a layer of separation
between the FC parameter of the ConcreteCategory instance and bare functions, to avoid defining
a FunLike instance on the latter (which would give two non-reducibly defeq coercions from
morphisms in Type to functions), and the outer nesting TypeCat.Hom gives a layer of separation
between morphisms and FC, as is done for all concrete categories in mathlib.
To promote a function to a morphism in this category, we provide the abbreviation ↾f,
as well as a corresponding notation ↾f. (Entered as \upr .)
Main definitions #
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,
Isois bothIsoandEquivtoEquiv(at least within a fixed universe),- every type level
IsLawfulFunctorgives a categorical functorType ⥤ Type(the corresponding fact about monads is inMathlib/CategoryTheory/Monad/Types.lean).
A one-field structure wrapping a function between types.
- toFun : X → Y
The underlying function.
Instances For
Equations
- TypeCat.instFunLikeFun = { coe := fun (f : TypeCat.Fun X Y) (x : X) => f.toFun x, coe_injective := ⋯ }
The equivalence between Funs and functions between types.
Equations
- TypeCat.Fun.homEquiv X Y = { toFun := fun (f : TypeCat.Fun X Y) => ⇑f, invFun := fun (f : X → Y) => { toFun := f }, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
The concrete category instance on Type u.
Note: sometimes one needs to specify explicitly (CC := fun X ↦ X) to help typeclass inference.
Equations
- One or more equations did not get rendered due to their size.
Turn a morphism in Type back into a function.
Equations
Instances For
Typecheck a function as a morphism in Type.
Equations
- TypeCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom { toFun := f }
Instances For
Typecheck a function as a morphism in 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.
Equations
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 ULifted to the same universe,
and the original type.
Equations
- CategoryTheory.uliftTrivial V = { hom := TypeCat.ofHom fun (a : ULift.{?u.1, ?u.1} V) => a.down, inv := TypeCat.ofHom 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
uliftFunctor : Type u ⥤ Type max u v is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 = TypeCat.ofHom fun (x_1 : PUnit.{?u.1 + 1}) => x
Instances For
A morphism in Type is a monomorphism if and only if it is injective.
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.
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
- One or more equations did not get rendered due to their size.
Instances For
Any equivalence between types in the same universe gives a categorical isomorphism between those types.
Equations
- e.toIso = { hom := TypeCat.ofHom fun (x : X) => e x, inv := TypeCat.ofHom fun (x : Y) => e.symm x, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Alias of Equiv.toIso_hom_hom_apply.
Alias of Equiv.toIso_inv_hom_apply.
Any isomorphism between types gives an equivalence.
Equations
- i.toEquiv = { toFun := ⇑(CategoryTheory.ConcreteCategory.hom i.hom), invFun := ⇑(CategoryTheory.ConcreteCategory.hom i.inv), left_inv := ⋯, right_inv := ⋯ }
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.
Equations
- equivIsoIso = { hom := TypeCat.ofHom fun (e : X ≃ Y) => e.toIso, inv := TypeCat.ofHom fun (i : X ≅ Y) => i.toEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms of types.