diff --git a/.DS_Store b/.DS_Store
new file mode 100644
index 00000000..6e68ebe8
Binary files /dev/null and b/.DS_Store differ
diff --git a/examples/Wrappers.dfy b/examples/Wrappers.dfy
index f9f5b111..f40a5716 100644
--- a/examples/Wrappers.dfy
+++ b/examples/Wrappers.dfy
@@ -10,6 +10,9 @@ include "../src/Wrappers.dfy"
 
 module Demo {
   import opened Wrappers
+  import opened Wrappers.Option
+  import opened Wrappers.Result
+  import opened Wrappers.Outcome
 
   // ------ Demo for Option ----------------------------
   // We use Option when we don't need to pass around a reason for the failure,
@@ -60,7 +63,7 @@ module Demo {
   // Sometimes we want to go from Option to Result:
   method FindName(m: MyMap<string, string>) returns (res: Result<string, string>) {
     // Will return a default error message in case of None:
-    res := m.Get("name").ToResult();
+    res := ToResult(m.Get("name"));
     // We can also match on the option to write a custom error:
     match m.Get("name")
     case Some(n) => res := Success(n);
diff --git a/src/Collections/Arrays/BinarySearch.dfy b/src/Collections/Arrays/BinarySearch.dfy
index d8bfeb4f..03f6d450 100644
--- a/src/Collections/Arrays/BinarySearch.dfy
+++ b/src/Collections/Arrays/BinarySearch.dfy
@@ -9,7 +9,7 @@ include "../../Wrappers.dfy"
 include "../../Relations.dfy"
 
 module BinarySearch {
-  import opened Wrappers
+  import opened Wrappers.Option
   import opened Relations
 
   method BinarySearch<T>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>)
diff --git a/src/Collections/Maps/Imaps.dfy b/src/Collections/Maps/Imaps.dfy
index b5da6de7..e1c4829d 100644
--- a/src/Collections/Maps/Imaps.dfy
+++ b/src/Collections/Maps/Imaps.dfy
@@ -12,7 +12,7 @@
 include "../../Wrappers.dfy"
 
 module {:options "-functionSyntax:4"} Imaps {
-  import opened Wrappers
+  import opened Wrappers.Option
 
   function Get<X, Y>(m: imap<X, Y>, x: X): Option<Y>
   {
diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
index f666d8c4..8eb2d803 100644
--- a/src/Collections/Maps/Maps.dfy
+++ b/src/Collections/Maps/Maps.dfy
@@ -12,7 +12,7 @@
 include "../../Wrappers.dfy"
 
 module {:options "-functionSyntax:4"} Maps {
-  import opened Wrappers
+  import opened Wrappers.Option
 
   function Get<X, Y>(m: map<X, Y>, x: X): Option<Y>
   {
diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
index 60c9612d..09b17bee 100644
--- a/src/Collections/Sequences/Seq.dfy
+++ b/src/Collections/Sequences/Seq.dfy
@@ -20,7 +20,8 @@ include "../../Relations.dfy"
 
 module {:options "-functionSyntax:4"} Seq {
 
-  import opened Wrappers
+  import opened Wrappers.Option
+  import opened Wrappers.Result  
   import opened MergeSort
   import opened Relations
   import Math
@@ -613,7 +614,7 @@ module {:options "-functionSyntax:4"} Seq {
 /* Applies a function to every element of a sequence, returning a Result value (which is a 
    failure-compatible type). Returns either a failure, or, if successful at every element, 
    the transformed sequence.  */
-  function {:opaque} MapWithResult<T, R, E>(f: (T ~> Result<R,E>), xs: seq<T>): (result: Result<seq<R>, E>)
+  function {:opaque} MapWithResult<T, R(!new), E(!new)>(f: (T ~> Result<R,E>), xs: seq<T>): (result: Result<seq<R>, E>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
     ensures result.Success? ==>
       && |result.value| == |xs|
diff --git a/src/Comonad.dfy b/src/Comonad.dfy
new file mode 100644
index 00000000..93bb4ac7
--- /dev/null
+++ b/src/Comonad.dfy
@@ -0,0 +1,172 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+include "Functor.dfy"
+include "Cowrappers.dfy"
+
+abstract module {:options "-functionSyntax:4"} Comonad refines Functor {
+  /* Structure  */
+  type F(!new)<T(!new)>
+
+  function Extract<T(!new)>(w: F<T>): T
+
+  function Duplicate<T(!new)>(w: F<T>): F<F<T>>
+
+  /* Naturality */
+  lemma LemmaExtractNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>)
+    requires EquivalenceRelation(eq)
+    ensures eq(f(Extract(w)), Extract(Map(f)(w)))
+
+  lemma LemmaDuplicateNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>)
+    requires EquivalenceRelation(eq)
+    ensures EquivalenceRelation(Equal(eq))
+    ensures Equal(Equal(eq))(Duplicate(Map(f)(w)), Map(Map(f))(Duplicate(w)))
+
+  /* Counitality and Coassociativity */
+  lemma LemmaCoUnitalityExtract<T(!new)>(eq: (T, T) -> bool, w: F<T>)
+    requires EquivalenceRelation(eq)
+    ensures && Equal(eq)(Map(Extract)(Duplicate(w)), w)
+            && Equal(eq)(w, Extract(Duplicate(w)))
+ 
+  lemma LemmaCoAssociativityDuplicate<T(!new)>(eq: (T, T) -> bool, w: F<T>) 
+    requires && EquivalenceRelation(eq)
+             && EquivalenceRelation(Equal(eq))
+             && EquivalenceRelation(Equal(Equal(eq))) 
+    ensures Equal(Equal(Equal(eq)))(Map(Duplicate)(Duplicate(w)), Duplicate(Duplicate(w)))
+}
+
+abstract module {:options "-functionSyntax:4"} CoreaderRightComonad refines Comonad {
+  import Cowrappers.Coreader
+
+  type X(!new)
+
+  function eql(x: X, y: X): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eql)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Coreader.Coreader<X,T>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Coreader.MapRight(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Coreader.Equal(eql, eq)
+  }  
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Comonad structure */
+  function Extract<T(!new)>(w: F<T>): T {
+    Coreader.ExtractRight(w)
+  } 
+
+  function Duplicate<T(!new)>(w: F<T>): F<F<T>> {
+    Coreader.DuplicateLeft(w)
+  }
+
+  /* Naturality */
+  lemma LemmaExtractNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+  }
+
+  lemma LemmaDuplicateNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  /* Counitality and Coassociativity */
+  lemma LemmaCoUnitalityExtract<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+ 
+  lemma LemmaCoAssociativityDuplicate<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+}
+
+abstract module {:options "-functionSyntax:4"} CoreaderLeftComonad refines Comonad {
+  import Cowrappers.Coreader
+
+  type X(!new)
+
+  function eqr(x: X, y: X): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eqr)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Coreader.Coreader<T,X>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Coreader.MapLeft(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Coreader.Equal(eq, eqr)
+  }  
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Comonad structure */
+  function Extract<T(!new)>(w: F<T>): T {
+    Coreader.ExtractLeft(w)
+  } 
+
+  function Duplicate<T(!new)>(w: F<T>): F<F<T>> {
+    Coreader.DuplicateRight(w)
+  }
+
+  /* Naturality */
+  lemma LemmaExtractNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+  }
+
+  lemma LemmaDuplicateNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  /* Counitality and Coassociativity */
+  lemma LemmaCoUnitalityExtract<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+ 
+  lemma LemmaCoAssociativityDuplicate<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+}
\ No newline at end of file
diff --git a/src/Cowrappers.dfy b/src/Cowrappers.dfy
new file mode 100644
index 00000000..f95c3302
--- /dev/null
+++ b/src/Cowrappers.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+module {:options "-functionSyntax:4"} Cowrappers {
+  module {:options "-functionSyntax:4"} Coreader {
+
+  datatype Coreader<+S,+T> = Coreader(left: S, right: T)
+
+  function ExtractRight<S,T>(r: Coreader<S,T>): T {
+    r.right
+  }
+
+  function ExtractLeft<S,T>(r: Coreader<S,T>): S {
+    r.left
+  }
+
+  function DuplicateLeft<S,T>(r: Coreader<S,T>): Coreader<S,Coreader<S,T>> {
+    Coreader(r.left, r)
+  }
+
+  function DuplicateRight<S,T>(r: Coreader<S,T>): Coreader<Coreader<S,T>,T> {
+    Coreader(r, r.right)
+  }
+
+  function ExtendRight<S,T1,T2>(f: Coreader<S,T1> -> T2, r: Coreader<S,T1>): Coreader<S,T2> {
+    Coreader(r.left, f(r))
+  }
+
+  function ExtendLeft<S1,S2,T>(f: Coreader<S1,T> -> S2, r: Coreader<S1,T>): Coreader<S2,T> {
+    Coreader(f(r), r.right)
+  }
+
+  function MapRight<S,T1,T2>(f: T1 -> T2): Coreader<S,T1> -> Coreader<S,T2> {
+    (r: Coreader<S,T1>) => 
+      Coreader(r.left, f(r.right))
+  }
+
+  function MapLeft<S1,S2,T>(f: S1 -> S2): Coreader<S1,T> -> Coreader<S2,T> {
+    (r: Coreader<S1,T>) => 
+      Coreader(f(r.left), r.right)
+  }
+
+  function KleisliCompositionRight<S,T1,T2,T3>(f: Coreader<S,T1> -> T2, g: Coreader<S,T2> -> T3): Coreader<S,T1> -> T3 {
+    r => g(ExtendRight(f, r))
+  }
+
+  function KleisliCompositionLeft<S1,S2,S3,T>(f: Coreader<S1,T> -> S2, g: Coreader<S2,T> -> S3): Coreader<S1,T> -> S3 {
+    r => g(ExtendLeft(f, r))
+  }
+
+  ghost function Equal<S,T>(eql: (S, S) -> bool, eqr: (T, T) -> bool): (Coreader<S,T>, Coreader<S,T>) -> bool {
+    (r1: Coreader<S,T>, r2: Coreader<S,T>) =>
+      eql(r1.left, r2.left) && eqr(r1.right, r2.right)
+  }
+
+  }
+}
\ No newline at end of file
diff --git a/src/FileIO/FileIO.dfy b/src/FileIO/FileIO.dfy
index 48ea0950..928502fd 100644
--- a/src/FileIO/FileIO.dfy
+++ b/src/FileIO/FileIO.dfy
@@ -18,9 +18,9 @@ include "../Wrappers.dfy"
  * File path symbols including . and .. are allowed.
  */
 module {:options "-functionSyntax:4"} FileIO {
-  import opened Wrappers
+  import opened Wrappers.Result
 
-  export provides ReadBytesFromFile, WriteBytesToFile, Wrappers
+  export provides ReadBytesFromFile, WriteBytesToFile, Result
 
   /*
    * Public API
diff --git a/src/Functions.dfy b/src/Functions.dfy
index 85757547..17eb2aa5 100644
--- a/src/Functions.dfy
+++ b/src/Functions.dfy
@@ -21,4 +21,8 @@ module {:options "-functionSyntax:4"} Functions {
     forall x1, x2 :: f(x1) == f(x2) ==> x1 == x2
   }
 
+  function Composition<X,Y,Z>(f: X -> Y, g: Y -> Z): X -> Z {
+    x => g(f(x))
+  }
+
 }
diff --git a/src/Functor.dfy b/src/Functor.dfy
new file mode 100644
index 00000000..16244a74
--- /dev/null
+++ b/src/Functor.dfy
@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+include "Functions.dfy"
+include "Relations.dfy"
+
+abstract module {:options "-functionSyntax:4"} Functor {
+  import opened Functions
+  import opened Relations
+
+  /* Structure */
+  type F(!new)<T(!new)>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T>
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool
+    requires EquivalenceRelation(eq)
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool)
+    requires EquivalenceRelation(eq)
+    ensures EquivalenceRelation(Equal(eq))
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T)
+    requires EquivalenceRelation(eq) 
+    requires forall x: S :: eq(f(x), g(x))
+    ensures forall w: F<S> :: Equal(eq)(Map(f)(w), Map(g)(w))
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>)
+    requires EquivalenceRelation(eq)
+    ensures Equal(eq)(Map(Composition(f, g))(w), Composition(Map(f), Map(g))(w))
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T)
+    requires EquivalenceRelation(eq) 
+    requires forall x: T :: eq(id(x), x)
+    ensures forall w: F<T> :: Equal(eq)(Map(id)(w), w)
+}
\ No newline at end of file
diff --git a/src/Monad.dfy b/src/Monad.dfy
new file mode 100644
index 00000000..723dc999
--- /dev/null
+++ b/src/Monad.dfy
@@ -0,0 +1,435 @@
+// RUN: %dafny /compile:0 "%s"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+include "Functor.dfy"
+include "Wrappers.dfy"
+
+abstract module {:options "-functionSyntax:4"} Monad refines Functor {
+  /* Structure  */
+  type F(!new)<T(!new)>
+
+  function Return<T(!new)>(x: T): F<T>
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T>
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S)
+    requires EquivalenceRelation(eq)
+    ensures Equal(eq)(Map(f)(Return(x)), Return(f(x)))
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>)
+    requires EquivalenceRelation(eq)
+    ensures Equal(eq)(Join(Map(Map(f))(ww)), Map(f)(Join(ww)))
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>)
+    requires EquivalenceRelation(eq)
+    ensures Equal(eq)(Join(Map(Return)(w)), w) && Equal(eq)(w, Join(Return(w)))
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) 
+    requires EquivalenceRelation(eq)
+    ensures Equal(eq)(Join(Map(Join)(www)), Join(Join(www)))
+}
+
+
+abstract module {:options "-functionSyntax:4"} ResultMonad refines Monad {
+  import Wrappers.Result
+    
+  type E(!new,==)
+
+  function eqe(x: E, y: E): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eqe)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Result.Result<T,E>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Result.Map(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Result.Equal(eq, eqe)
+  }    
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Monad structure */
+  function Return<T(!new)>(x: T): F<T> {
+    Result.Return(x)
+  }
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T> {
+    Result.Join(ww)
+  }
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S) {
+  }
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>) {
+    LemmaEquiv();
+  }
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) {
+    LemmaEquiv();
+  }
+}
+
+
+module {:options "-functionSyntax:4"} WriterMonad refines Monad {
+  import Wrappers.Writer 
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Writer.Writer<T>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Writer.Map(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Writer.Equal(eq)
+  }    
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+  }
+
+  /* Monad structure */
+  function Return<T(!new)>(x: T): F<T> {
+    Writer.Return(x)
+  }
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T> {
+    Writer.Join(ww)
+  }
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S) {
+  }
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>) {
+  }
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+  }
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) {
+  }
+}
+
+
+module {:options "-functionSyntax:4"} OptionMonad refines Monad {
+  import Wrappers.Option
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Option.Option<T>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Option.Map(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Option.Equal(eq)
+  }    
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+  }
+
+  /* Monad structure */
+  function Return<T(!new)>(x: T): F<T> {
+    Option.Return(x)
+  }
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T> {
+    Option.Join(ww)
+  }
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S) {
+  }
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>) {
+  }
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+  }
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) {
+  }
+}
+
+
+abstract module {:options "-functionSyntax:4"} EitherRightMonad refines Monad {
+  import Wrappers.Either 
+
+  type X(!new)
+
+  function eql(x: X, y: X): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eql)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Either.Either<X,T>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Either.MapRight(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Either.Equal(eql, eq)
+  }  
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Monad structure */
+  function Return<T(!new)>(x: T): F<T> {
+    Either.ReturnRight(x)
+  }
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T> {
+    Either.JoinRight(ww)
+  }
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S) {
+  }
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>) {
+    LemmaEquiv();
+  }
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) {
+    LemmaEquiv();
+  }
+}
+
+
+abstract module {:options "-functionSyntax:4"} EitherLeftMonad refines Monad {
+  import Wrappers.Either 
+
+  type X(!new,==)
+
+  function eqr(x: X, y: X): bool
+
+  lemma LemmaEquiv()
+    ensures EquivalenceRelation(eqr)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Either.Either<T,X>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Either.MapLeft(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Either.Equal(eq, eqr)
+  }  
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    LemmaEquiv();
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+    LemmaEquiv();
+  }
+
+  /* Monad structure */
+  function Return<T(!new)>(x: T): F<T> {
+    Either.ReturnLeft(x)
+  }
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T> {
+    Either.JoinLeft(ww)
+  }
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S) {
+  }
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>) {
+    LemmaEquiv();
+  }
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+    LemmaEquiv();
+  }
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) {
+    LemmaEquiv();
+  }
+}
+
+
+abstract module {:options "-functionSyntax:4"} ReaderMonad refines Monad {
+  import Wrappers.Reader
+
+  type X(!new)
+
+  /* Functor structure */
+  type F(!new)<T(!new)> = Reader.Reader<X,T>
+
+  function Map<S(!new),T(!new)>(f: S -> T): F<S> -> F<T> {
+    Reader.Map(f)
+  }
+
+  ghost function Equal<T(!new)>(eq: (T, T) -> bool): (F<T>, F<T>) -> bool {
+    Reader.Equal(eq)
+  }    
+
+  /* Properties of Equal */
+  lemma LemmaEquivRelLift<T(!new)>(eq: (T, T) -> bool) {
+    forall w: F<T> ensures Equal(eq)(w, w) {
+      forall x: X ensures eq(w.f(x), w.f(x)) {
+        assert eq(w.f(x), w.f(x));
+      }
+    }
+    assert Reflexive(Equal(eq));
+
+    forall v, w: F<T> ensures Equal(eq)(v, w) <==> Equal(eq)(w, v) {
+      calc {
+        Equal(eq)(v, w);
+        <==>
+        forall x: X :: eq(v.f(x), w.f(x));
+        <==> { assert Symmetric(eq); }
+        forall x: X :: eq(v.f(x), w.f(x));
+        <==>
+        Equal(eq)(w, v);
+      }
+    }
+    assert Symmetric(Equal(eq));
+
+    forall v, w, u: F<T> ensures Equal(eq)(v, w) && Equal(eq)(w, u) ==> Equal(eq)(v, u) {
+      if Equal(eq)(v, w) && Equal(eq)(w, u) {
+        forall x: X ensures eq(v.f(x), u.f(x)) {
+          calc {
+            eq(v.f(x), w.f(x)) && eq(w.f(x), u.f(x));
+          ==> { assert Transitive(eq); }
+            eq(v.f(x), u.f(x));
+          }
+        }
+      }
+    }
+    assert Transitive(Equal(eq));
+  }
+
+  /* Properties of Map */
+  lemma LemmaMapFunction<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, g: S -> T) {
+  }
+
+  lemma LemmaMapFunctorial<S(!new),T(!new),U(!new)>(eq: (U, U) -> bool, f: S -> T, g: T -> U, w: F<S>) {
+  }
+
+  lemma LemmaMapIdentity<T(!new)>(eq: (T, T) -> bool, id: T -> T) {
+  }
+
+  /* Monad structure */
+  function Return<T(!new)>(x: T): F<T> {
+    Reader.Return(x)
+  }
+
+  function Join<T(!new)>(ww: F<F<T>>): F<T> {
+    Reader.Join(ww)
+  }
+
+  /* Naturality */
+  lemma LemmaReturnNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, x: S) {
+  }
+
+  lemma LemmaJoinNaturality<S(!new),T(!new)>(eq: (T, T) -> bool, f: S -> T, ww: F<F<S>>) {
+  }
+
+  /* Unitality and Associativity */
+  lemma LemmaUnitalityJoin<T(!new)>(eq: (T, T) -> bool, w: F<T>) {
+  }
+
+  lemma LemmaAssociativityJoin<T(!new)>(eq: (T, T) -> bool, www: F<F<F<T>>>) {
+  }
+}
+
+
+
+
+
diff --git a/src/Relations.dfy b/src/Relations.dfy
index ac25532f..93029480 100644
--- a/src/Relations.dfy
+++ b/src/Relations.dfy
@@ -19,6 +19,10 @@ module {:options "-functionSyntax:4"} Relations {
     forall x, y :: R(x, y) && R(y, x) ==> x == y
   }
 
