Documentation

Mathlib.CategoryTheory.PEmpty

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

    Any functor out of the empty category is isomorphic to the canonical functor from the empty category.

    Instances For

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