{"action":"closed","issue":{"url":"https://api.github.com/repos/mortberg/cubicaltt/issues/26","labels_url":"https://api.github.com/repos/mortberg/cubicaltt/issues/26/labels{/name}","comments_url":"https://api.github.com/repos/mortberg/cubicaltt/issues/26/comments","events_url":"https://api.github.com/repos/mortberg/cubicaltt/issues/26/events","html_url":"https://github.com/mortberg/cubicaltt/issues/26","id":122820207,"number":26,"title":"univalence normalization","user":{"login":"stelleg","id":150376,"avatar_url":"https://avatars.githubusercontent.com/u/150376?v=3","gravatar_id":"","url":"https://api.github.com/users/stelleg","html_url":"https://github.com/stelleg","followers_url":"https://api.github.com/users/stelleg/followers","following_url":"https://api.github.com/users/stelleg/following{/other_user}","gists_url":"https://api.github.com/users/stelleg/gists{/gist_id}","starred_url":"https://api.github.com/users/stelleg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/stelleg/subscriptions","organizations_url":"https://api.github.com/users/stelleg/orgs","repos_url":"https://api.github.com/users/stelleg/repos","events_url":"https://api.github.com/users/stelleg/events{/privacy}","received_events_url":"https://api.github.com/users/stelleg/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":15,"created_at":"2015-12-17T20:48:17Z","updated_at":"2016-01-04T20:40:52Z","closed_at":"2016-01-04T20:40:52Z","body":"Hey Guys,\r\n\r\nI've enjoyed playing around with building proofs using funExt, all of which have normalized successfully. When I went to play around with univalence, however, I noticed that none of the proofs of univalence normalize. I let each of the three proofs from `examples/univalence.ctt` run to about 12GB of memory usage, and none of them terminated.\r\n\r\nI haven't carefully read all of the cubicaltt papers, nor carefully reasoned about the proofs of univalence, so I'm wondering if this is a known property of the type theory? It seems worrying from a standard Curry-Howard perspective.\r\n\r\nCheers,\r\nGeorge"}}