feat(category_theory/kleisli): monoids, const applicative functor and…

… kleisli categories (#660)

* feat(category_theory/kleisli): monoids, const applicative functor and
kleisli categories

src/algebra/group.lean

@@ -354,6 +354,32 @@ instance [add_monoid α] : monoid (multiplicative α) :=
   mul_one := @add_zero _ _,
   ..multiplicative.semigroup }
 
+def free_monoid (α) := list α
+
+instance {α} : monoid (free_monoid α) :=
+{ one := [],
+  mul := λ x y, (x ++ y : list α),
+  mul_one := by intros; apply list.append_nil,
+  one_mul := by intros; refl,
+  mul_assoc := by intros; apply list.append_assoc }
+
+@[simp] lemma free_monoid.one_def {α} : (1 : free_monoid α) = [] := rfl
+
+@[simp] lemma free_monoid.mul_def {α} (xs ys : list α) : (xs * ys : free_monoid α) = (xs ++ ys : list α) := rfl
+
+def free_add_monoid (α) := list α
+
+instance {α} : add_monoid (free_add_monoid α) :=
+{ zero := [],
+  add := λ x y, (x ++ y : list α),
+  add_zero := by intros; apply list.append_nil,
+  zero_add := by intros; refl,
+  add_assoc := by intros; apply list.append_assoc }
+
+@[simp] lemma free_add_monoid.zero_def {α} : (1 : free_monoid α) = [] := rfl
+
+@[simp] lemma free_add_monoid.add_def {α} (xs ys : list α) : (xs * ys : free_monoid α) = (xs ++ ys : list α) := rfl
+
 section monoid
   variables [monoid α] {a b c : α}
 

src/category/applicative.lean

@@ -55,40 +55,6 @@ end lemmas
 instance : is_comm_applicative id :=
 by refine { .. }; intros; refl
 
-namespace const
-open functor
-variables {γ : Type u} [monoid γ]
-
-protected def pure {α} (x : α) : const γ α := (1 : γ)
-protected def seq {α β : Type*} (f : const γ (α → β)) (x : const γ α) : const γ β :=
-(f * x : γ)
-
-instance : applicative (const γ) :=
-{ pure := @const.pure γ _,
-  seq := @const.seq γ _ }
-
-instance : is_lawful_applicative (const γ) :=
-by refine { .. }; intros; simp! [const.seq,const.pure,mul_assoc]
-
-end const
-
-namespace add_const
-open functor
-variables {γ : Type u} [add_monoid γ]
-
-protected def pure {α} (x : α) : add_const γ α := (0 : γ)
-protected def seq {α β : Type*} (f : add_const γ (α → β)) (x : add_const γ α) : add_const γ β :=
-(f + x : γ)
-
-instance : applicative (add_const γ) :=
-{ pure := @add_const.pure γ _,
-  seq  := @add_const.seq γ _ }
-
-instance : is_lawful_applicative (add_const γ) :=
-by refine { .. }; intros; simp! [add_const.seq,add_const.pure,add_assoc]
-
-end add_const
-
 namespace comp
 
 open function (hiding comp)
@@ -175,3 +141,17 @@ lemma comp.seq_mk {α β : Type w}
   [applicative f] [applicative g]
   (h : f (g (α → β))) (x : f (g α)) :
   comp.mk h <*> comp.mk x = comp.mk (has_seq.seq <$> h <*> x) := rfl
+
+instance {α} [has_one α] [has_mul α] : applicative (const α) :=
+{ pure := λ β x, (1 : α),
+  seq := λ β γ f x, (f * x : α) }
+
+instance {α} [monoid α] : is_lawful_applicative (const α) :=
+by refine { .. }; intros; simp [mul_assoc]
+
+instance {α} [has_zero α] [has_add α] : applicative (add_const α) :=
+{ pure := λ β x, (0 : α),
+  seq := λ β γ f x, (f + x : α) }
+
+instance {α} [add_monoid α] : is_lawful_applicative (add_const α) :=
+by refine { .. }; intros; simp

src/category/basic.lean

@@ -73,6 +73,8 @@ by simp [(pure_seq_eq_map _ _).symm]; simp [seq_assoc]
 end applicative
 
 -- TODO: setup `functor_norm` for `monad` laws
