mathlib3 documentation


The category discrete punit #

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

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

The constant functor sending everything to

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.


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.

Functors from discrete punit are equivalent to the category itself.


A category being equivalent to punit is equivalent to it having a unique morphism between any two objects. (In fact, such a category is also a groupoid; see groupoid.of_hom_unique)