Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je...
by askthereception on Wednesday August 07, 2019 @10:11AM
(#20634811)
Perhaps 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.
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je...
by cjfd on Wednesday August 07, 2019 @05:09AM
(#20633051)
Yes, 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?
Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je...
by ocfnash on Wednesday August 07, 2019 @05:23AM
(#20633106)
Well 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 (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.
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
rather than the syntax of the language used for building these terms.