I wrote:
> For example, we know just from the fact that
> concat : Forall a. a -> a, that
>
> \xs.map A B f (concat A xs) = \xs. concat B (map A B f xs)
>
> where map : forall a. forall b. A -> B -> ([A] -> [B]). Here the
> endofunctor in question is the list functor, [].
Oops, I really screwed this up.
First, I wrote the wrong type for concat:
concat : forall a. [[a]] -> [a]
Second, that equation is not even well-typed. I meant:
\xs. map A B f (concat A xs) = \xs. concat B (map [A] [B] (map A B f) xs)
BTW, there is no significance to the fact that I kept switching between
"Forall" and "forall"...
Maybe I should just leave the category theory to Hans...!
--FC
