Discussion of Homotopy Type Theory and Univalent Foundations
help / Atom feed
* [HoTT] New theorem prover Arend is released
@ 2019-08-06 22:16 Валерий Исаев
2019-08-07 15:01  Andrej Bauer
 (2 more replies)
0 siblings, 3 replies; 20+ messages in thread
From: Валерий Исаев @ 2019-08-06 22:16 UTC (permalink / raw)
To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 2913 bytes --]

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

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
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.

[-- Attachment #1.2: Type: text/html, Size: 3367 bytes --]

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-06 22:16 [HoTT] New theorem prover Arend is released Валерий Исаев
@ 2019-08-07 15:01  Andrej Bauer
2019-08-07 22:13  Nicolai Kraus
2019-08-08 12:20  Jon Sterling
2 siblings, 0 replies; 20+ messages in thread
From: Andrej Bauer @ 2019-08-07 15:01 UTC (permalink / raw)
To: Валерий
Исаев,
Homotopy Type Theory

Very impressive indeed!

I don't think it's necessary to ask why we need another theorem
prover. However, we may reach a point when some consolidation will
have to happen, one way or another. Functional programming was a bit
like that (slightly before my time), and it consolidated around

With kind regards,

Andrej

--
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/CAB0nkh0UKEgnv85QEFt44CcbA9To3Js%3DEAhdB0xLy0M9F6Z2%2BA%40mail.gmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-06 22:16 [HoTT] New theorem prover Arend is released Валерий Исаев
2019-08-07 15:01  Andrej Bauer
@ 2019-08-07 22:13  Nicolai Kraus
2019-08-08  9:55    Valery Isaev
2019-08-08 12:20  Jon Sterling
From: Nicolai Kraus @ 2019-08-07 22:13 UTC (permalink / raw)
To: Валерий
Исаев
Cc: Homotopy Type Theory

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

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
>
> 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
>    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
> 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/CA%2BAZBBpjRJ8ndS-jWaL-NT3HOtQ1S8nb_tefa6P13zkLcbZJPA%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-07 22:13  Nicolai Kraus
@ 2019-08-08  9:55    Valery Isaev
2019-08-10  9:47      Michael Shulman
From: Valery Isaev @ 2019-08-08  9:55 UTC (permalink / raw)
To: Nicolai Kraus; +Cc: Homotopy Type Theory

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

You can say that they are hidden in the background, but I prefer to think
\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
>>
>> 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
>>    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.
>>
>> are welcome at google groups
>>
>> --
>> 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/CAA520fsVx%2BGUpYN%2ByPesJ_1PwKV0MfU%3DGQD4ovpfHhy%3DDuj7yA%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-06 22:16 [HoTT] New theorem prover Arend is released Валерий Исаев
2019-08-07 15:01  Andrej Bauer
2019-08-07 22:13  Nicolai Kraus
@ 2019-08-08 12:20  Jon Sterling
2019-08-08 12:29    Bas Spitters
From: Jon Sterling @ 2019-08-08 12:20 UTC (permalink / raw)
To: Martin Escardo' via Homotopy Type Theory

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
> 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
>  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/06e24c98-7409-4e75-88ee-a6e1bb891e1e%40www.fastmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-08 12:20  Jon Sterling
@ 2019-08-08 12:29    Bas Spitters
2019-08-08 14:44      Valery Isaev
From: Bas Spitters @ 2019-08-08 12:29 UTC (permalink / raw)
To: Jon Sterling; +Cc: Martin Escardo' via Homotopy Type Theory

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 an email to HomotopyTypeTheory+unsubscribe@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.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-08 12:29    Bas Spitters
@ 2019-08-08 14:44      Valery Isaev
2019-08-08 15:11        Jon Sterling
From: Valery Isaev @ 2019-08-08 14:44 UTC (permalink / raw)
To: Bas Spitters; +Cc: Jon Sterling, Martin Escardo' via Homotopy Type Theory

[-- 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 --]

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-08 14:44      Valery Isaev
@ 2019-08-08 15:11        Jon Sterling
2019-08-08 15:22          Valery Isaev
From: Jon Sterling @ 2019-08-08 15:11 UTC (permalink / raw)
To: Martin Escardo' via Homotopy Type Theory

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.

- 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!).

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://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.
> >  > > If you want to know about language updates, you can follow us on
> >  > >
> >  > > --
> >  > > 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 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>.
>
>  --
>  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 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.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-08 15:11        Jon Sterling
@ 2019-08-08 15:22          Valery Isaev
2019-08-10  9:42            Michael Shulman
From: Valery Isaev @ 2019-08-08 15:22 UTC (permalink / raw)
To: Jon Sterling; +Cc: Martin Escardo' via Homotopy Type Theory

