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.
def
category_theory.functor.empty_ext
{C : Type u}
[category_theory.category C]
(F G : category_theory.discrete pempty ⥤ C) :
F ≅ G
Any two functors out of the empty category are isomorphic.
Equations
- F.empty_ext G = category_theory.discrete.nat_iso (λ (x : category_theory.discrete pempty), pempty.elim x)
def
category_theory.functor.unique_from_empty
{C : Type u}
[category_theory.category C]
(F : category_theory.discrete pempty ⥤ C) :
Any functor out of the empty category is isomorphic to the canonical functor from the empty category.
Equations
theorem
category_theory.functor.empty_ext'
{C : Type u}
[category_theory.category C]
(F G : category_theory.discrete pempty ⥤ C) :
F = G
Any two functors out of the empty category are equal. You probably want to use
empty_ext instead of this.