coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Categorical programming with more than one category?

From: Vladimir Komendantsky <Vladimir.Komendantsky AT sophia.inria.fr>
To: coq-club AT pauillac.inria.fr
Cc: Robin Green <greenrd AT greenrd.org>
Subject: Re: [Coq-Club] Categorical programming with more than one category?
Date: Mon, 7 Jul 2008 20:04:56 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Robin,

Are you familiar with the library of constructive category theory
(definitions) contributed by Amokrane Saibi? It should be somewhere in
contributions to Coq on coq.inria.fr. However I don't know a single
implementation of this library with the properties you described.

Vladimir

On Mon, Jul 07, 2008 at 05:36:55PM +0100, 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?

[Coq-Club] Categorical programming with more than one category?, Robin Green
- Re: [Coq-Club] Categorical programming with more than one category?, Arnaud Spiwack
- Re: [Coq-Club] Categorical programming with more than one category?, Vladimir Komendantsky
- Re: [Coq-Club] Categorical programming with more than one category?, Conor McBride
- Re: [Coq-Club] Categorical programming with more than one category?, Noam Zeilberger