Stupid of me: > Isn't the code for mapBox :: forall a. (a -> a) -> Box -> Box > encoding the proof: > > Assume forall a. a -> a > Assume exists a.a > unpack the existential, x :: a = T for some T > apply f to x, we get (f x) :: a > pack into existential, B (f x) :: exists a.a > Discharge first assumption > Discharge second assumption > > The error must be in step 3. Sorry if this is obvious, it's not to me right > now.
The proof outlined is that of (forall a. a -> a) -> Box -> Box, my apologies. We have to prove a universally quantified formula and that requires forall-introduction. If someone has the proof in the tip of their fingers, I'm grateful if you could let me know. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