+  ghost predicate Symmetric<T(!new)>(R: (T, T) -> bool) {
+    forall x, y :: R(x, y) <==> R(y, x)
+  }
+
   ghost predicate Connected<T(!new)>(R: (T, T) -> bool) {
     forall x, y :: x != y ==> R(x, y) || R(y, x)
   }
@@ -45,6 +49,12 @@ module {:options "-functionSyntax:4"} Relations {
     && Connected(R)
   }  
 
+  ghost predicate EquivalenceRelation<T(!new)>(R: (T, T) -> bool) {
+    && Reflexive(R)
+    && Symmetric(R)
+    && Transitive(R)
+  }
+
   ghost predicate SortedBy<T>(a: seq<T>, lessThan: (T, T) -> bool) {
     forall i, j | 0 <= i < j < |a| :: lessThan(a[i], a[j])
   }
diff --git a/src/Unicode/Unicode.dfy b/src/Unicode/Unicode.dfy
index 316e61e0..56204168 100644
--- a/src/Unicode/Unicode.dfy
+++ b/src/Unicode/Unicode.dfy
@@ -10,8 +10,6 @@ include "../Collections/Sequences/Seq.dfy"
 
 // This module implements basic functionality of Unicode 14.0.
 module {:options "-functionSyntax:4"} Unicode {
-  import opened Wrappers
-
   import Seq
 
   /**
diff --git a/src/Unicode/UnicodeEncodingForm.dfy b/src/Unicode/UnicodeEncodingForm.dfy
index 1cd3c366..70e77d88 100644
--- a/src/Unicode/UnicodeEncodingForm.dfy
+++ b/src/Unicode/UnicodeEncodingForm.dfy
@@ -26,7 +26,7 @@ include "Unicode.dfy"
  *    code unit subsequences to scalar values.
  */
 abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm {
-  import opened Wrappers
+  import opened Wrappers.Option
 
   import Functions
   import Seq
@@ -48,7 +48,7 @@ abstract module {:options "-functionSyntax:4"} UnicodeEncodingForm {
    * A code unit is the minimal bit combination that can represent a unit of encoded text for processing or
    * interchange. (Section 3.9 D77.)
    */
-  type CodeUnit
+  type CodeUnit(==)
 
   /**
    * A well-formed Unicode code unit sequence that maps to a single Unicode scalar value.
diff --git a/src/Unicode/Utf8EncodingScheme.dfy b/src/Unicode/Utf8EncodingScheme.dfy
index 210e1082..f7a3d813 100644
--- a/src/Unicode/Utf8EncodingScheme.dfy
+++ b/src/Unicode/Utf8EncodingScheme.dfy
@@ -29,8 +29,6 @@ include "Utf8EncodingForm.dfy"
  * but that runs into <https://github.com/dafny-lang/dafny/issues/1639>.
  */
 module {:options "-functionSyntax:4"} Utf8EncodingScheme {
-  import opened Wrappers
-
   import BoundedInts
   import Seq
   import Unicode
diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy
index 22fc4bf5..1b8a098e 100644
--- a/src/Wrappers.dfy
+++ b/src/Wrappers.dfy
@@ -4,96 +4,429 @@
 *  Copyright by the contributors to the Dafny Project
 *  SPDX-License-Identifier: MIT 
 *******************************************************************************/
-
 module {:options "-functionSyntax:4"} Wrappers {
-  
-  datatype Option<+T> = None | Some(value: T) {
-    function ToResult(): Result<T, string> {
-      match this
-      case Some(v) => Success(v)
-      case None() => Failure("Option is None")
+  module {:options "-functionSyntax:4"} Result {
+    import opened Option
+
+    datatype Result<T(!new,==),E(!new)> = | Success(value: T) | Failure(error: E) {
+      predicate IsSuccess() {
+        Success?
+      }  
+
+      predicate IsFailure() {
+        Failure?
+      }  
+
+      function GetValue(): T
+        requires Success?
+      {
+        value
+      }
+
+      function GetValueDefault(default: T): T {
+        match this 
+        case Success(v) => v
+        case Failure(_) => default
+      }
+
+      function PropagateFailure<S>(): Result<S,E>
+        requires Failure?
+      {
+        Failure(error)
+      }
+
+      function GetError(): E 
+        requires Failure?
+      {
+        error
+      }
+
+      function Extract(): T
+        requires Success?
+      {
+        value
+      }
+
+      function ToOption(): Option<T> {
+        match this
+        case Success(v) => Some(v)
+        case Failure(_) => None
+      }
+
+      function ToSeq(): seq<T> {
+        match this
+        case Success(v) => [v]
+        case Failure(_) => []
+      }
+
+      function ToSet(): set<T> {
+        match this
+        case Success(v) => {v}
+        case Failure(_) => {}   
+      }
     }
     
-    function UnwrapOr(default: T): T {
-      match this
-      case Some(v) => v
-      case None() => default
+    function Return<T,E>(v: T): Result<T,E> {
+      Result.Success(v)
     }
 
-    predicate IsFailure() {
-      None?
+    function Bind<S(!new),T(!new),E(!new)>(r: Result<S,E>, f: S -> Result<T,E>): Result<T,E> {
+      match r
+      case Success(v) => f(v)
+      case Failure(e) => Result<T,E>.Failure(e)
     }
 
-    function PropagateFailure<U>(): Option<U>
-      requires None?
-    {
-      None
+    function Join<T(!new,==),E(!new,==)>(rr: Result<Result<T,E>,E>): Result<T,E> {
+      match rr
+      case Success(v) => v
+      case Failure(e) => Result<T,E>.Failure(e)
     }
 
-    function Extract(): T
-      requires Some?
-    {
-      value
+    function Map<S(!new),T(!new),E(!new)>(f: S -> T): Result<S,E> -> Result<T,E> {
+      (r: Result<S,E>) =>
+        match r 
+        case Success(v) => Result<T,E>.Success(f(v))
+        case Failure(e) => Result<T,E>.Failure(e)
+    }
+
+    function MapError<T(!new),E1(!new),E2(!new)>(f: E1 -> E2): Result<T,E1> -> Result<T,E2> {
+      (r: Result<T,E1>) =>
+        match r 
+        case Success(v) => Result<T,E2>.Success(v)
+        case Failure(e) => Result<T,E2>.Failure(f(e))
+    } 
+
+    function KleisliComposition<S(!new),T(!new),U(!new),E(!new)>(f: S -> Result<T,E>, g: T -> Result<U,E>): S -> Result<U,E> {
+      s => Bind(f(s), g)
+    }
+
+    function Success<T,E>(v: T): Result<T,E> {
+      Result.Success(v)
+    }
+
+    function Failure<T,E>(e: E): Result<T,E> {
+      Result.Failure(e)
+    } 
+
+    function Fold<T(!new),E(!new),U>(f: T -> U, g: E -> U): Result<T,E> -> U {
+      (r: Result<T,E>) =>
+        match r 
+        case Success(v) => f(v)
+        case Failure(e) => g(e)
+    }
+
+    function Equal<T(!new),E(!new)>(eqt: (T, T) -> bool, eqe: (E, E) -> bool): (Result<T,E>, Result<T,E>) -> bool {
+      (r1: Result<T,E>, r2: Result<T,E>) =>
+        match (r1, r2)
+        case (Success(v1), Success(v2)) => eqt(v1, v2)
+        case (Failure(e1), Failure(e2)) => eqe(e1, e2)
+        case _ => false
+    }
+
+    function Compare<T(!new),E(!new)>(cmps: (T, T) -> int, cmpf: (E, E) -> int): (Result<T,E>, Result<T,E>) -> int {
+      (r1: Result<T,E>, r2: Result<T,E>) =>
+        match (r1, r2)
+        case (Success(v1), Success(v2)) => cmps(v1, v2)
+        case (Failure(e1), Failure(e2)) => cmpf(e1, e2)
+        case (Success(_), Failure(_)) => -1
+        case (Failure(_), Success(_)) => 1
     }
   }
 
-  datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) {
-    function ToOption(): Option<T> 
-    {
-      match this
-      case Success(s) => Some(s)
-      case Failure(e) => None()
+  module {:options "-functionSyntax:4"} Writer {
+    datatype Writer<T> = Result(value: T, log: string) {
+      function GetValue<T>(w: Writer<T>): T {
+        w.value
+      }
+
+      function GetLog<T>(w: Writer<T>): string {
+        w.log
+      }
     }
 
-    function UnwrapOr(default: T): T 
-    {
-      match this
-      case Success(s) => s
-      case Failure(e) => default
+    function Return<T>(v: T): Writer<T> {
+      Result(v, "")
     }
 
-    predicate IsFailure() {
-      Failure?
+    function Bind<S,T>(w: Writer<S>, f: S -> Writer<T>): Writer<T> {
+      Writer<T>.Result(f(w.value).value, w.log + f(w.value).log)
     }
 
-    function PropagateFailure<U>(): Result<U, R>
-      requires Failure?
-    {
-      Failure(this.error)
+    function Join<T>(ww: Writer<Writer<T>>): Writer<T> {
+      Result((ww.value).value, (ww.value).log + ww.log)
     }
 
-    function MapFailure<NewR>(reWrap: R -> NewR): Result<T, NewR>
-    {
-      match this
-      case Success(s) => Success(s)
-      case Failure(e) => Failure(reWrap(e))
+    function Map<S,T>(f: S -> T): Writer<S> -> Writer<T> {
+      (w: Writer<S>) => Writer<T>.Result(f(w.value), w.log)
+    }
+
+    function KleisliComposition<S,T,U>(f: S -> Writer<T>, g: T -> Writer<U>): S -> Writer<U> {
+      s => Bind(f(s), g)
+    }
+
+    function Result<T>(v: T, s: string): Writer<T> {
+      Writer<T>.Result(v, s)
+    }
+
+    ghost function Equal<T(!new)>(eq: (T, T) -> bool): (Writer<T>, Writer<T>) -> bool {
+      (w1: Writer<T>, w2: Writer<T>) => 
+        && eq(w1.value, w2.value) 
+        && w1.log == w2.log
+    }
+  }
+
+  module {:options "-functionSyntax:4"} Option {
+    datatype Option<+T(==)> = None | Some(value: T) {
+      function GetValueDefault(default: T): T {
+        match this
+        case None => default
+        case Some(v) => v
+      }
+
+      function GetValue(): T
+        requires Some?
+      {
+        value
+      }
+
+      predicate IsFailure() {
+        None?
+      }
+
+      function Extract(): T
+        requires Some?
+      {
+        value
+      }
+
+      function PropagateFailure<S>(): Option<S>
+        requires None?
+      {
+        None
+      }
+
+      function ToSeq(): seq<T> {
+        match this 
+        case None => []
+        case Some(v) => [v]
+      }
+
+      function ToSet(): set<T> {
+        match this
+        case None => {}
+        case Some(v) => {v}
+      }
+    }
+
+    function Return<T>(v: T): Option<T> {
+      Option.Some(v)
     }
 
-    function Extract(): T
-      requires Success?
+    function Bind<S,T>(o: Option<S>, f: S -> Option<T>): Option<T> {
+      match o 
+      case None => Option<T>.None
+      case Some(v) => f(v)
+    }
+
+    function Join<T>(oo: Option<Option<T>>): Option<T> {
+      match oo
+      case None => Option<T>.None
+      case Some(o) => o
+    }
+
+    function Map<S,T>(f: S -> T): Option<S> -> Option<T>
     {
-      value
+      (o: Option<S>) =>
+        match o 
+        case None => Option<T>.None
+        case Some(v) => Option<T>.Some(f(v))
+    }
+
+    function KleisliComposition<S,T,U>(f: S -> Option<T>, g: T-> Option<U>): S -> Option<U> {
+      s => Bind(f(s), g)
+    }
+
+    function Fold<T,U>(u: U, f: T -> U): Option<T> -> U {
+      (o: Option<T>) =>
+        match o 
+        case None => u
+        case Some(v) => f(v)
+    }
+
+    function Equal<T>(eq: (T, T) -> bool): (Option<T>, Option<T>) -> bool {
+      (o1: Option<T>, o2: Option<T>) =>
+        match (o1, o2)
+        case (Some(v1), Some(v2)) => eq(v1, v2)
+        case (None, None) => true
+        case _ => false
+    }
+    
+    function Compare<T>(cmp: (T, T) -> int): (Option<T>, Option<T>) -> int {
+      (o1: Option<T>, o2: Option<T>) =>
+        match (o1, o2)
+        case (Some(v1), Some(v2)) => cmp(v1, v2)
+        case (None, None) => 0
+        case (None, Some(_)) => -1
+        case (Some(_), None) => 1
     }
   }
 
-  datatype Outcome<E> = Pass | Fail(error: E)
-  {
-    predicate IsFailure() {
-      Fail?
+  module {:options "-functionSyntax:4"} Either {
+    import opened Option
+
+    datatype Either<+S,+T> = Left(left: S) | Right(right: T) {
+      predicate IsLeft<S,T>() {
+        Left?
+      }
+
+      predicate IsRight<S,T>() {
+        Right?
+      }
+    }
+
+    function FindLeft<S,T>(e: Either<S,T>): Option<S> {
+      match e 
+      case Left(v) => Some(v)
+      case Right(v) => None
+    }
+
+    function FindRight<S,T>(e: Either<S,T>): Option<T> {
+      match e 
+      case Left(v) => None
+      case Right(v) => Some(v)
+    }
+
+    function ReturnLeft<S,T>(v: S): Either<S,T> {
+      Either.Left(v)
     }
-    // Note: PropagateFailure returns a Result, not an Outcome.
-    function PropagateFailure<U>(): Result<U, E>
-      requires Fail?
+
+    function ReturnRight<S,T>(v: T): Either<S,T> {
+      Either.Right(v)
+    }
+
+
+
+    function JoinRight<S,T>(ee: Either<S,Either<S,T>>): Either<S,T> {
+      match ee
+      case Left(v) => Either<S,T>.Left(v)
+      case Right(v) => v
+    }
+
+    function JoinLeft<S,T>(ee: Either<Either<S,T>,T>): Either<S,T> {
+      match ee
+      case Left(v) => v
+      case Right(v) => Either<S,T>.Right(v)
+    }
+
+    function MapLeft<S,T,U>(f: S -> T): Either<S,U> -> Either<T,U> {
+      (e: Either<S,U>) =>
+      match e 
+      case Left(v) => Either<T,U>.Left(f(v))
+      case Right(v) => Either<T,U>.Right(v)
+    }
+
+    function MapRight<S,T,U>(f: T -> U): Either<S,T> -> Either<S,U> {
+      (e: Either<S,T>) =>
+      match e 
+      case Left(v) => Either<S,U>.Left(v)
+      case Right(v) => Either<S,U>.Right(f(v))
+    }
+
+    function Map<S1,S2,T1,T2>(f: S1 -> S2, g: T1 -> T2): Either<S1,T1> -> Either<S2,T2> {
+      (e: Either<S1,T1>) =>
+        match e
+        case Left(v) => Either<S2,T2>.Left(f(v))
+        case Right(v) => Either<S2,T2>.Right(g(v))
+    }
+
+    function Fold<S,T,U>(f: S -> U, g: T -> U): Either<S,T> -> U {
+      (e: Either<S,T>) =>
+        match e
+        case Left(v) => f(v)
+        case Right(v) => g(v)
+    }
+
+    function Equal<S,T>(eql: (S, S) -> bool, eqr: (T, T) -> bool): (Either<S,T>, Either<S,T>) -> bool {
+      (e1: Either<S,T>, e2: Either<S,T>) =>
+        match (e1, e2)
+        case (Left(v1), Left(v2)) => eql(v1, v2)
+        case (Right(v1), Right(v2)) => eqr(v1, v2)
+        case _ => false
+    }
+
+    function Compare<S,T>(cmpl: (S, S) -> int, cmpr: (T, T) -> int): (Either<S,T>, Either<S,T>) -> int {
+      (e1: Either<S,T>, e2: Either<S,T>) =>
+        match (e1, e2)
+        case (Left(v1), Left(v2)) => cmpl(v1, v2)
+        case (Right(v1), Right(v2)) => cmpr(v1, v2)
+        case (Left(_), Right(_)) => -1
+        case (Right(_), Left(_)) => 1
+    }
+  }
+
+  module {:options "-functionSyntax:4"} Reader {
+    datatype Reader<-X,+T> = Reader(f: X -> T)
+
+    function Return<X,T>(t: T): Reader<X,T> {
+      Reader(x => t)
+    }
+
+    function Bind<X,S,T>(r: Reader<X,S>, f: S -> Reader<X,T>): Reader<X,T> {
+      Reader(x => (f((r.f)(x)).f)(x))
+    }
+
+    function Join<X,T>(rr: Reader<X,Reader<X,T>>): Reader<X,T> {
+      Reader(x => (rr.f(x)).f(x))
+    }
+
+    function Map<X,S,T>(f: S -> T): Reader<X,S> -> Reader<X,T> {
+      (r: Reader<X,S>) => 
+        Reader(x => f((r.f)(x)))
+    }
+
+    function MapContra<X,Y,T>(f: X -> Y): Reader<Y,T> -> Reader<X,T> {
+      (r: Reader<Y,T>) =>
+        Reader(x => r.f(f(x)))
+    }
+
+    function KleisliComposition<X,S,T,U>(f: S -> Reader<X,T>, g: T -> Reader<X,U>): S -> Reader<X,U> {
+      s => Bind(f(s), g)
+    } 
+
+    ghost function Equal<X(!new),T>(eq: (T, T) -> bool): (Reader<X,T>, Reader<X,T>) -> bool 
     {
-      Failure(this.error)
+      (r1: Reader<X,T>, r2: Reader<X,T>) => 
+        forall x: X :: eq(r1.f(x), r2.f(x))
+    }
+  }
+
+  module {:options "-functionSyntax:4"} Outcome {
+    import Result 
+
+    datatype Outcome<E> = Pass | Fail(error: E) {
+        predicate IsFailure() {
+          Fail?
+        }
+        // Note: PropagateFailure returns a Result, not an Outcome.
+        function PropagateFailure<U>(): Result.Result<U, E>
+          requires Fail?
+        {
+          Result.Failure(this.error)
+        }
+        // Note: no Extract method
+      }
+
+      // A helper function to ensure a requirement is true at runtime
+      // :- Need(5 == |mySet|, "The set MUST have 5 elements.")
+      function Need<E>(condition: bool, error: E): (result: Outcome<E>)
+      {
+        if condition then Pass else Fail(error)
     }
-    // Note: no Extract method
   }
 
-  // A helper function to ensure a requirement is true at runtime
-  // :- Need(5 == |mySet|, "The set MUST have 5 elements.")
-  function Need<E>(condition: bool, error: E): (result: Outcome<E>)
-  {
-    if condition then Pass else Fail(error)
+  function ToResult<T>(o: Option.Option<T>): Result.Result<T,string> {
+    match o
+    case Some(v) => Result.Success(v)
+    case None => Result.Failure("Option is None")
   }
-}
+}  
\ No newline at end of file
diff --git a/src/Wrappers.dll b/src/Wrappers.dll
new file mode 100644
index 00000000..d6f54e80
Binary files /dev/null and b/src/Wrappers.dll differ