Discussion of Homotopy Type Theory and Univalent Foundations
help / Atom feed
From: Valery Isaev <valery.isaev@gmail.com>
To: Bas Spitters <b.a.w.spitters@gmail.com>
Cc: Jon Sterling <jon@jonmsterling.com>,
"'Martin Escardo' via Homotopy Type Theory"
Subject: Re: [HoTT] New theorem prover Arend is released
Date: Thu, 8 Aug 2019 17:44:56 +0300
Message-ID: <CAA520ft6xBR1fJz4N0c5NvB+pWD+14RPCu5g32cxv+YdbEmd0g@mail.gmail.com> (raw)

[-- Attachment #1: Type: text/plain, Size: 6461 bytes --]

Yes, Arend implements the theory described in this document. Semantically,
the additional constructions of this theory correspond to the assumption
that the model has a fibrant object I such that maps <id,left> : X -> X
\times I have the left lifting property with respect to fibrations, and the
path object functor is given by (-)^I. So, the usual interpretation in
model categories (and other similar models) of HoTT extends to an
interpretation of this theory if the model category is a Cartesian model
category.

Regards,
Valery Isaev

чт, 8 авг. 2019 г. в 15:29, Bas Spitters <b.a.w.spitters@gmail.com>:

> I imagine it could be related to earlier discussions, but Valery will
> correct me:
> https://valis.github.io/doc.pdf
>
> On Thu, Aug 8, 2019 at 2:20 PM Jon Sterling <jon@jonmsterling.com> wrote:
> >
> > 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
> > >
> > > 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.
> > >
> > > <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.
> > >
> > >  * 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.
> > >
> > >  --
> > >  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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> > >  To view this discussion on the web visit
> > >
> <
> >.
> >
> > --
> > 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
> > To view this discussion on the web visit
> .
>
> --
> 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
> To view this discussion on the web visit
> .
>

--
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520ft6xBR1fJz4N0c5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 9642 bytes --]


next prev parent reply index

Thread overview: 20+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-08-06 22:16 Валерий Исаев
2019-08-07 15:01  Andrej Bauer
2019-08-07 22:13  Nicolai Kraus
2019-08-08  9:55    Valery Isaev
2019-08-10  9:47      Michael Shulman
2019-08-10 12:30        Valery Isaev
2019-08-10 12:37        Valery Isaev
2019-08-08 12:20  Jon Sterling
2019-08-08 12:29    Bas Spitters
2019-08-08 14:44      Valery Isaev [this message]
2019-08-08 15:11        Jon Sterling
2019-08-08 15:22          Valery Isaev
2019-08-10  9:42            Michael Shulman
2019-08-10 12:24              Valery Isaev
2019-08-10 23:37                Michael Shulman
2019-08-11 10:46                  Valery Isaev
2019-08-11 12:39                    Michael Shulman
2019-08-11 16:55                      Michael Shulman
2019-08-12 14:44                        Daniel R. Grayson
2019-08-12 17:32                          Michael Shulman


Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
--to=valery.isaev@gmail.com \
--cc=b.a.w.spitters@gmail.com \
--cc=jon@jonmsterling.com \

https://kernel.org/pub/software/scm/git/docs/git-send-email.html


Discussion of Homotopy Type Theory and Univalent Foundations
AGPL code for this site: git clone https://public-inbox.org/ public-inbox`