-
Notifications
You must be signed in to change notification settings - Fork 259
/
KleisliCat.lean
77 lines (58 loc) · 2.59 KB
/
KleisliCat.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
! This file was ported from Lean 3 source module category_theory.category.Kleisli
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.Category.Basic
/-!
# The Kleisli construction on the Type category
Define the Kleisli category for (control) monads.
`CategoryTheory/Monad/Kleisli` defines the general version for a monad on `C`, and demonstrates
the equivalence between the two.
## TODO
Generalise this to work with CategoryTheory.Monad
-/
universe u v
namespace CategoryTheory
-- This file is about Lean 3 declaration "Kleisli".
set_option linter.uppercaseLean3 false
/-- The Kleisli category on the (type-)monad `m`. Note that the monad is not assumed to be lawful
yet. -/
@[nolint unusedArguments]
def KleisliCat (_ : Type u → Type v) :=
Type u
#align category_theory.Kleisli CategoryTheory.KleisliCat
/-- Construct an object of the Kleisli category from a type. -/
def KleisliCat.mk (m) (α : Type u) : KleisliCat m :=
α
#align category_theory.Kleisli.mk CategoryTheory.KleisliCat.mk
instance KleisliCat.categoryStruct {m} [Monad.{u, v} m] :
CategoryStruct (KleisliCat m) where
Hom α β := α → m β
id _ x := pure x
comp f g := f >=> g
#align category_theory.Kleisli.category_struct CategoryTheory.KleisliCat.categoryStruct
instance KleisliCat.category {m} [Monad.{u, v} m] [LawfulMonad m] : Category (KleisliCat m) := by
-- Porting note: was
-- refine' { id_comp' := _, comp_id' := _, assoc' := _ } <;> intros <;> ext <;> unfold_projs <;>
-- simp only [(· >=> ·), functor_norm]
refine' { id_comp := _, comp_id := _, assoc := _ } <;> intros <;> refine funext (fun x => ?_) <;>
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]
#align category_theory.Kleisli.category CategoryTheory.KleisliCat.category
@[simp]
theorem KleisliCat.id_def {m} [Monad m] (α : KleisliCat m) : 𝟙 α = @pure m _ α :=
rfl
#align category_theory.Kleisli.id_def CategoryTheory.KleisliCat.id_def
theorem KleisliCat.comp_def {m} [Monad m] (α β γ : KleisliCat m) (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) :
(xs ≫ ys) a = xs a >>= ys :=
rfl
#align category_theory.Kleisli.comp_def CategoryTheory.KleisliCat.comp_def
instance : Inhabited (KleisliCat id) :=
⟨PUnit⟩
instance {α : Type u} [Inhabited α] : Inhabited (KleisliCat.mk id α) :=
⟨show α from default⟩
end CategoryTheory