Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Valery Isaev <valery.isaev@gmail.com>
To: Nicolai Kraus <nicolai.kraus@gmail.com>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] New theorem prover Arend is released
Date: Thu, 8 Aug 2019 12:55:46 +0300
Message-ID: <CAA520fsVx+GUpYN+yPesJ_1PwKV0MfU=GQD4ovpfHhy=Duj7yA@mail.gmail.com> (raw)
In-Reply-To: <CA+AZBBpjRJ8ndS-jWaL-NT3HOtQ1S8nb_tefa6P13zkLcbZJPA@mail.gmail.com>

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

You can say that they are hidden in the background, but I prefer to think
about this in a different way. I think about \Set0 as a *strict* subtype of
\Type0. In comparison, the type \Sigma (A : \Type0) (isSet A) is only
homotopically embeds into \Type0. It is equivalent to \Set0, but not
isomorphic to it. In particular, this means that every type in \Set0
satisfies isSet and every type in \Type0 which satisfies isSet is
equivalent to some type in \Set0, but not necessarily belongs to \Set0
itself. So, if we have (1), we also have (2) and we do not have (3). It may
be true that A is a 2-type, which means that there is a type A' : \2-Type 1
equivalent to A, but A itself does not belong to \2-Type 1.

Regards,
Valery Isaev


чт, 8 авг. 2019 г. в 01:13, Nicolai Kraus <nicolai.kraus@gmail.com>:

> Exciting and impressive! Many of Arend's features sound very useful!
> I find the universes most interesting, but I don't understand how exactly
> they work. From your site, I learned:
> * A universe in Arend has two parameters, for size and for homotopy level.
> * Universes are cumulative in both parameters.
>
> Is type-checking still decidable? Say, we have this judgment:
> (1)  A : \3-Type 1
> We have
> (2)  A : \4-Type 1
> by cumulativity, but it shouldn't be decidable whether we also have
> (3)  A : \2-Type 1.
> In book-HoTT, only (1) would type-check, since A would be a pair of a type
> and a proof of its homotopy level (i.e. you can only get (2,3) by changing
> the proof). But your site says these proofs don't need to be carried
> around. Are they still somewhere hidden in the background?
>
>
>
> On Wed, Aug 7, 2019 at 12:16 AM Валерий Исаев <valery.isaev@gmail.com>
> 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.
>> 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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520fsVx%2BGUpYN%2ByPesJ_1PwKV0MfU%3DGQD4ovpfHhy%3DDuj7yA%40mail.gmail.com.

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

  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 [this message]
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
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,
  and reply-to-all from there: mbox

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

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAA520fsVx+GUpYN+yPesJ_1PwKV0MfU=GQD4ovpfHhy=Duj7yA@mail.gmail.com' \
    --to=valery.isaev@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=nicolai.kraus@gmail.com \
    /path/to/YOUR_REPLY

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

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox