News for hackers. Stuff that matters.

A comment on Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains. Parent comment

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.

[1] http://drops.dagstuhl.de/opus/volltexte/2018/8475/

[ Parent | on HN ]

There are no comments on this comment yet.