From 70320f743c9ac48bcc71be3e0e5100e2e206f913 Mon Sep 17 00:00:00 2001
From: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Fri, 9 Jul 2021 22:11:36 +0000
Subject: [PATCH] feat(category_theory/category/Kleisli): Fix lint errors
 (#8244)

Fixes some lint errors for this file: unused arguments, module doc, inhabited instances
---
 src/category_theory/category/Kleisli.lean | 35 +++++++++++++++--------
 1 file changed, 23 insertions(+), 12 deletions(-)

diff --git a/src/category_theory/category/Kleisli.lean b/src/category_theory/category/Kleisli.lean
index e62b3eeda7bb4..204325a09cff3 100644
--- a/src/category_theory/category/Kleisli.lean
+++ b/src/category_theory/category/Kleisli.lean
@@ -9,31 +9,42 @@ TODO: generalise this to work with category_theory.monad
 -/
 import category_theory.category
 
+/-!
+# The Kleisli construction on the Type category
+
+Define the Kleisli category for (control) monads.
+`category_theory/monad/kleisli` defines the general version for a monad on `C`, and demonstrates
+the equivalence between the two.
+-/
+
 universes u v
 
 namespace category_theory
 
-def Kleisli (m) [monad.{u v} m] := Type u
+/-- The Kleisli category on the (type-)monad `m`. Note that the monad is not assumed to be lawful
+yet. -/
+@[nolint unused_arguments]
+def Kleisli (m : Type u → Type v) := Type u
 
-def Kleisli.mk (m) [monad.{u v} m] (α : Type u) : Kleisli m := α
+/-- Construct an object of the Kleisli category from a type. -/
+def Kleisli.mk (m) (α : Type u) : Kleisli m := α
 
-instance Kleisli.category_struct {m} [monad m] : category_struct (Kleisli m) :=
+instance Kleisli.category_struct {m} [monad.{u v} m] : category_struct (Kleisli m) :=
 { hom := λ α β, α → m β,
-  id := λ α x, (pure x : m α),
+  id := λ α x, pure x,
   comp := λ X Y Z f g, f >=> g }
 
-instance Kleisli.category {m} [monad m] [is_lawful_monad m] : category (Kleisli m) :=
-by refine { hom := λ α β, α → m β,
-            id := λ α x, (pure x : m α),
-            comp := λ X Y Z f g, f >=> g,
-            id_comp' := _, comp_id' := _, assoc' := _ };
-   intros; ext; simp only [(>=>)] with functor_norm
+instance Kleisli.category {m} [monad.{u v} m] [is_lawful_monad m] : category (Kleisli m) :=
+by refine { id_comp' := _, comp_id' := _, assoc' := _ };
+   intros; ext; unfold_projs; simp only [(>=>)] with functor_norm
 
-@[simp] lemma Kleisli.id_def {m} [monad m] [is_lawful_monad m] (α : Kleisli m) :
+@[simp] lemma Kleisli.id_def {m} [monad m] (α : Kleisli m) :
   𝟙 α = @pure m _ α := rfl
 
-lemma Kleisli.comp_def {m} [monad m] [is_lawful_monad m] (α β γ : Kleisli m)
+lemma Kleisli.comp_def {m} [monad m] (α β γ : Kleisli m)
   (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) :
   (xs ≫ ys) a = xs a >>= ys := rfl
 
+instance : inhabited (Kleisli id) := ⟨punit⟩
+instance {α : Type u} [inhabited α] : inhabited (Kleisli.mk id α) := ⟨(default α : _)⟩
 end category_theory