Dear Valery,
Arend looks really impressive, especially the IDE features! I look forward to trying it. I like the little screen demos on the website.
We have been curious for some time if someone could begin to explain what type theory Arend implements --- I am not necessarily looking for something super precise, but it would be great to have a high-level gloss that would help experts in the semantics of HoTT understand where Arend's type theory lies. For instance, I can see that Arend uses an interval, but this interval seems to work a bit differently from the interval in some other type theories. Is there any note or document that explains some of the mathematics behind Arend?
Nice work! And I look forward to hearing and reading more.
Best,
Jon
On Tue, Aug 6, 2019, at 6:16 PM, Валерий Исаев wrote:
> Arend is a new theorem prover that have been developed at JetBrains
> <
https://www.jetbrains.com/> for quite some time. We are proud to
> announce that the first version of the language was released! To learn
> more about Arend, visit our site <
https://arend-lang.github.io/>.
>
> Arend is based on a version of homotopy type theory that includes some
> of the cubical features. In particular, it has native higher inductive
> types, including higher inductive-inductive types. It also has other
> features which are necessary for a theorem prover such as universe
> polymorphism and class system. We believe that a theorem prover should
> be convenient to use. That is why we also developed a plugin for
> IntelliJ IDEA <
https://www.jetbrains.com/idea/> that turns it into a
> full-fledged IDE for the Arend language. It implements many standard
> features such as syntax highlighting, completion, auto import, and auto
> formatting. It also has some language-specific features such as
> incremental typechecking and various refactoring tools.
>
> To learn more about Arend, you can check out the documentation
> <
https://arend-lang.github.io/documentation>. You can also learn a lot
> from studying the standard library
> <
https://github.com/JetBrains/arend-lib>. It implements some basic
> algebra, including localization of rings, and homotopy theory,
> including joins, modalities, and localization of types.
>
> Frequently asked questions (that nobody asked):
> * Why do we need another theorem prover? We believe that a theorem
> prover should be convenient to use. This means that it should have an
> IDE comparable to that of mainstream programming languages. That is why
> we implemented IntelliJ Arend
> <
https://arend-lang.github.io/about/intellij-features>. This also means
> that the underlying theory should be powerful and expressive. That is
> why Arend is based on homotopy type theory and has features such as an
> impredicative type of propositions and a powerful class system.
> * Does Arend have tactics? Not yet, but we are working on it.
> * Does Arend have the canonicity property, i.e. does it evaluate
> closed expressions to their canonical forms? No, but it computes more
> terms than ordinary homotopy type theory, which makes it more
> convenient in many aspects.
> If you want to know about language updates, you can follow us on
> twitter <
https://twitter.com/ArendLang>. Questions, suggestions, and
> comments are welcome at google groups
> <
https://groups.google.com/forum/#!forum/arend-lang>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to
HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit
>
https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com <
https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com?utm_medium=email&utm_source=footer>.