coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] FMaps and proof irrelevance

From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] FMaps and proof irrelevance
Date: Fri, 18 Sep 2009 13:35:10 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

A complement to my previous message. Proof irrelevance as a consequence of the axioms of of excluded middle and some form of axiom of choice is already given in Coquand's 1990 paper "metamathematical investigations of a calculus of constructions". Available from the page:

http://www.cse.chalmers.se/~coquand/type.html
http://www.cse.chalmers.se/~coquand/meta.pdf

Yves

[Coq-Club] FMaps and proof irrelevance, Filou Vincent
- Re: [Coq-Club] FMaps and proof irrelevance, Yves Bertot
  - Re: [Coq-Club] FMaps and proof irrelevance, Yves Bertot