The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I started to re-write the standard library using hProp instead of Prop. Here 
is the re-written Logic.v

Attachment: hLogic_r.v
Description: Binary data

To compile it one needs a Type_in_Type patch as well as my distribution of 
the univalent foundations up to Prop_r.v 


I should say that it was not a very hard work - the whole file took about 3 
days. 

There are many examples there of how one proves things in hProp instead of 
Prop. May be someone can start thinking  about writing a tactic  htauto ...

Vladimir