proposition: Corollary Yoneda_parametricity : forall `{Functor f} a b c (k : Yoneda f a) (g : b -> c) (h : a -> b), fmap g (k _ h) = k _ (g \o h).
proof: Proof. intros. pose proof (@Ran_parametricity a b c Identity _ f _). simpl in H0. unfold id in H0. Admitted. #[export] Program Instance Yoneda_FunctorLaws {f : Type -> Type} : FunctorLaws (Yoneda f). #[export] Program Instance Yoneda_ApplicativeLaws `{ApplicativeLaws f} : ApplicativeLaws (Yoneda f). Obligation 1. extensionality x. extensionality r. extensionality k0. rewrite ap_fmap, <- fmap_comp, fmap_id. unfold comp, id. apply Yoneda_parametricity. Qed.
imports: Hask.Prelude Hask.Ltac Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Control.Monad FunctionalExtensionality