proposition: Theorem retract_liftF_id `{MonadLaws f} : forall a, retract \o liftF = @id (f a).
proof: Proof. Admitted. Theorem retract_distributes `{Monad f} `{MonadLaws f} : forall a (x y : Free f a), retract (x >> y) = (retract x >> retract y). Admitted. Theorem retract_naturality `{MonadLaws f} : forall a b (g : a -> b), fmap g \o retract (f:=f) = retract \o fmap g. Admitted. Theorem liftF_naturality `{FunctorLaws f} : forall a b (g : a -> b), fmap g \o liftF (f:=f) = liftF \o fmap g. Admitted. Corollary liftF_naturality_x `{FunctorLaws f} : forall a b (g : a -> b) x, fmap g (liftF x) = liftF (fmap g x). Proof. intros. replace ((fmap[Free f] g) (liftF x)) with (((fmap[Free f] g) \o liftF) x). rewrite liftF_naturality. reflexivity. reflexivity. Qed.
imports: Hask.Prelude Hask.Control.Monad FunctionalExtensionality