I just noticed that Voevodsky's Homotopy Type Theory book deals on p 7 with issues I've posted here: http://hottheory.files.wordpress.com/2013/03/hott-online.pdf
One difficulty often encountered by the classical mathematician when faced with learning about type theory is that [it is not even] familiar to most working mathematicians, even those who might be interested in foundations of mathematics. One objective of the present work is to develop an informal style of doing mathematics in univalent foundations that is at once rigorous and precise, but is also closer to the language and style of presentation of everyday mathematics. In present-day mathematics, [...] for the most part, one does not even need to be aware of this possibility [of ZFC formalization], since it largely coincides with the condition that a proof be "fully rigorous" (in the sense that all mathematicians have come to understand intuitively through education and experience). One can imagine a not-too-distant future when it will be possible for mathematicians to verify the correctness of their own papers by working within the system of univalent foundations, formalized in a proof assistant, and that doing so will become as natural as typesetting their own papers in TEX. In principle, this could be equally true for any other foundational system, but we believe it to be more practically attainable using univalent foundations, as witnessed by the present work and its formal counterpart. This sounds great! And the comment on `"fully rigorous" education and experience' is very interesting. My feeling right now is that if Voevodsky's univalent ideas are helpful, we port them to HOL, where I would think it would work better. Isn't straight HOL much easier to write formal proofs in that straight Coq, where you have to master the intricacies of dependent types? -- Best, Bill ------------------------------------------------------------------------------ This SF.net email is sponsored by Windows: Build for Windows Store. http://p.sf.net/sfu/windows-dev2dev _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
