coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] product category in Coq.

From: Theodoros Tsokos <T.Tsokos AT cs.bham.ac.uk>
To: robdockins AT fastmail.fm
Cc: Coq Mailing List <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] product category in Coq.
Date: Thu, 06 Dec 2007 13:10:30 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: SoCS - University of Birmingham

Robert Dockins wrote:

I think you want

Define F := PROD C C : Category.

Thank you very much. Indeed, that's what I wanted. Quite trivial mistake as I assumed.

*Apologies* to the list for multiple emails too - it was my mistake in cooperation with my email client.

Theo.

[Coq-Club] product category in Coq., Theodoros Tsokos
- <Possible follow-ups>
- [Coq-Club] product category in Coq., Theodoros Tsokos
  - Re: [Coq-Club] product category in Coq., Robert Dockins
    - Re: [Coq-Club] product category in Coq., Theodoros Tsokos