# mathlibdocumentation

category_theory.pempty

# The empty category #

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

Equivalence between two empty categories.

Equations
• category_theory.functor.empty_equivalence = category_theory.equivalence.mk {obj := , map := λ (x : , , map_id' := category_theory.functor.empty_equivalence._proof_1, map_comp' := category_theory.functor.empty_equivalence._proof_2} {obj := , map := λ (x : , , map_id' := category_theory.functor.empty_equivalence._proof_3, map_comp' := category_theory.functor.empty_equivalence._proof_4} (id {hom := category_theory.functor.empty_equivalence._aux_2, inv := category_theory.functor.empty_equivalence._aux_4, hom_inv_id' := category_theory.functor.empty_equivalence._proof_9, inv_hom_id' := category_theory.functor.empty_equivalence._proof_10}) (id {hom := category_theory.functor.empty_equivalence._aux_6, inv := category_theory.functor.empty_equivalence._aux_8, hom_inv_id' := category_theory.functor.empty_equivalence._proof_11, inv_hom_id' := category_theory.functor.empty_equivalence._proof_12})
def category_theory.functor.empty (C : Type u)  :

The canonical functor out of the empty category.

Equations
def category_theory.functor.empty_ext {C : Type u} (F G : C) :
F G

Any two functors out of the empty category are isomorphic.

Equations

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} (F G : C) :
F = G

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