The empty category #
Defines a category structure on PEmpty
, and the unique functor PEmpty ⥤ C
for any category C
.
The canonical functor out of the empty category.
Instances For
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.
Instances For
def
CategoryTheory.Functor.uniqueFromEmpty
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C)
:
Any functor out of the empty category is isomorphic to the canonical functor from the empty category.
Instances For
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.