proposition: Theorem mul_exp_iso : forall a b c, a -> (b * c) ≅ (a -> b) * (a -> c).
proof: Proof. intros; exists (fun k => ((fun a => fst (k a)), (fun a => snd (k a)))). exists (fun p a => match p with (f, g) => (f a, g a) end). extensionalize. 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