rm a couple of the functor (#141)

impredicative_set/imonad_lib.v

@@ -221,6 +221,7 @@ Proof. by rewrite functor_o. Qed.
 
 Section id_natural_transformation.
 Variables C : functor.
+
 Definition NId := fun A => @idfun (C A).
 Let natural_id : naturality C C NId. Proof. by []. Qed.
 
@@ -525,47 +526,31 @@ Qed.
 
 End composite_adjoint.
 
-Definition operation (E : functor) (M : monad) := [the functor of E \o M] ~> M.
+Definition operation (E : functor) (M : monad) := E \o M ~> M.
 Notation "E .-operation M" := (operation E M).
 
 Section algebraicity.
 Variables (E : functor) (M : monad).
-Definition algebraicity (op : (*E.-operation M*)E \o M ~~> M) :=
+Definition algebraicity (op : E \o M ~~> M) :=
   forall (A B : UU0) (f : A -> M B) (t : E (M A)),
     op A t >>= f = op B ((E # (fun m => m >>= f)) t).
 End algebraicity.
 
 HB.mixin Record isAOperation (E : functor) (M : monad) (op : E \o M ~~> M) := {
   algebraic : algebraicity op }.
+
+#[short(type=aoperation)]
 HB.structure Definition AOperation (E : functor) (M : monad) :=
   {op of isAOperation E M op &
-         isNatural [the functor of E \o M] M op (*NB: this is an operation in fact*)}.
-Notation aoperation := AOperation.type.
-Arguments algebraic {E} {M} s.
+         isNatural (E \o M) M op (*NB: this is an operation in fact*)}.
 
-(*Module AOperation.
-Section aoperation.
-Variables (E : functor) (M : monad).
-Record mixin_of (op : E \O M ~> M) := Mixin { _ : algebraicity op }.
-Record class_of (op : E \O M ~~> M) := Class {
-  base : Natural.mixin_of op ;
-  mixin : mixin_of (Natural.Pack base) }.
-Structure t := Pack { m : E \O M ~~> M ; class : class_of m }.
-Definition baseType (o : t) := Natural.Pack (base (class o)).
-End aoperation.
-Module Exports.
-Arguments m {E} {M}.
-Notation aoperation := t.
-Coercion baseType : aoperation >-> nattrans.
-Canonical baseType.
-End Exports.
-End AOperation.
-Export AOperation.Exports.*)
+Arguments algebraic {E} {M} s.
 
 Notation "E .-aoperation M" := (aoperation E M).
 
 Section algebraic_operation_interface.
 Variables (E : functor) (M : monad) (op : E.-aoperation M).
+
 Lemma aoperation_ext (f g : E.-aoperation M) :
   f = g <-> forall a, (f a = g a :> (_ -> _)).
 Proof.