Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Yet another dependent type question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Yet another dependent type question


chronological Thread 
  • From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • To: Michael Shulman <viritrilbia AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Yet another dependent type question
  • Date: Mon, 29 Mar 2010 11:59:12 +0200

Hi,

> Anyway, as long as I'm commenting on this, let me say that I hope that
> if Coq is eventually extended in some way which makes axiom K or its
> equivalents provable, that it will at least be possible to turn off
> such an extension.  Since my interest is largely in models such as
> groupoids and homotopy theory, I would not want uniqueness of
> reflexive identity proofs to be built into the system unavoidably.

A few people mentioned these models to me. 

Do you then mean that you are interested in using Coq with axioms
incompatible with the uniqueness of reflexive identity proofs?

Hugo Herbelin



Archive powered by MhonArc 2.6.16.

Top of Page