[-- 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://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.
> > >  > > If you want to know about language updates, you can follow us on
> and
> > >  > > <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
> > >  > >
> <
> >.
> > >  >
> > >  > --
> > >  > 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:
> > >  > 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 <mailto:
> > >  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
> >
> <
> >.
>
> --
> 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/CAA520fuU-BEcdg6mrAkTxmqpDhG9pHpD-1a%3DX7ZU-n8q57dKsg%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-08 15:22          Valery Isaev
@ 2019-08-10  9:42            Michael Shulman
2019-08-10 12:24              Valery Isaev
From: Michael Shulman @ 2019-08-10  9:42 UTC (permalink / raw)
To: Valery Isaev; +Cc: Jon Sterling, HomotopyTypeTheory

There is a bit more subtlety here than is evident from the brief
description, since everything has to happen in an arbitrary slice
category of the model category.  But although the slices of a
cartesian model category are not in general again cartesian, they are
enriched model categories over the base, and so I think I agree that
this works since I lives in the base.

However, section 2.2 of https://valis.github.io/doc.pdf also appears
to assert that an equivalence can be made into a line in the universe
for which coercing along the line is *definitionally* equal to the
action of the given equivalence, and such that the line associated to
the identity equivalence is definitionally constant.  The latter seems
like it might be obtainable by a lifting property, but I don't
immediately see how to obtain the former in a model category?

--
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/CAOvivQzzLHnq%2BbXBzkFv3tST0GEUo4f2zmdj025LTaq%2BEMB7CQ%40mail.gmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
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
0 siblings, 2 replies; 20+ messages in thread
From: Michael Shulman @ 2019-08-10  9:47 UTC (permalink / raw)
To: Valery Isaev; +Cc: Nicolai Kraus, Homotopy Type Theory

On Thu, Aug 8, 2019 at 2:56 AM Valery Isaev <valery.isaev@gmail.com> wrote:
> 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.

How do you ensure that "every type in \Type0 which satisfies isSet is
equivalent to some type in \Set0"?  Is it just an axiom?

Also, since \Prop "has no predicative level", does this property
applied to \Prop imply that propositional resizing holds?

--
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.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-10  9:42            Michael Shulman
@ 2019-08-10 12:24              Valery Isaev
2019-08-10 23:37                Michael Shulman
From: Valery Isaev @ 2019-08-10 12:24 UTC (permalink / raw)
To: Michael Shulman; +Cc: Jon Sterling, HomotopyTypeTheory

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

The document is slightly outdated. We do not have the rule iso A B (λx ⇒ x)
(λx ⇒ x) idp idp i ⇒β A in the actual implementation since univalence is
true even without it. This rule has another problem. It seems that the
theory as presented in the document introduces a *quasi*-equivalence
between A = B and Equiv A B, which means that there are some true
statements which are not provable in it. The theory without this rule
should be completely equivalent to the ordinary HoTT, even though I cannot
prove this yet.

Regards,
Valery Isaev

сб, 10 авг. 2019 г. в 12:42, Michael Shulman <shulman@sandiego.edu>:

> There is a bit more subtlety here than is evident from the brief
> description, since everything has to happen in an arbitrary slice
> category of the model category.  But although the slices of a
> cartesian model category are not in general again cartesian, they are
> enriched model categories over the base, and so I think I agree that
> this works since I lives in the base.
>
> However, section 2.2 of https://valis.github.io/doc.pdf also appears
> to assert that an equivalence can be made into a line in the universe
> for which coercing along the line is *definitionally* equal to the
> action of the given equivalence, and such that the line associated to
> the identity equivalence is definitionally constant.  The latter seems
> like it might be obtainable by a lifting property, but I don't
> immediately see how to obtain the former in a model category?
>

--
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.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-10  9:47      Michael Shulman
@ 2019-08-10 12:30        Valery Isaev
2019-08-10 12:37        Valery Isaev
1 sibling, 0 replies; 20+ messages in thread
From: Valery Isaev @ 2019-08-10 12:30 UTC (permalink / raw)
To: Michael Shulman; +Cc: Nicolai Kraus, Homotopy Type Theory

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

In the theory, the rule looks like this:
A : \Type0    p : isSet A
----------------------------------
F(A,p) : \Set0

and we also add an equivalence between A and F(A,p). In the actual
implementation, you can do this using \use \level construction. If you can
prove that some \data or \record satisfies isSet (or, more generally, that
it is an n-type), then you can put this proof in \use \level function
corresponding to this definition and it will be put in the corresponding
universe. So, you can define \data F(A,p) with one constructor with one
parameter of type A and put it in \Set0.

Regards,
Valery Isaev

сб, 10 авг. 2019 г. в 12:47, Michael Shulman <shulman@sandiego.edu>:

> On Thu, Aug 8, 2019 at 2:56 AM Valery Isaev <valery.isaev@gmail.com>
> wrote:
> > You can say that they are hidden in the background, but I prefer to
> 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.
>
> How do you ensure that "every type in \Type0 which satisfies isSet is
> equivalent to some type in \Set0"?  Is it just an axiom?
>
> Also, since \Prop "has no predicative level", does this property
> applied to \Prop imply that propositional resizing holds?
>

--
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/CAA520fuDN9yffbCT6Hxv9kvB%3DWW%2BiUcTf%3DJuXi7kuD5NknWbfg%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-10  9:47      Michael Shulman
2019-08-10 12:30        Valery Isaev
@ 2019-08-10 12:37        Valery Isaev
1 sibling, 0 replies; 20+ messages in thread
From: Valery Isaev @ 2019-08-10 12:37 UTC (permalink / raw)
To: Michael Shulman; +Cc: Nicolai Kraus, Homotopy Type Theory

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

Yes, propositional resizing holds. \Prop classifies all subobjects.

Regards,
Valery Isaev

сб, 10 авг. 2019 г. в 12:47, Michael Shulman <shulman@sandiego.edu>:

> On Thu, Aug 8, 2019 at 2:56 AM Valery Isaev <valery.isaev@gmail.com>
> wrote:
> > You can say that they are hidden in the background, but I prefer to
> 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.
>
> How do you ensure that "every type in \Type0 which satisfies isSet is
> equivalent to some type in \Set0"?  Is it just an axiom?
>
> Also, since \Prop "has no predicative level", does this property
> applied to \Prop imply that propositional resizing holds?
>

--
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.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-10 12:24              Valery Isaev
@ 2019-08-10 23:37                Michael Shulman
2019-08-11 10:46                  Valery Isaev
From: Michael Shulman @ 2019-08-10 23:37 UTC (permalink / raw)
To: Valery Isaev; +Cc: Jon Sterling, HomotopyTypeTheory

On Sat, Aug 10, 2019 at 5:25 AM Valery Isaev <valery.isaev@gmail.com> wrote:
> The document is slightly outdated. We do not have the rule iso A B (λx ⇒ x) (λx ⇒ x) idp idp i ⇒β A in the actual implementation since univalence is true even without it. This rule has another problem. It seems that the theory as presented in the document introduces a quasi-equivalence between A = B and Equiv A B, which means that there are some true statements which are not provable in it.

I don't understand.  By "quasi-equivalence" do you mean an incoherent
equivalence (what the book calls a map with a quasi-inverse)?  If so,
then every quasi-equivalence can of course be promoted to a strong
equivalence.

However, as I said, I'm more worried about the fourth rule coe_{λ k ⇒
iso A B f g p q k} a right ⇒β f a.  That's the one that I have trouble
seeing how to interpret in a model category.  Can you say anything

