[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Vladimir Voevodsky]

On Jan 7, 2014, at 5:01 AM, Frédéric Blanqui <frederic.blanqui at inria.fr> wrote:

> This of course may raise
> problems for making sure that such definitions are consistent, but it is
> another (interesting) problem.
> 

Do not forget that proof assistants are there precisely because we need proofs which we know are correct. So a proof assistant which certifies incorrect proofs is useless except for experimental purposes. 

For those of us who want to *use* proof assistants not to develop proof assistants the consistency issue is crucial. 

Vladimir.