3 ms·
Wow, I am delighted to see this! However I cannot find a precise reference for the chosen type theory. E.g., is univalence a theorem in their type theory? I p
by ocfnash 7y ago
Wow, I am delighted to see this!
However I cannot find a precise reference for the chosen type theory.
E.g., is univalence a theorem in their type theory? I presume it is given that they say their language has "syntax similar to cubical type theory" but I could not say for sure.
What I'm looking for is a reference containing the actual typing rules, like this one for Coq:
https://coq.inria.fr/refman/language/cic.html#typing-rules https://coq.inria.fr/refman/language/cic.html#typing-rules
rather than the syntax of the language used for building these terms.
- cjfd 7y agoYes, I came here to say precisely that. It looks like it has about the same things available as coq as far as syntax is concerned, so what are the differences?
- ocfnash 7y agoWell they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC. For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features https://arend-lang.github.io/about/arend-features (not true in CIC). It would just be nice to see a list of the rules. Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.
- askthereception 7y agoPerhaps have a look at the paper "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom" by Cohen et al. [1] which gives the typing rules in the early sections. [1] http://drops.dagstuhl.de/opus/volltexte/2018/8475/ http://drops.dagstuhl.de/opus/volltexte/2018/8475/