> If you can prove that some \data or \record satisfies isSet (or, more generally, that it is an n-type), then you can put this proof in \use \level function corresponding to this definition and it will be put in the corresponding universe.

What does it mean for it to be "put in" the corresponding universe?
The documentation for \use \level makes it sound as though the
definition *itself*, rather than something equivalent to it, ends up
in the corresponding universe.  How is the equivalence between A and
F(A,p) accessed inside the proof assistant?

--
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/CAOvivQxKMPvpm9Vwkt4ARR7R5qLmzJMUkFCrf%3DrFUL5sd4nXLQ%40mail.gmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-10 23:37                Michael Shulman
@ 2019-08-11 10:46                  Valery Isaev
2019-08-11 12:39                    Michael Shulman
From: Valery Isaev @ 2019-08-11 10:46 UTC (permalink / raw)
To: Michael Shulman; +Cc: Jon Sterling, HomotopyTypeTheory

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

вс, 11 авг. 2019 г. в 02:37, Michael Shulman <shulman@sandiego.edu>:

> On Sat, Aug 10, 2019 at 5:25 AM Valery Isaev <valery.isaev@gmail.com>
> wrote:
> > The document is slightly outdated. We do not have the rule iso A B (λx ⇒
> x) (λx ⇒ x) idp idp i ⇒β A in the actual implementation since univalence is
> true even without it. This rule has another problem. It seems that the
> theory as presented in the document introduces a quasi-equivalence between
> A = B and Equiv A B, which means that there are some true statements which
> are not provable in it.
>
> I don't understand.  By "quasi-equivalence" do you mean an incoherent
> equivalence (what the book calls a map with a quasi-inverse)?  If so,
> then every quasi-equivalence can of course be promoted to a strong
> equivalence.
>

