search

type-theory / type-theory-study-group

Resources for the online Type Theory Study Group
161 stars 18 forks source link

regarding cubical type theory & canonicity #2

Closed jonsterling closed 8 years ago

jonsterling commented 9 years ago

I think that cubical type theory is sufficiently technical and not-yet-figured-out that it might be a bit too advanced a topic. cubical type theories as published today do not have the canonicity property, though they are a lot closer than "Book HoTT".

so far the only higher dimensional type theory which has had canonicity is Bob Harper & Dan Licata's Two Dimensional Type Theory; might be worthwhile to take a look at that in the study group, since it is a "straightforward" generalization of the Nuprl semantics with one further dimension.

(I also wouldn't call cubical type theory as "special case of HoTT w/ canonicity", since HoTT doesn't have canonicity (yet); I'd say it is a proposed higher-dimensional type theory which may come to have the canonicity property.)

jozefg commented 9 years ago

I'm also unaware of any resources on cubical type theory that actually make sense to people not doing research on cubical type theory. Though I would love to be surprised :)

jonsterling commented 9 years ago

Yeah... Even people who are working on cubical type theory have told me they don't understand many of the papers that are being published about it.

markfarrell commented 9 years ago

I don't really understand 'cubical type theory' either, but was, broadly speaking, impressed with Dan Licata's talk A Cubical Infinite Dimensional Type Theory and the project Cubical Type Theory here on GitHub. I've heard about Bob Harper and Dan Licata's Two Dimensional Type Theory, but haven't really looked at it or studied it any amount of detail yet. I'd imagine, as you suggested, that might be a better place to start (when we get there). Though I would like to hear what other people think of Dan's talk and/or the Cubical Type Theory project here on GitHub - partly because I don't really understand them and hope that other people would be interested and/or can help shed some light on them! :persevere: