This group may be of interest:
https://groups.google.com/forum/#!forum/hott-amateurs
On Tue, Jun 25, 2013 at 4:33 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> 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
>
------------------------------------------------------------------------------
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