Yes, a quasi-equivalence is a function together with its quasi-inverse. The
problem is that we've got some terms in the theory of which we know
nothing about. It's the same as if I just add a new type *Magic *without
any additional rules. Then we cannot prove anything about it and the
resulting theory won't be equivalent to the original one.

>
> However, as I said, I'm more worried about the fourth rule coe_{λ k ⇒
> iso A B f g p q k} a right ⇒β f a.  That's the one that I have trouble
> seeing how to interpret in a model category.  Can you say anything
>

I don't remember well, but I think the idea is that you need to prove that
there is a trivial cofibration Eq(A,B) -> F(U^I,A,B), where the first
object is the object of equivalences between A and B and the second object
is the fiber of U^I over A and B. The fact that this map is a weak
equivalence is just the univalence axiom. The problem is to show that it is
a cofibration and whether this is true or not depends on the definition of
Eq(A,B). I don't actually remember whether I finished this proof.

>
> > If you can prove that some \data or \record satisfies isSet (or, more
> generally, that it is an n-type), then you can put this proof in \use
> \level function corresponding to this definition and it will be put in the
> corresponding universe.
>
> What does it mean for it to be "put in" the corresponding universe?
>

I mean F(A,p) will have type \Set0 instead of \Type0 that it would have
without the \use \level annotation.

> The documentation for \use \level makes it sound as though the
> definition *itself*, rather than something equivalent to it, ends up
> in the corresponding universe.

Yes, F(A,p) *itself* has type \Set0, but A still has type \Type0.

> How is the equivalence between A and
> F(A,p) accessed inside the proof assistant?
>

