1      let Reader = ./Type
 2  
 3  in    λ(r : Type)
 4      →   { withReader =
 5                λ(a : Type)
 6              → λ(rPrime : Type)
 7              → λ(f : rPrime → r)
 8              → λ(reader : Reader r a)
 9              → ./withReader r a rPrime f reader
10          }
11        ∧ ./monad r