proposition: Theorem coyo_lower_naturality `{FunctorLaws f} : forall a b (g : a -> b), fmap g \o lowerCoyoneda (f:=f) = lowerCoyoneda \o fmap g.
proof: Proof. intros a b k. extensionality x. destruct x as [x g h]; simpl. rewrite fmap_comp_x. reflexivity. Qed.
imports: Hask.Prelude Hask.Ltac Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Control.Monad FunctionalExtensionality FunctionalExtensionality