Theory readerMonad

⊢ ∀M f s. BIND M f s = f (M s) s

⊢ ∀f M1. FMAP f M1 = f ∘ M1

⊢ ∀MM s. JOIN MM s = MM s s

⊢ ∀f1 f2 a. MCOMPOSE f1 f2 a = BIND (f1 a) f2

⊢ ∀x s. UNIT x s = x

⊢ BIND M f = JOIN (FMAP f M)

⊢ BIND (UNIT x) f = f x

⊢ BIND m UNIT = m

⊢ FMAP f M = BIND M (UNIT ∘ f)

⊢ FMAP (λx. x) M = M ∧ FMAP I M = M

⊢ FMAP (f ∘ g) = FMAP f ∘ FMAP g

⊢ JOIN M = BIND M I

⊢ MCOMPOSE f (MCOMPOSE g h) = MCOMPOSE (MCOMPOSE f g) h

⊢ MCOMPOSE UNIT g = g

⊢ MCOMPOSE f UNIT = f