proposition: Lemma IStore_IStore_iso : forall s t a b, (forall `{Functor f}, (IStore a b ⟹ f) -> (IStore s t ⟹ f)) ≅ (IStore s t ⟹ IStore a b).
proof: Proof. intros. rewrite IStore_Yoneda_iso. unfold IStore, Nat. Abort. Lemma Lens_IStore_iso : forall s t a b, Lens s t a b ≅ (IStore s t ⟹ IStore a b). Proof. Abort. Lemma Lens_pair_iso : forall (s t a b : Type), Lens s t a b ≅ (s -> a) * (s -> b -> t). Proof. intros. unfold Lens. rewrite <- mul_exp_iso. pose proof (@IStore_Yoneda_iso (fun t => (a * (b -> t))%type) _ _ s t). simpl in H. rewrite <- H. unfold IStore. assert ((forall f : Type -> Type, Functor f -> (a -> f b) -> s -> f t) ≅ (s -> forall f : Type -> Type, Functor f -> (a -> f b) -> f t)). exists (fun k s f H g => k f H g s). exists (fun k f H g s => k s f H g). extensionalize. rewrite H; clear H. exists (fun (k : Lens s t a b) s => (@k (Const a) _ id s, fun b => @k Identity _ (const b) s)). exists (fun (k : s -> a * (b -> t)) => fun `{Functor f} g s => match k s with (a, h) => fmap[f] h (g a) end). unfold comp, id. simpl. split. extensionality k. extensionality u. destruct (k u). f_equal. extensionality l. extensionality f. extensionality H. extensionality g. extensionality u. Abort. Lemma Lan_alg_iso : forall f g a, Lan f g a -> a ≅ forall x, (f x -> a) -> g x -> a. Proof. intros. unfold Lan. rewrite exp_sigT_iso. 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