Since F(A,p) is the usual (inductive) data type, you can do everything you
can do with other data types. In particular, since it has only one
constructor with one parameter A, it is easy to proof that it is equivalent
to A.

--
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/CAA520ftYLYwiZs0B3fmuYb%3D%3D8mWiOpVD0yVbV8otfTEfgWV8UQ%40mail.gmail.com.

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

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-11 10:46                  Valery Isaev
@ 2019-08-11 12:39                    Michael Shulman
2019-08-11 16:55                      Michael Shulman
From: Michael Shulman @ 2019-08-11 12:39 UTC (permalink / raw)
To: Valery Isaev; +Cc: Jon Sterling, HomotopyTypeTheory

On Sun, Aug 11, 2019 at 6:47 AM Valery Isaev <valery.isaev@gmail.com> wrote:
> I don't remember well, but I think the idea is that you need to prove that there is a trivial cofibration Eq(A,B) -> F(U^I,A,B), where the first object is the object of equivalences between A and B and the second object is the fiber of U^I over A and B. The fact that this map is a weak equivalence is just the univalence axiom. The problem is to show that it is a cofibration and whether this is true or not depends on the definition of Eq(A,B). I don't actually remember whether I finished this proof.

Yes, in a straightforward approach that's what you would need to
prove, or more precisely that the map Eq -> U^I is a trivial
cofibration in the slice over UxU (since the lifting has to be done in
the universal case rather than just over each global element).
Possibly you could get away with less, since you're only asking to
recover the action of the given equivalence as a function (rather than
the entire equivalence data).  Perhaps a clever choice of fibration
structure in the equivalence extension property would suffice.

> Since F(A,p) is the usual (inductive) data type, you can do everything you can do with other data types. In particular, since it has only one constructor with one parameter A, it is easy to proof that it is equivalent to A.

Okay, it sounds like you're saying that the datatype defined with
\use\level is F(A,p) and the analogous one defined without \use\level
is A, while both have their usual rules but are not identical.  In
this case you have somewhat *more* than an equivalence between F(A,p)
and A, at least if all datatypes have their usual definitional
computation rules, since an arbitrary type "F(A,p)" that is only
*equivalent* to a datatype will only inherit a typal computation rule.
It seems plausible though that one could construct universes of
n-types that are strictly closed under a given datatype construction
that preserves n-types (at least, assuming one can do the same for
arbitrary universes).

However, the documentation also suggests that \use\level can be
applied to plain definitions (\func).  How is F(A,p) distinguished
from A in this case?

--
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/CAOvivQxMwmkA0o2XBecGQaiaVFO0rjwKvZfbMqS%2Be363GJwRbA%40mail.gmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-11 12:39                    Michael Shulman
@ 2019-08-11 16:55                      Michael Shulman
2019-08-12 14:44                        Daniel R. Grayson
From: Michael Shulman @ 2019-08-11 16:55 UTC (permalink / raw)
To: HomotopyTypeTheory

