<story><title>Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains</title><url>https://arend-lang.github.io/</url></story><parent_chain></parent_chain><comment><author>jey</author><text>Wow, JetBrains has a whole HoTT and Dependent Types Research Group: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;research.jetbrains.org&amp;#x2F;groups&amp;#x2F;group-for-dependent-types-and-hott&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;research.jetbrains.org&amp;#x2F;groups&amp;#x2F;group-for-dependent-ty...&lt;/a&gt;</text></comment>
<story><title>Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains</title><url>https://arend-lang.github.io/</url></story><parent_chain></parent_chain><comment><author>ocfnash</author><text>Wow, I am delighted to see this!&lt;p&gt;However I cannot find a precise reference for the chosen type theory.&lt;p&gt;E.g., is univalence a theorem in their type theory? I presume it is given that they say their language has &amp;quot;syntax similar to cubical type theory&amp;quot; but I could not say for sure.&lt;p&gt;What I&amp;#x27;m looking for is a reference containing the actual typing rules, like this one for Coq:
&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;coq.inria.fr&amp;#x2F;refman&amp;#x2F;language&amp;#x2F;cic.html#typing-rules&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;coq.inria.fr&amp;#x2F;refman&amp;#x2F;language&amp;#x2F;cic.html#typing-rules&lt;/a&gt;&lt;p&gt;rather than the syntax of the language used for building these terms.</text></comment>