The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Robin

On 7 Jul 2008, at 17:36, Robin Green wrote:

> 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)?

There's some stuff in chapter 7 of my thesis which develops
small categories of renamings, substitutions, etc. I gave a
not very sophisticated treatment of "concrete" categories
with a faithful functor into Type. It seemed like a good
idea at the time.

I don't know if this is what you had in mind, but it certainly
involved more than one category.

Cheers

Conor