mathlib documentation

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.