+attribute [functor_norm] pure_bind bind_assoc bind_pure
+
 section monad
 variables {m : Type u → Type v} [monad m] [is_lawful_monad m]
 
@@ -95,6 +97,28 @@ by rw [← bind_pure_comp_eq_map, bind_assoc]; simp [pure_bind]
 lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x)) :=
 (bind_map_eq_seq m f x).symm
 
+/-- This is the Kleisli composition -/
+@[reducible] def fish {m} [monad m] {α β γ} (f : α → m β) (g : β → m γ) := λ x, f x >>= g
+
+-- >=> is already defined in the core library but it is unusable
+-- because of its precedence (it is defined with precedence 2) and
+-- because it is defined as a lambda instead of having a named
+-- function
+infix ` >=> `:55 := fish
+
+@[functor_norm]
+lemma fish_pure {α β} (f : α → m β) : f >=> pure = f :=
+by simp only [(>=>)] with functor_norm
+
+@[functor_norm]
+lemma fish_pipe {α β} (f : α → m β) : pure >=> f = f :=
+by simp only [(>=>)] with functor_norm
+
+@[functor_norm]
+lemma fish_assoc {α β γ φ} (f : α → m β) (g : β → m γ) (h : γ → m φ) :
+  (f >=> g) >=> h = f >=> (g >=> h) :=
+by simp only [(>=>)] with functor_norm
+
 variables {β' γ' : Type v}
 variables {m' : Type v → Type w} [monad m']
 

src/category/functor.lean

@@ -43,10 +43,11 @@ def id.mk {α : Sort u} : α → id α := id
 namespace functor
 
 def const (α : Type*) (β : Type*) := α
-def add_const (α : Type*) := const α
 
 @[pattern] def const.mk {α β} (x : α) : const α β := x
 
+def const.mk' {α} (x : α) : const α punit := x
+
 def const.run {α β} (x : const α β) : α := x
 
 namespace const
@@ -57,17 +58,25 @@ protected def map {γ α β} (f : α → β) (x : const γ β) : const γ α :=
 
 instance {γ} : functor (const γ) :=
 { map := @const.map γ }
-instance add_const.functor {γ} : functor (add_const γ) :=
-@const.functor γ
 
 instance {γ} : is_lawful_functor (const γ) :=
 by constructor; intros; refl
 
+end const
+
+def add_const (α : Type*) := const α
+
+@[pattern]
+def add_const.mk {α β} (x : α) : add_const α β := x
+
+def add_const.run {α β} : add_const α β → α := id
+
+instance add_const.functor {γ} : functor (add_const γ) :=
+@const.functor γ
+
 instance add_const.is_lawful_functor {γ} : is_lawful_functor (add_const γ) :=
 @const.is_lawful_functor γ
 
-end const
-
 /-- `functor.comp` is a wrapper around `function.comp` for types.
     It prevents Lean's type class resolution mechanism from trying
     a `functor (comp F id)` when `functor F` would do. -/

src/category/traversable/basic.lean

@@ -20,9 +20,9 @@ variables (F : Type u → Type v) [applicative F] [is_lawful_applicative F]
 variables (G : Type u → Type w) [applicative G] [is_lawful_applicative G]
 
 structure applicative_transformation : Type (max (u+1) v w) :=
