{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1703","labels_url":"https://api.github.com/repos/agda/agda/issues/1703/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1703/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1703/events","html_url":"https://github.com/agda/agda/issues/1703","id":113385256,"number":1703,"title":"Add support for \"cubical type theory\" under flag --cubical","user":{"login":"Saizan","id":130892,"avatar_url":"https://avatars.githubusercontent.com/u/130892?v=3","gravatar_id":"","url":"https://api.github.com/users/Saizan","html_url":"https://github.com/Saizan","followers_url":"https://api.github.com/users/Saizan/followers","following_url":"https://api.github.com/users/Saizan/following{/other_user}","gists_url":"https://api.github.com/users/Saizan/gists{/gist_id}","starred_url":"https://api.github.com/users/Saizan/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Saizan/subscriptions","organizations_url":"https://api.github.com/users/Saizan/orgs","repos_url":"https://api.github.com/users/Saizan/repos","events_url":"https://api.github.com/users/Saizan/events{/privacy}","received_events_url":"https://api.github.com/users/Saizan/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-10-26T15:49:22Z","updated_at":"2015-10-28T11:10:04Z","closed_at":null,"body":"Considering there has been an actual type system with conversion rules for a while:\r\n  http://www.cse.chalmers.se/~coquand/face.pdf\r\n\r\nIt would be interesting to have a proper proof assistant which implements that theory, to gain support for functional extensionality, bisimilarity-as-equality, quotients, univalence.\r\n\r\n##### Partial Elements\r\nThe main addition required would be \"partial elements\", or \"systems\" as previously called, since the interesting primitives rely on those. This implies changes to both the source and internal syntax.\r\n\r\n##### Overloading Lambdas\r\nWe might want to reuse lambdas and whitespace for path abstraction and application, instead of ```<i> t``` and ```p @ i```, unless that complicates type inference too much.\r\n\r\n##### Pattern Matching and Inductive Families\r\nConcerning pattern matching the flag --cubical should imply --without-K.\r\nThat is still not enough to guarantee definitional canonicity at e.g. Bool though, for which we could initially disable inductive families. (The end-goal however would be to have inductive families as parametrized types with embedded equality proofs behind the scenes, while still being able to use dependent pattern matching as we can now. It might need some amount of research and user interface design.)\r\n\r\n##### Higher Inductive Types\r\nFor higher inductive types we could initially only provide support for quotients and truncations as primitives, considering the theory is not completely settled on them. In \"cubicaltt\" this means that pattern matching on one of those types also needs to pattern match on the path constructors: we should be able to handle this by extending the grammar for copatterns. \r\n\r\n##### Impact\r\nMy impression is that implementing this minimal support for cubical will not have too big of an impact on the codebase, since in the end the Path type is a mix of a dependent function and a singleton type and our conversion checking is already type directed. We might need more type information during reduction though.\r\n\r\nI will come up with a more detailed plan in the future, but I opened this issue so that we can collect comments.\r\n\r\n\r\n\r\n\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/151804825","html_url":"https://github.com/agda/agda/issues/1703#issuecomment-151804825","issue_url":"https://api.github.com/repos/agda/agda/issues/1703","id":151804825,"user":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"created_at":"2015-10-28T11:10:04Z","updated_at":"2015-10-28T11:10:04Z","body":"In any case, we should not use the ugly shortcut `t(i 0)` for `t(i = 0)`."}}