From 248e035402dc90be1ee36848d723416c3953bbff Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 6 Jan 2018 00:56:46 +0100 Subject: [PATCH] fix(init/category/transformers): make has_monad_lift more universe polymorphic --- library/init/category/transformers.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/category/transformers.lean b/library/init/category/transformers.lean index abe9f7d6d8..8461910569 100644 --- a/library/init/category/transformers.lean +++ b/library/init/category/transformers.lean @@ -16,13 +16,13 @@ class monad_transformer (transformer : ∀ (m : Type u → Type v) [monad m], Ty instance transformed_monad (m t) [monad_transformer t] [monad m] : monad (t m) := monad_transformer.is_monad t m -class has_monad_lift (m n : Type u → Type v) := +class has_monad_lift (m : Type u → Type v) (n : Type u → Type w) := (monad_lift : ∀ α, m α → n α) instance monad_transformer_lift (t m) [monad_transformer t] [monad m] : has_monad_lift m (t m) := ⟨monad_transformer.monad_lift t m⟩ -class has_monad_lift_t (m n : Type u → Type v) := +class has_monad_lift_t (m : Type u → Type v) (n : Type u → Type w) := (monad_lift : ∀ α, m α → n α) def monad_lift {m n} [has_monad_lift_t m n] {α} : m α → n α :=