-(app : ∀ {α : Type u}, F α → G α)
-(preserves_pure' : ∀ {α : Type u} (x : α), app (pure x) = pure x)
-(preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app (x <*> y) = app x <*> app y)
+(app : ∀ α : Type u, F α → G α)
+(preserves_pure' : ∀ {α : Type u} (x : α), app _ (pure x) = pure x)
+(preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y)
 
 end applicative_transformation
 
@@ -31,7 +31,9 @@ namespace applicative_transformation
 variables (F : Type u → Type v) [applicative F] [is_lawful_applicative F]
 variables (G : Type u → Type w) [applicative G] [is_lawful_applicative G]
 
-instance : has_coe_to_fun (applicative_transformation F G) := ⟨_, λ m, m.app⟩
+instance : has_coe_to_fun (applicative_transformation F G) :=
+{ F := λ _, Π {α}, F α → G α,
+  coe := λ a, a.app }
 
 variables {F G}
 variables (η : applicative_transformation F G)

src/category_theory/category.lean

@@ -38,32 +38,34 @@ class has_hom (obj : Type u) : Type (max u (v+1)) :=
 
 infixr ` ⟶ `:10 := has_hom.hom -- type as \h
 
+class category_struct (obj : Type u)
+extends has_hom.{v} obj :=
+(id       : Π X : obj, hom X X)
+(comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
+
+notation `𝟙` := category_struct.id -- type as \b1
+infixr ` ≫ `:80 := category_struct.comp -- type as \gg
+
 /--
 The typeclass `category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
 -/
-class category (obj : Type u) extends has_hom.{v} obj : Type (max u (v+1)) :=
-(id       : Π X : obj, X ⟶ X)
-(notation `𝟙` := id)
-(comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
-(infixr ` ≫ `:80 := comp)
-(id_comp' : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f . obviously)
-(comp_id' : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f . obviously)
-(assoc'   : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
+class category (obj : Type u)
+extends category_struct.{v} obj :=
+(id_comp' : ∀ {X Y : obj} (f : hom X Y), 𝟙 X ≫ f = f . obviously)
+(comp_id' : ∀ {X Y : obj} (f : hom X Y), f ≫ 𝟙 Y = f . obviously)
+(assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z),
   (f ≫ g) ≫ h = f ≫ (g ≫ h) . obviously)
 
-notation `𝟙` := category.id -- type as \b1
-infixr ` ≫ `:80 := category.comp -- type as \gg
-
 -- `restate_axiom` is a command that creates a lemma from a structure field,
 -- discarding any auto_param wrappers from the type.
 -- (It removes a backtick from the name, if it finds one, and otherwise adds "_lemma".)
 restate_axiom category.id_comp'
 restate_axiom category.comp_id'
 restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
-attribute [trans] category.comp
+attribute [trans] category_struct.comp
 
 lemma category.assoc_symm {C : Type u} [category.{v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
   f ≫ (g ≫ h) = (f ≫ g) ≫ h :=
@@ -118,12 +120,19 @@ instance [preorder α] : small_category α :=
   comp := λ X Y Z f g, ⟨ ⟨ le_trans f.down.down g.down.down ⟩ ⟩ }
 
 section
-variables {C : Type u} [𝒞 : category.{v} C]
-include 𝒞
+variables {C : Type u}
+
+def End [has_hom.{v} C] (X : C) := X ⟶ X
+
+instance End.has_one [category_struct.{v} C] {X : C} : has_one (End X) := by refine { one := 𝟙 X }
+instance End.has_mul [category_struct.{v} C] {X : C} : has_mul (End X) := by refine { mul := λ x y, x ≫ y }
+instance End.monoid [category.{v} C] {X : C} : monoid (End X) :=
+by refine { .. End.has_one, .. End.has_mul, .. }; dsimp [has_mul.mul,has_one.one]; obviously
+
+@[simp] lemma End.one_def {C : Type u} [category_struct.{v} C] {X : C} : (1 : End X) = 𝟙 X := rfl
 
-def End (X : C) := X ⟶ X
+@[simp] lemma End.mul_def {C : Type u} [category_struct.{v} C] {X : C} (xs ys : End X) : xs * ys = xs ≫ ys := rfl
 
-instance {X : C} : monoid (End X) := by refine { one := 𝟙 X, mul := λ x y, x ≫ y, .. } ; obviously
 end
 
 end category_theory

src/category_theory/instances/kleisli.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+
+The Kleisli construction on the Type category
+-/
+import category_theory.category
+
+universes u v
+
+namespace category_theory
+
+def Kleisli (m) [monad.{u v} m] := Type u
+
+def Kleisli.mk (m) [monad.{u v} m] (α : Type u) : Kleisli m := α
+
+instance Kleisli.category_struct {m} [monad m] : category_struct (Kleisli m) :=
+{ hom := λ α β, α → m β,
+  id := λ α x, (pure x : m α),
+  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
+
+@[simp] lemma Kleisli.id_def {m} [monad m] [is_lawful_monad m] (α : Kleisli m) :
+  𝟙 α = @pure m _ α := rfl
+
+lemma Kleisli.comp_def {m} [monad m] [is_lawful_monad m] (α β γ : Kleisli m)
+  (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) :
+  (xs ≫ ys) a = xs a >>= ys := rfl
+
+end category_theory

src/category_theory/instances/rings.lean

@@ -7,7 +7,6 @@ Introduce CommRing -- the category of commutative rings.
 Currently only the basic setup.
 -/
 
-import category_theory.concrete_category
 import category_theory.instances.monoids
 import category_theory.fully_faithful
 import category_theory.adjunction

src/category_theory/natural_isomorphism.lean

@@ -127,8 +127,8 @@ variables {C : Type u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
 def ulift_down_up : ulift_down.{v₁} C ⋙ ulift_up C ≅ functor.id (ulift.{u₂} C) :=
-{ hom := { app := λ X, @category.id (ulift.{u₂} C) _ X },
-  inv := { app := λ X, @category.id (ulift.{u₂} C) _ X } }
+{ hom := { app := λ X, @category_struct.id (ulift.{u₂} C) _ X },
+  inv := { app := λ X, @category_struct.id (ulift.{u₂} C) _ X } }
 
 def ulift_up_down : ulift_up.{v₁} C ⋙ ulift_down C ≅ functor.id C :=
 { hom := { app := λ X, 𝟙 X },

src/category_theory/opposites.lean

@@ -47,6 +47,11 @@ attribute [irreducible] opposite
 @[simp] lemma unop_op (X : C) : unop (op X) = X := rfl
 @[simp] lemma op_unop (X : Cᵒᵖ) : op (unop X) = X := rfl
 
+lemma op_inj : function.injective (@op C) :=
+by { rintros _ _ ⟨ ⟩, refl }
+lemma unop_inj : function.injective (@unop C) :=
+by { rintros _ _ ⟨ ⟩, refl }
+
 section has_hom
 
 variables [𝒞 : has_hom.{v₁} C]
@@ -173,4 +178,27 @@ end
 
 end functor
 
+omit 𝒞
+
+instance opposite.has_one [has_one C] : has_one (Cᵒᵖ) :=
+{ one := op 1 }
+
+instance opposite.has_mul [has_mul C] : has_mul (Cᵒᵖ) :=
+{ mul := λ x y, op $ unop y * unop  x }
+
+@[simp] lemma opposite.unop_one [has_one C] : unop (1 : Cᵒᵖ) = (1 : C) := rfl
+
+@[simp] lemma opposite.unop_mul [has_mul C] (xs ys : Cᵒᵖ) : unop (xs * ys) = (unop ys * unop xs : C) := rfl
+
+@[simp] lemma opposite.op_one [has_one C] : op (1 : C) = 1 := rfl
+
+@[simp] lemma opposite.op_mul [has_mul C] (xs ys : C) : op (xs * ys) = (op ys * op xs) := rfl
+
+instance opposite.monoid [monoid C] : monoid (Cᵒᵖ) :=
+{ one := op 1,
+  mul := λ x y, op $ unop y * unop  x,
+  mul_one := by { intros, apply unop_inj, simp },
+  one_mul := by { intros, simp },
+  mul_assoc := by { intros, simp [mul_assoc], } }
+
 end category_theory

src/data/fintype.lean

@@ -536,7 +536,7 @@ suffices f ∈ perms_of_list l ∨ ∃ (b : α), b ∈ l ∧ ∃ g : perm α, g
     if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.bijective.1 h) hfa))
       else this _ $ by simp [mul_apply, swap_apply_def]; split_ifs; cc,
     ⟨swap a (f a) * f, mem_perms_of_list_of_mem this,
-      by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← one_def, one_mul]⟩⟩)
+      by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← equiv.perm.one_def, one_mul]⟩⟩)
 
 lemma mem_of_mem_perms_of_list : ∀ {l : list α} {f : perm α}, f ∈ perms_of_list l → ∀ {x}, f x ≠ x → x ∈ l
 | []     f h := have f = 1 := by simpa [perms_of_list] using h, by rw this; simp