The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Mar 19, 2014, at 12:49 PM, Victor Porton <porton AT narod.ru> wrote:

19.03.2014, 18:44, "Vladimir Voevodsky" <vladimir AT ias.edu>:

On Mar 18, 2014, at 2:18 PM, Todd Wilson <twilson AT csufresno.edu> wrote:

Nor, it seems, could I use a theory that included Univalence, again unless it were easy to
see that I've avoided it in my construction and proof.

None of the Foundations library and very little of the RezkCompletion library uses Univalence Axiom.

 

On the other hand, if you do not care about the constructivity of your development, the use of the Univalence Axiom is perfectly acceptable since it has been shown to be consistent with the rest of Coq and it can simplify many proofs considerably.

 

V.

 

 

Does this mean that Univalence Axiom can be used without HoTT?

 

Of course. It is just an axiom. 

V.