The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

Are there any developments in Coq (or any other proof assistant)
which use more than one category-theoretic category in some
interesting way, and yield a useful program?

What I am getting at is: can more than one category be useful in
programming (as opposed to merely doing mathematics)?

I know that, for example, the Set category can be used to define
monads like in Haskell. However, what would categorical programming
look like with more than one category?

If we take a subcategory of the Set category, we can define, for
example, monad type constructors which only obey the monad laws for
certain arguments (those denoted by the objects of the subcategory).
However, I am not aware of any such "partial monads" being used
anywhere.

-- 
Robin