mathlib3 documentation

category_theory.pempty

The empty category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Equivalence between two empty categories.

Equations

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.