# 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 both Iso and Equiv to Equiv (at least within a fixed universe),
• every type level IsLawfulFunctor gives a categorical functor Type ⥤ Type (the corresponding fact about monads is in Mathlib/CategoryTheory/Monad/Types.lean).
theorem CategoryTheory.types_hom {α : Type u} {β : Type u} :
(α β) = (αβ)
theorem CategoryTheory.types_ext {α : Type u} {β : Type u} (f : α β) (g : α β) (h : ∀ (a : α), f a = g a) :
f = g
theorem CategoryTheory.types_comp {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.types_id_apply (X : Type u) (x : X) :
@[simp]
theorem CategoryTheory.types_comp_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) (x : X) :
= g (f x)
@[simp]
theorem CategoryTheory.hom_inv_id_apply {X : Type u} {Y : Type u} (f : X Y) (x : X) :
f.inv (f.hom x) = x
@[simp]
theorem CategoryTheory.inv_hom_id_apply {X : Type u} {Y : Type u} (f : X Y) (y : Y) :
f.hom (f.inv y) = y
@[reducible, inline]
abbrev CategoryTheory.asHom {α : Type u} {β : Type u} (f : αβ) :
α β

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
Instances For
def CategoryTheory.Functor.sections {J : Type u} (F : ) :
Set ((j : J) → F.obj j)

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
• F.sections = {u : (j : J) → F.obj j | ∀ {j j' : J} (f : j j'), F.map f (u j) = u j'}
Instances For
@[simp]
theorem CategoryTheory.Functor.sections_property {J : Type u} {F : } (s : F.sections) {j : J} {j' : J} (f : j j') :
F.map f (s j) = s j'
theorem CategoryTheory.Functor.sections_ext_iff {J : Type u} {F : } {x : F.sections} {y : F.sections} :
x = y ∀ (j : J), x j = y j
@[simp]
theorem CategoryTheory.Functor.sectionsFunctor_map_coe (J : Type u) {F : } {G : } (φ : F G) (x : F.sections) (j : J) :
( φ x) j = φ.app j (x j)
@[simp]
theorem CategoryTheory.Functor.sectionsFunctor_obj (J : Type u) (F : ) :
= F.sections

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
@[simp]
theorem CategoryTheory.FunctorToTypes.map_comp_apply {C : Type u} (F : ) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (a : F.obj X) :
F.map a = F.map g (F.map f a)
@[simp]
theorem CategoryTheory.FunctorToTypes.map_id_apply {C : Type u} (F : ) {X : C} (a : F.obj X) :
F.map a = a
theorem CategoryTheory.FunctorToTypes.naturality {C : Type u} (F : ) (G : ) {X : C} {Y : C} (σ : F G) (f : X Y) (x : F.obj X) :
σ.app Y (F.map f x) = G.map f (σ.app X x)
@[simp]
theorem CategoryTheory.FunctorToTypes.comp {C : Type u} (F : ) (G : ) (H : ) {X : C} (σ : F G) (τ : G H) (x : F.obj X) :
.app X x = τ.app X (σ.app X x)
@[simp]
theorem CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply {C : Type u} (F : ) {X : C} {Y : C} {Z : C} (p : X = Y) (q : Y = Z) (x : F.obj X) :
F.map (F.map x) = F.map x
@[simp]
theorem CategoryTheory.FunctorToTypes.hcomp {C : Type u} (F : ) (G : ) (σ : F G) {D : Type u'} [𝒟 : ] (I : ) (J : ) (ρ : I J) {W : D} (x : (I.comp F).obj W) :
(ρ σ).app W x = G.map (ρ.app W) (σ.app (I.obj W) x)
@[simp]
theorem CategoryTheory.FunctorToTypes.map_inv_map_hom_apply {C : Type u} (F : ) {X : C} {Y : C} (f : X Y) (x : F.obj X) :
F.map f.inv (F.map f.hom x) = x
@[simp]
theorem CategoryTheory.FunctorToTypes.map_hom_map_inv_apply {C : Type u} (F : ) {X : C} {Y : C} (f : X Y) (y : F.obj Y) :
F.map f.hom (F.map f.inv y) = y
@[simp]
theorem CategoryTheory.FunctorToTypes.hom_inv_id_app_apply {C : Type u} (F : ) (G : ) (α : F G) (X : C) (x : F.obj X) :
α.inv.app X (α.hom.app X x) = x
@[simp]
theorem CategoryTheory.FunctorToTypes.inv_hom_id_app_apply {C : Type u} (F : ) (G : ) (α : F G) (X : C) (x : G.obj X) :
α.hom.app X (α.inv.app X x) = x

The isomorphism between a Type which has been ULifted to the same universe, and the original type.

Equations
• = { hom := fun (a : ) => 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
@[simp]
@[simp]
theorem CategoryTheory.uliftFunctor_map {X : Type u} {Y : Type u} (f : X Y) (x : ) :
f x = { down := f x.down }

The functor embedding Type u into Type u via ULift is isomorphic to the identity functor.

Equations
Instances For
def CategoryTheory.homOfElement {X : Type u} (x : X) :

Any term x of a type X corresponds to a morphism PUnit ⟶ X.

Equations
• = x✝
Instances For
theorem CategoryTheory.homOfElement_eq_iff {X : Type u} (x : X) (y : X) :
theorem CategoryTheory.mono_iff_injective {X : Type u} {Y : Type u} (f : X Y) :

A morphism in Type is a monomorphism if and only if it is injective.

theorem CategoryTheory.injective_of_mono {X : Type u} {Y : Type u} (f : X Y) [hf : ] :
theorem CategoryTheory.epi_iff_surjective {X : Type u} {Y : Type u} (f : X Y) :

A morphism in Type is an epimorphism if and only if it is surjective.

theorem CategoryTheory.surjective_of_epi {X : Type u} {Y : Type u} (f : X Y) [hf : ] :
def CategoryTheory.ofTypeFunctor (m : Type u → Type v) [] [] :

ofTypeFunctor m converts from Lean's Type-based Category to CategoryTheory. This allows us to use these functors in category theory.

Equations
• = { obj := m, map := fun {X Y : Type u} (f : X Y) => , map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.ofTypeFunctor_obj (m : Type u → Type v) [] [] :
.obj = m
@[simp]
theorem CategoryTheory.ofTypeFunctor_map (m : Type u → Type v) [] [] {α : Type u} {β : Type u} (f : αβ) :
.map f =
def Equiv.toIso {X : Type u} {Y : Type u} (e : X Y) :
X Y

Any equivalence between types in the same universe gives a categorical isomorphism between those types.

Equations
• e.toIso = { hom := e.toFun, inv := e.invFun, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem Equiv.toIso_hom {X : Type u} {Y : Type u} {e : X Y} :
e.toIso.hom = e
@[simp]
theorem Equiv.toIso_inv {X : Type u} {Y : Type u} {e : X Y} :
e.toIso.inv = e.symm
def CategoryTheory.Iso.toEquiv {X : Type u} {Y : Type u} (i : X Y) :
X Y

Any isomorphism between types gives an equivalence.

Equations
• i.toEquiv = { toFun := i.hom, invFun := i.inv, left_inv := , right_inv := }
Instances For
@[simp]
theorem CategoryTheory.Iso.toEquiv_fun {X : Type u} {Y : Type u} (i : X Y) :
i.toEquiv = i.hom
@[simp]
theorem CategoryTheory.Iso.toEquiv_symm_fun {X : Type u} {Y : Type u} (i : X Y) :
i.toEquiv.symm = i.inv
@[simp]
theorem CategoryTheory.Iso.toEquiv_id (X : Type u) :
.toEquiv =
@[simp]
theorem CategoryTheory.Iso.toEquiv_comp {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) (g : Y Z) :
(f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv
theorem CategoryTheory.isIso_iff_bijective {X : Type u} {Y : Type u} (f : X Y) :

A morphism in Type u is an isomorphism if and only if it is bijective.

@[simp]
theorem equivIsoIso_hom {X : Type u} {Y : Type u} (e : X Y) :
equivIsoIso.hom e = e.toIso
@[simp]
theorem equivIsoIso_inv {X : Type u} {Y : Type u} (i : X Y) :
equivIsoIso.inv i = i.toEquiv
def equivIsoIso {X : Type u} {Y : Type u} :
X Y X Y

Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms of types.

Equations
• equivIsoIso = { hom := fun (e : X Y) => e.toIso, inv := fun (i : X Y) => i.toEquiv, hom_inv_id := , inv_hom_id := }
Instances For
def equivEquivIso {X : Type u} {Y : Type u} :
X Y (X Y)

Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms of types.

Equations
• equivEquivIso = equivIsoIso.toEquiv
Instances For
@[simp]
theorem equivEquivIso_hom {X : Type u} {Y : Type u} (e : X Y) :
equivEquivIso e = e.toIso
@[simp]
theorem equivEquivIso_inv {X : Type u} {Y : Type u} (e : X Y) :
equivEquivIso.symm e = e.toEquiv