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 gallabytes on Saturday July 11, 2015 @01:21PM (#9870650)
Why would it do that? Univalence is unrelated to the halting problem.

What the univalence axiom says is that you can treat types you have proven isomorphic as equal.

[ Parent | on HN ]

There are no comments on this comment yet.