In an off-list discussion, Valery clarified to me that \use\level for
\func does not actually put the type in the corresponding universe,
only marks it as having the corresponding homotopy level (and added
some documentation
https://arend-lang.github.io/documentation/language-reference/definitions/level#use-level-for-functions).
However, it also emerged that F(A,p) can also be *defined* for an
arbitrary type A (and an externally fixed n) as

\record F (A : \Type) (p : ofHLevel A n) {
| in : A
} \where \use \level isntype (A : \Type) (p : ofHLevel A n) : ofHLevel A n => p

and that because records have definitional eta-conversion, this F(A,p)
will actually be definitionally isomorphic to A, rather than just
equivalent to it.

In particular, since \Prop is invariant under predicative level, this
means that (in the current version of Arend) every h-proposition is
definitionally isomorphic to one living in the lowest universe.  This
is not quite as strong as Voeovdsky's propositional resizing rule
(that every h-proposition *itself* lives in the lowest universe), but
I find it about equally semantically dubious, and in particular it's
unclear whether it has any univalent models (not even classically in
simplicial sets).  Perhaps it does; but until such models are known,
it may be better to avoid using this feature for \Prop, and perhaps
add a restriction to Arend preventing it.

On Sun, Aug 11, 2019 at 8:39 AM Michael Shulman <shulman@sandiego.edu> wrote:
>
> On Sun, Aug 11, 2019 at 6:47 AM Valery Isaev <valery.isaev@gmail.com> wrote:
> > I don't remember well, but I think the idea is that you need to prove that there is a trivial cofibration Eq(A,B) -> F(U^I,A,B), where the first object is the object of equivalences between A and B and the second object is the fiber of U^I over A and B. The fact that this map is a weak equivalence is just the univalence axiom. The problem is to show that it is a cofibration and whether this is true or not depends on the definition of Eq(A,B). I don't actually remember whether I finished this proof.
>
> Yes, in a straightforward approach that's what you would need to
> prove, or more precisely that the map Eq -> U^I is a trivial
> cofibration in the slice over UxU (since the lifting has to be done in
> the universal case rather than just over each global element).
> Possibly you could get away with less, since you're only asking to
> recover the action of the given equivalence as a function (rather than
> the entire equivalence data).  Perhaps a clever choice of fibration
> structure in the equivalence extension property would suffice.
>
> > Since F(A,p) is the usual (inductive) data type, you can do everything you can do with other data types. In particular, since it has only one constructor with one parameter A, it is easy to proof that it is equivalent to A.
>
> Okay, it sounds like you're saying that the datatype defined with
> \use\level is F(A,p) and the analogous one defined without \use\level
> is A, while both have their usual rules but are not identical.  In
> this case you have somewhat *more* than an equivalence between F(A,p)
> and A, at least if all datatypes have their usual definitional
> computation rules, since an arbitrary type "F(A,p)" that is only
> *equivalent* to a datatype will only inherit a typal computation rule.
> It seems plausible though that one could construct universes of
> n-types that are strictly closed under a given datatype construction
> that preserves n-types (at least, assuming one can do the same for
> arbitrary universes).
>
> However, the documentation also suggests that \use\level can be
> applied to plain definitions (\func).  How is F(A,p) distinguished
> from A in this case?

--
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/CAOvivQzjOnpZj27f44GyDjtX1-WNwWN8aqOnv3L7gkVnpYpnyw%40mail.gmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-11 16:55                      Michael Shulman
@ 2019-08-12 14:44                        Daniel R. Grayson
2019-08-12 17:32                          Michael Shulman
From: Daniel R. Grayson @ 2019-08-12 14:44 UTC (permalink / raw)
To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 448 bytes --]

Mike, what do you mean by "definitionally isomorphic" ?

--
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.

[-- Attachment #1.2: Type: text/html, Size: 757 bytes --]

^ permalink raw reply	[flat|nested] 20+ messages in thread

* Re: [HoTT] New theorem prover Arend is released
2019-08-12 14:44                        Daniel R. Grayson
@ 2019-08-12 17:32                          Michael Shulman
0 siblings, 0 replies; 20+ messages in thread
From: Michael Shulman @ 2019-08-12 17:32 UTC (permalink / raw)
To: Daniel R. Grayson; +Cc: Homotopy Type Theory

Maps f : A -> F(A,p) and g : F(A,p) -> A such that g(f(x)) == x and
f(g(y)) == y, where == means definitional/judgmental equality.

On Mon, Aug 12, 2019 at 10:44 AM Daniel R. Grayson
<danielrichardgrayson@gmail.com> wrote:
>
> Mike, what do you mean by "definitionally isomorphic" ?
>
> --
> 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.

--
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/CAOvivQw17Au6b1P6FwxZF7x84qM9vhCgOf5xuKcdzW59_F67Ag%40mail.gmail.com.

^ permalink raw reply	[flat|nested] 20+ messages in thread

end of thread, back to index

2019-08-06 22:16 [HoTT] New theorem prover Arend is released Валерий Исаев
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
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


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