It's actually not very interesting formulation of category theory. You can't express a category of categories, with isomorphic categories considered equal in this way. Partially, this can be worked around if we state that everything important preserves equivalence (i.e. if A ~ A` and B ~ B` A x B ~ A` x B`). Though, if you want to express this in full generality, you will need Homotopy Type Theory.<p>But, all in all, even formulating all this and proving theorems was a good exercise. Good job!
I believe this is what John Wiegley talked about in this Haskell Cast[1] which, as I understand it, should allow translating Haskell into Coq.<p>I’m just beginning to understand all of this category stuff but, as far as I can see, a Haskell function of type<p><pre><code> f :: a -> b
</code></pre>
should be equivalent to a Coq function of type<p><pre><code> f :: a -> Either SomeException a
</code></pre>
to account for the Hask category’s “bottom” value.<p>[1] <a href="http://www.haskellcast.com/episode/013-john-wiegley-on-categories-and-compilers" rel="nofollow">http://www.haskellcast.com/episode/013-john-wiegley-on-categ...</a> (skip to “compiling to categories”)
Is there a good lecture series on Coq? Or maybe introductory project?<p>I've seen a video intro [0] and poked a little bit around the reference manual [1], but I'm not sure what's "between" basic understanding of the commands and being able to extract a complex verified program.<p>It all seems to be either the theory (which I mostly grok) or completed projects, not a lot about the engineering details.<p>...Or does that just not exist?<p>[0] <a href="https://www.youtube.com/watch?v=ngM2N98ppQE" rel="nofollow">https://www.youtube.com/watch?v=ngM2N98ppQE</a><p>[1] <a href="https://coq.inria.fr/refman/" rel="nofollow">https://coq.inria.fr/refman/</a>
A question for those of you here who are into functional programming:<p>Is category theory worth studying if I (coming from c++ background) am looking to get into functional languages like Haskell? How common is it actually among Haskell or Lisp programmers to know and utilize concepts from category theory in their programming?