News for hackers. Stuff that matters.

A comment on Relation Between Type Theory, Category Theory and Logic. Parent comment

Re:Relation Between Type Theory, Category Theory and Logic by YorkshireSeason on Saturday July 11, 2015 @05:49AM (#9869203)
What is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.
[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by gallabytes on Saturday July 11, 2015 @01:23PM (#9870658)
A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.
[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by Kutta on Saturday July 11, 2015 @01:39PM (#9870752)
Could you give pointers wrt cubical model being a dead end? As yet I've heard nothing about this.
[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by doall on Sunday July 12, 2015 @04:52PM (#9874921)
See this https://groups.google.com/d/msg/homotopytypetheory/oXQe5u_Mm...
[ Parent | on HN ]