proposition: Lemma IStore_Yoneda_iso : forall `{FunctorLaws f} a b, (IStore a b ⟹ f) ≅ a -> f b.
proof: Proof. intros. unfold IStore. pose proof (@Yoneda_iso f H H0 b). unfold Yoneda in H1. rewrite <- H1. assert ((a -> forall r : Type, (b -> r) -> f r) ≅ (forall r : Type, a -> (b -> r) -> f r)). exists (fun k r a g => k a r g). exists (fun k a r g => k r a g). extensionalize. rewrite H2. apply iso_ext; intros. rewrite exp_mul_iso. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude Hask.Control.Applicative Hask.Control.Monad Hask.Control.Monad.Cont Hask.Control.Monad.State Hask.Data.Functor.Contravariant Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Data.Functor.Yoneda Hask.Control.Lens Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Init.Datatypes Coq.Relations.Relation_Definitions FunctionalExtensionality Hask.Data.Functor.Fix Hask.Control.Monad.Freer