minor edits

affeldt-aist · Jul 10, 2024 · b0798ad · b0798ad
1 parent 9ae4ea0
commit b0798ad
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/impredicative_set/imonad_lib.v b/impredicative_set/imonad_lib.v
@@ -646,7 +646,7 @@ Qed.
 
 Definition commute {M : monad} A B (m : M A) (n : M B) C (f : A -> B -> M C) : Prop :=
   m >>= (fun x => n >>= (fun y => f x y)) =
-  n >>= (fun y => m >>= (fun x => f x y)) :> M _.
+  n >>= (fun y => m >>= (fun x => f x y)).
 
 Definition preserves {M : monad} (A B : UU0) (f : A -> M A) (g : A -> B) :=
   forall x, (f x >>= fun y => Ret (y, g y)) = (f x >>= fun y => Ret (y, g x)).

diff --git a/monad_lib.v b/monad_lib.v
@@ -648,7 +648,7 @@ Qed.
 
 Definition commute {M : monad} A B (m : M A) (n : M B) C (f : A -> B -> M C) : Prop :=
   m >>= (fun x => n >>= (fun y => f x y)) =
-  n >>= (fun y => m >>= (fun x => f x y)) :> M _.
+  n >>= (fun y => m >>= (fun x => f x y)).
 
 Definition preserves {M : monad} (A B : UU0) (f : A -> M A) (g : A -> B) :=
   forall x, (f x >>= fun y => Ret (y, g y)) = (f x >>= fun y => Ret (y, g x)).

diff --git a/monad_transformer.v b/monad_transformer.v
@@ -152,7 +152,7 @@ Lemma MS_bindE [S : UU0] [M : monad] [A B : UU0] (m : MS S M A) (f : A -> MS S M
   (m >>= f) s = m s >>= uncurry f.
 Proof. by []. Qed.
 
-Definition stateT (S : UU0) : monad -> monad := MS S.
+Definition stateT : UU0 -> monad -> monad := MS.
 
 HB.instance Definition _ (S : UU0) := isMonadT.Build
   (stateT S) (@liftS S).