mathlib documentation

category_theory.​pempty

category_theory.​pempty

The empty category

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

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

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