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.

@[simp]
theorem category_theory.functor.star_map_down_down (C : Type u) [category_theory.category C] (j j' : C) (f : j j') :
_ = _

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.