{"action":"closed","issue":{"url":"https://api.github.com/repos/HoTT/book/issues/764","labels_url":"https://api.github.com/repos/HoTT/book/issues/764/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/book/issues/764/comments","events_url":"https://api.github.com/repos/HoTT/book/issues/764/events","html_url":"https://github.com/HoTT/book/issues/764","id":56706149,"number":764,"title":"Returning to constructivity and (un)truncated logic","user":{"login":"mikeshulman","id":646600,"avatar_url":"https://avatars.githubusercontent.com/u/646600?v=3","gravatar_id":"","url":"https://api.github.com/users/mikeshulman","html_url":"https://github.com/mikeshulman","followers_url":"https://api.github.com/users/mikeshulman/followers","following_url":"https://api.github.com/users/mikeshulman/following{/other_user}","gists_url":"https://api.github.com/users/mikeshulman/gists{/gist_id}","starred_url":"https://api.github.com/users/mikeshulman/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mikeshulman/subscriptions","organizations_url":"https://api.github.com/users/mikeshulman/orgs","repos_url":"https://api.github.com/users/mikeshulman/repos","events_url":"https://api.github.com/users/mikeshulman/events{/privacy}","received_events_url":"https://api.github.com/users/mikeshulman/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":12,"created_at":"2015-02-05T18:03:12Z","updated_at":"2015-02-27T03:22:41Z","closed_at":"2015-02-27T03:22:41Z","body":"The introduction to the book currently says\r\n\r\n> Using all types as propositions yields a \"constructive\" conception of logic... which gives type theory its good computational character.\r\n\r\nMultiple people have complained about this sort of remark (at least Vladimir, Thierry, and Martin, I think), and I would now like to add my voice to them.  At best, I think this remark is misleading because it is vague about what is meant by \"computational character\", and there are meanings of \"computation\" for which truncated logic is perfectly computational.  For instance, computational models such as setoids and (now) cubical sets do implement (-1)-truncation.  Moreover, plenty of people doing \"constructive\" mathematics have used (-1)-truncated logic.\r\n\r\nIn fact, I am no longer even sure what this remark is referring to.  If I remember correctly, @RobertHarper was one of the main voices at IAS advocating the value of untruncated logic in computation, but I don't remember the exact arguments.  Right now, the only possibility I can think of is that when using type theory as a programming language itself, rather than extracting programs from it metatheoretically, having an element of A+B (for instance) allows us to match on it and define functions into arbitrary types, whereas with only an element of A\\/B our codomains would be restricted to propositions.  However, it seems to me right now that this observation actually has little to do with computation specifically --- it is just as true in pure mathematics that an element of A+B is more useful than an element of A\\/B, for the same reason.\r\n\r\nIs there any sense in which untruncated logic is \"more computational\" than truncated logic?  If not, we should modify this sentence.\r\n"}}