proposition: Theorem coyo_lift_naturality `{FunctorLaws f} : forall a b (g : a -> b), fmap g \o liftCoyoneda (f:=f) = liftCoyoneda \o fmap g.
proof: Proof. intros a b g. unfold liftCoyoneda. extensionality x. simpl. replace (g \o id) with g; auto. rewrite coyo_parametricity. reflexivity. Qed.
imports: Hask.Prelude Hask.Ltac Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Control.Monad FunctionalExtensionality FunctionalExtensionality