proposition: Theorem Free_Fix_iso : forall `{Functor f} a, Fix (Either a ∘ f) ≅ Free f a.
proof: Proof. unfold Fix, Free, comp. intros. apply iso_ext; intros. rewrite exp_exp_sym_dep_iso. unfold isomorphic. exists (fun (k : (forall x0 : Type, (x0 -> x) -> a + f x0 -> x) -> x) (g : forall x0 : Type, (x0 -> x) -> f x0 -> x) (h : a -> x) => k (fun x j p => match p with | inl a => h a | inr f => g x j f end)). exists (fun (k : (forall x0 : Type, (x0 -> x) -> f x0 -> x) -> (a -> x) -> x) (g : forall x0 : Type, (x0 -> x) -> a + f x0 -> x) => k (fun x j f => g x j (inr f)) (fun a => g False (False_rect _) (inl a))). extensionalize. f_equal. extensionality x0. extensionality j. extensionality p. destruct p; trivial. Abort. Require Import Hask.Control.Monad.Free. Theorem Free_Fix_iso : forall `{Functor f} a, Fix (Either a ∘ f) ≅ Free f a. Proof. intros. exists (fun (k : forall r : Type, (forall x, (x -> r) -> a + f x -> r) -> r) => k (Free f a) (fun _ h p => match p return Free f a with | inl x => Pure x | inr x => Join h x end)). Abort. Axiom Lens_parametricity : forall `{Functor f} `{Functor g} (eta : forall a, f a -> g a) `(c : a -> f b) `(lens : Lens s t a b), eta t ∘ lens f H c = lens g H0 (eta b ∘ c). Definition IStore a b t := (a * (b -> t))%type. #[export] Instance IStore_Functor {a b} : Functor (IStore a b) := { fmap := fun _ _ f x => match x with (a, k) => (a, fun b => f (k b)) end }. #[export] Program Instance IStore_FunctorLaws {a b} : FunctorLaws (IStore a b). Obligation 1. extensionality p. destruct p. 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