fix(category_theory/punit): fix regression (#550)

Author: jcommelin

category_theory/punit.lean

@@ -13,4 +13,20 @@ instance punit_category : small_category punit :=
   id   := λ _, punit.star,
   comp := λ _ _ _ _ _, punit.star }
 
+namespace functor
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞
+
+/-- The constant functor. For `X : C`, `of.obj X` is the functor `punit ⥤ C`
+  that maps `punit.star` to `X`. -/
+def of : C ⥤ (punit.{w+1} ⥤ C) := const punit
+
+namespace of
+@[simp] lemma obj_obj (X : C) : (of.obj X).obj = λ _, X := rfl
+@[simp] lemma obj_map (X : C) : (of.obj X).map = λ _ _ _, 𝟙 X := rfl
+@[simp] lemma map_app {X Y : C} (f : X ⟶ Y) : (of.map f).app = λ _, f := rfl
+end of
+
+end functor
+
 end category_theory