mathlib documentation

category_theory.punit

The category discrete punit #

We define star : C ⥤ discrete punit sending everything to punit.star, show that any two functors to discrete punit are naturally isomorphic, and construct the equivalence (discrete punit ⥤ C) ≌ C.

Any two functors to discrete punit are isomorphic.

Equations

Any two functors to discrete punit are equal. You probably want to use punit_ext instead of this.

The functor from discrete punit sending everything to the given object.