Composition of effects function added

Author: clarus

src/Effect.v

@@ -2,3 +2,11 @@
 Record t := New {
   command : Type;
   answer : command -> Type }.
+
+(** The composition of two effects. *)
+Definition compose (E1 E2 : t) : t :=
+  New (command E1 + command E2) (fun c =>
+    match c with
+    | inl c1 => answer E1 c1
+    | inr c2 => answer E2 c2
+    end).