IAS Univalent Foundations

For those of you without access to the link: http://cacm.acm.org/magazines/2014/2/171675-a-new-type-

It seems that QA9 is the popular choice. Thank you! On Tue, Oct 8, 2013 at 12:00 PM, Michael Nahas

On Oct 3, 2013, at 10:56 PM, Michael Shulman <shu...@sandiego.edu> wrote: > I would think

Dear All, Have a look at: http://www.ams.org/home/page and check out the link under Publishing

http://www.newscientist.com/article/dn23749-mathematicians-think-like-machines-for-perfect-proofs.

http://www.wired.com/wiredenterprise/2013/06/cades-witty-headline-here/

!

Dear Friends, It's finally done! Homotopy Type Theory: Univalent Foundations of Mathematics The

[Apologies for multiple postings] Dear friends and colleagues, This is a reminder that the conference

We just put the following on the arxiv. Those of you reading/writing the book, will notice quite some

I support the idea, but I can't promise to have a lot of time to help, especially in August. On

When reading the post, I was wondering whether such an idea could be used in the future to translate

Dear UFers, Just a brief report from our recent successful incursion into the world of straight logic

This position at our department may be of interest to some readers of this list. (For instance the

If nobody objects or improve, I am going to use the following bibtex file for the final version of an

John Reynolds, one of the visionaries of type theory, sadly passed away yesterday. In his honor,

A citation for the Hott book? "First they ignore you, then they laugh at you, then they fight

Just to let you know, I have formalized the proof that "Universe n is not an n-type" (on

Hi, I've investigated this and the problem is that Coq does not know about the polymorphic

Re: "We did not set out to write a book." Hmm, I thought that was the original plan that

It is likely to be due to one of Matthieu's latest commits from April 17th. https://github.com/

here is a higher res image: I also posted some photos of the Coq WG on the wiki.

Marc Bezem and Thierry Coquand have added a note on Presheaf models of simplicial sets to the wiki,

Hi, Is point 2 of the list referring to an inductively-generated, constructive, dependently-typed

On 2013/4/14 Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk> wrote: > On 14/04/2013 18:

Thanks to all participants in the special for a uniquely memorable and educational experience.

I just noticed that there is another interesting application of Higher Inductive-Inductive

On 11/4/13 2:47 PM, bertot wrote: > Definition S1_rect (P : S1 -> Type) (b : P base) (l : loop

Dear collegues, I very much enjoyed watching the story of silicon valley: http://video.pbs.org/video/

I hope so - this one is really pixelated. T. On 12/04/2013 12:09, "Dan Licata" <drl@cs.