Re: [HoTT] New theorem prover Arend is released

[Valery Isaev <valery.isaev@gmail.com>]

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

чт, 8 авг. 2019 г. в 18:11, Jon Sterling <jon@jonmsterling.com>:

> Hi Valery (and Bas),
>
> Thanks very much for the reference! Can you say a bit more about the
> interpretation in model categories? I have the following specific questions:
>
> - By "Cartesian model category" do you refer to the pushout-product axiom?
> I apologize for my ignorance, model categories are not my area of expertise.
>
>
Yes.


> - In most models of HoTT that I'm familiar with, including simplicial sets
> and several versions of cubical sets, the interval is not fibrant. What
> interpretation do have in mind for I? (btw, sorry if this has been
> discussed before!).
>

You can take any contractible fibrant object such that the map 1+1 -> I is
a cofibration. Such an object always exists (just factor the map 1+1 -> 1
as a cofibration followed by trivial fibration), so the only additional
assumption is that the exponential (-)^I exists and the pushout-product
axiom holds.


>
> Thanks,
> Jon
>
>
> On Thu, Aug 8, 2019, at 10:45 AM, Valery Isaev wrote:
> > 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://groups.google.com/forum/#!topic/homotopytypetheory/N8jw_5h2Qjs
> > > 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
> > >  > > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com
> <mailto:HomotopyTypeTheory%2Bunsubscribe@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
> >.
> > >  >
> > >  > --
> > >  > 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 <mailto:
> HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
> > >  > To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/06e24c98-7409-4e75-88ee-a6e1bb891e1e%40www.fastmail.com
> .
> > >
> > >  --
> > >  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 <mailto:
> HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>.
> > >  To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSLoX8gKy54NQM6SNoi43wVA0A1Ad59qKs6prULkh6zBw%40mail.gmail.com
> .
> >
> >  --
> >  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
> <
> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520ft6xBR1fJz4N0c5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.com?utm_medium=email&utm_source=footer
> >.
>
> --
> 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/d0fd1d18-136b-41fa-b721-f64b9c487376%40www.fastmail.com
> .
>

-- 
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/CAA520fuU-BEcdg6mrAkTxmqpDhG9pHpD-1a%3DX7ZU-n8q57dKsg%40mail.gmail.com.

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