From e50763397814429741cdb4f5e5db4a788700e675 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Mon, 3 Dec 2018 13:00:18 +0100
Subject: [PATCH] feat(category_theory/const): Constant functor of object from
 punit

---
 category_theory/const.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/category_theory/const.lean b/category_theory/const.lean
index 4b08ed139cf9a..bed3dea6e23dd 100644
--- a/category_theory/const.lean
+++ b/category_theory/const.lean
@@ -4,6 +4,7 @@
 
 import category_theory.functor_category
 import category_theory.isomorphism
+import category_theory.punit
 
 universes u₁ v₁ u₂ v₂ u₃ v₃
 
@@ -47,4 +48,13 @@ include 𝒟
 
 end
 
+omit 𝒥
+def of : C ⥤ (punit ⥤ 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 category_theory.functor