Documentation

Mathlib.CategoryTheory.PEmpty

The empty category #

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

The (unique) functor from an empty category.

Equations
Instances For

    Any two functors out of an empty category are isomorphic.

    Equations
    Instances For

      The equivalence between two empty categories.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        Instances For

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