The empty category

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

instance CategoryTheory.instIsEmptyDiscrete (α : Type u_1) [IsEmpty α] : IsEmpty (Discrete α)

def CategoryTheory.functorOfIsEmpty (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [IsEmpty C] : Functor C D

The (unique) functor from an empty category.

def CategoryTheory.Functor.isEmptyExt {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [IsEmpty C] (F G : Functor C D) : F ≅ G

Any two functors out of an empty category are isomorphic.

def CategoryTheory.equivalenceOfIsEmpty (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [IsEmpty C] [IsEmpty D] : C ≌ D

The equivalence between two empty categories.

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

Equivalence between two empty categories.

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

The canonical functor out of the empty category.

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

Any two functors out of the empty category are isomorphic.

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

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

theorem CategoryTheory.Functor.empty_ext' {C : Type u} [Category.{v, u} C] (F G : Functor (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.