The empty category

Defines a category structure on PEmpty, and the unique functor PEmpty ⥤ C for any category C.

def CategoryTheory.Functor.emptyEquivalence : CategoryTheory.Discrete PEmpty.{w + 1} ≌ CategoryTheory.Discrete PEmpty.{v + 1}

Equivalence between two empty categories.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Functor.empty (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C

The canonical functor out of the empty category.

Equations

• CategoryTheory.Functor.empty C = CategoryTheory.Discrete.functor PEmpty.elim

def CategoryTheory.Functor.emptyExt {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C) (G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C) : F ≅ G

Any two functors out of the empty category are isomorphic.

Equations

• CategoryTheory.Functor.emptyExt F G = CategoryTheory.Discrete.natIso fun x => PEmpty.elim x.as

def CategoryTheory.Functor.uniqueFromEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C) : F ≅ CategoryTheory.Functor.empty C

Any functor out of the empty category is isomorphic to the canonical functor from the empty category.

Equations

• CategoryTheory.Functor.uniqueFromEmpty F = CategoryTheory.Functor.emptyExt F (CategoryTheory.Functor.empty C)

theorem CategoryTheory.Functor.empty_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C) (G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C) : F = G

Any two functors out of the empty category are equal. You probably want to use emptyExt instead of this.