[-- Attachment #1: Type: text/plain, Size: 1425 bytes --] Dear all, CT Octoberfest 2019 will be held at Johns Hopkins University, Baltimore on the 26th and 27th of October. The meeting is free and open to all. All details, including instructions on contributing a talk or ``registering'', and accommodation and travel recommendations, are available on the website: https://ct-octoberfest.github.io . In conjunction with Octoberfest we are pleased to announce a plenary talk, joint with the Johns Hopkins Category Theory seminar, on Friday the 26th of October: Mike Shulman will be talking on the theme of internal languages. Those wishing to speak should send an email to ctoctoberfest19@math.jhu.edu with the subject ``Submission'' including the submission title and any notes or special requests. The talk submission deadline is the 25th of September, anywhere on earth. For any queries related to the meeting please do not hesitate to contact tslil clingman at tslil@jhu.edu or the meeting email address ctoctoberfest19@math.jhu.edu. We hope to see you there! -- 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/BYAPR01MB53515ADE68E1795AB5A7EAAEB9A60%40BYAPR01MB5351.prod.exchangelabs.com. [-- Attachment #2: Type: text/html, Size: 2531 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2719 bytes --] Resurrecting this thread from many years ago, because I was thinking about it again recently, it seems to me that although { f & isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e judgmentally, it doesn't satisfy the rule that sym id = id judgmentally. (In particular, I am not sure what relational equivalence to use for the identity equivalence which does not change judgmentally when I flip the order of its arguments.) Is there a version of equivalence which simultaneously satisfies that the inverse of the identity is judgmentally the identity, and that inverting an equivalence twice judgmentally gives you what you started with? -Jason On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <vladimir@ias.edu> wrote: > In general no. But their model is essentially syntactic and more or less > complete. Or, to be more precise, I would expect it to > be more or less complete. > > V. > > > On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine < > p.l.lumsdaine@gmail.com> wrote: > > On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vladimir@ias.edu> > wrote: > >> The question is about how you interpret this operation for the univalent >> universe. If there is an interpretation of such an operation then there is >> a way to define equivalences between types in an involutionary way. >> > > I don’t follow why this should be the case. This shows that there is some > notion of equivalence *in the model* (i.e. constructed in the meta-theory) > which is strictly involutive. But there is no reason that this notion need > be definable in the syntax of the object theory, is there? > > –p. > > -- > 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. > For more options, visit https://groups.google.com/d/optout. > > > -- > 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. > For more options, visit https://groups.google.com/d/optout. > -- 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/CAKObCao60%3DRFWY%3DCn0BTV9bWcRCQXRSqOjvCYbS37mHOeJ0Yqg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4424 bytes --]

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. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/61d38dbf-541b-4d5a-97f2-094c3f3c1da4%40googlegroups.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.

[-- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/61d38dbf-541b-4d5a-97f2-094c3f3c1da4%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 757 bytes --]

FINAL CALL FOR PARTICIPATION: FoPPS 2019: Nominal Techniques 3rd Summer School on Foundations of Programming and Software Systems 10-15 September, Warsaw, Poland https://www.mimuw.edu.pl/~fopss19/ ================================================================== The 2019 Alonzo Church Award was given to M. J. Gabbay and A. M. Pitts for their ground-breaking work on nominal sets. (https://siglog.org/winners-of-the-2019-alonzo-church-award/) Do you want to learn what that was about? Come to FoPSS 2019! ================================================================== The Summer School on Foundations of Programming and Software Systems (FoPSS) was jointly created by EATCS, ETAPS, ACM SIGLOG and ACM SIGPLAN. It was first organised in 2017. The goal is to introduce the participants to various aspects of computation theory and programming languages. The school, spread over a single week, is aimed at students and researchers in Theoretical Computer Science, broadly construed. Each year the school is focused on a particular, actively researched topic. Our focus in 2019 are Nominal Techniques in Computer Science. For the introduction and cornerstone contributions to this area Murdoch J. Gabbay and Andrew M. Pitts received the 2019 Alonzo Church Award. Both of them are among the lecturers of FoPSS 2019. The scientific programme of the school is available from our website: https://www.mimuw.edu.pl/~fopss19/programme.html Registration fee includes lunches, coffee breaks and accommodation in a hotel within a walking distance from the school venue. We have a few scholarships available to participants who have difficult access to funding. Registration is open! ================================================================== COLOCATED EVENT: Highlights 2019: 7th annual conference on Highlights of Logic, Games and Automata 17-20 September (http://highlights-conference.org) -- 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/E3B01D81-A7AE-45E2-A6DA-0360C83F84FA%40mimuw.edu.pl.

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.

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.

[-- 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 > about that? > 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 --]

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 about that? > 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.

[-- 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 > 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520fuS3O%3DyPtzHUkTxStiadxP%3DSr4%2BjaBpZQuA93LXkWfzTg%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2510 bytes --]

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

[-- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520ftTacC4iegu2UM887nbyJWQTByMKhrcsftKPXCadH06kQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2849 bytes --]

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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzAdt3Pj0TtoxZA29R9XyZm%2Bxwz8-9AN5ap0iatf-%3DFLQ%40mail.gmail.com.

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.

[-- Attachment #1: Type: text/plain, Size: 7798 bytes --] I think it is an excellent question. However, looking at the examples it may seem that we only need QITs, that is set-truncated HITs. However, this is not true when you are dealing with higher structures that arise naturally like the type of sets. For example when you define the integers as a quotient, or nicer as a QIT, you can only eliminate into types that are sets, for example you cannot define a function from the Integers into Set. However, this can be addressed by replacing set-truncation with a coherence law, in this case you basically say that integers have 0 and suc and suc is an equivalence. You can prove that the HIT constructed by these principles is a Set (this is actually harder than it seems) – Luis Soccola and I have recently written a paper about this (need to put it on arxiv). Another example is the intrinsic presentation of type theory as the initial Category with Families which was already mentioned. Again the problem is that you need to set-truncate but then you cannot even define the set-interpretation. This can be again addressed by adding some coherence laws (need to check the details) and you get a coherent version of CWFs which enable us to eliminate into any 1-type, including the universe of sets. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Timothy Carstens <intoverflow@gmail.com> Date: Thursday, 8 August 2019 at 23:09 Cc: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] (Beginner's question) Uses of HITs beyond homotopy theory Thank you for the excellent replies! It looks like I was struggling with a lack of imagination while the answer was staring me right in the face. On Thu, Aug 8, 2019 at 2:49 PM Michael Shulman <shulman@sandiego.edu<mailto:shulman@sandiego.edu>> wrote: More generally, all colimits other than coproducts are HITs (of the "non-recursive" variety). This includes both homotopy colimits and ordinary colimits of sets (obtained by 0-truncating homotopy colimits). Having colimits of sets is fairly essential for nearly all ordinary set-based mathematics, even for people who don't care about homotopy theory or higher category theory in the slightest. There aren't really papers specifically about this, because it's so vast, and because there's not much to say other than the observation that colimits exist, since at that point you can just appeal to the long-known fact that once the category of sets satisfies certain basic properties (Lawvere's "Elementary Theory of the Category of Sets") it suffices as a basis on which to develop a large amount of mathematics. The verification of these axioms in HoTT with HITs can be found in section 10.1 of the HoTT Book. (Before HITs, people formalizing set-based mathematics in type theory used "setoids" to mimic quotients and other colimits.) Beyond this, in set-based mathematics HITs are used to construct free algebraic structures, as Niels said. Some free algebraic structures (free monoids, free groups, free rings, etc.) can be constructed based only on the axioms of ETCS, but for fancier (and in particular, infinitary) algebraic structures one needs more. In fact there are algebraic theories for which free algebraic structures cannot be constructed in ZF (at least, under a large cardinal assumption): the idea is to use a theory to encode the existence of large regular cardinals, which cannot be constructed in ZF (see Blass's paper "Words, free algebras, and coequalizers"). But HITs suffice to construct even free infinitary algebras of this sort; see e.g. section 9 of my paper with Peter Lumsdaine, "Semantics of higher inductive types". Thus, HITs can be useful for doing (universal) algebra constructively, where here "constructively" can even mean "with classical logic but without the axiom of choice". On Thu, Aug 8, 2019 at 1:18 PM Steve Awodey <steveawodey@gmail.com<mailto:steveawodey@gmail.com>> wrote: > > quotients by equivalence relations. > see HoTT Book 6.10 > > On Aug 8, 2019, at 2:32 PM, Timothy Carstens <intoverflow@gmail.com<mailto:intoverflow@gmail.com>> wrote: > > Sorry for the broad & naive question. I'm a geometer by training but have been working in compsci for most of my career (with lots of time spent in Coq verifying programs). > > I've got a naive question that I hope isn't too inappropriate for this list: can anyone suggest some papers that show applications of HITs? I'm embarrassed to admit it, but I don't know any applications outside of synthetic homotopy theory and higher categories. > > Perhaps categorical semantics? But even still I'm not personally aware of any applied results from that domain (contrast with operational semantics; but I am extremely ignorant, so please correct me!) > > All my best and apologies in advance if this is off-topic for this list, > -t > > > -- > 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/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%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<mailto:HomotopyTypeTheory%2Bunsubscribe@googlegroups.com>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.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/CAOvivQyYyPzpT0Y04vi27gdg6Un147RkJ4tyPcCRC_Tsed5PMA%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<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zH1qWjaQYy-jOGfuxm--cLw3AJ6y6WPheqHmA8Dr1B%2Bww%40mail.gmail.com<https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zH1qWjaQYy-jOGfuxm--cLw3AJ6y6WPheqHmA8Dr1B%2Bww%40mail.gmail.com?utm_medium=email&utm_source=footer>. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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/85B0463F-8B1E-4677-924D-05162484B926%40nottingham.ac.uk. [-- Attachment #2: Type: text/html, Size: 12285 bytes --]

[-- Attachment #1: Type: text/plain, Size: 4999 bytes --] Thank you for the excellent replies! It looks like I was struggling with a lack of imagination while the answer was staring me right in the face. On Thu, Aug 8, 2019 at 2:49 PM Michael Shulman <shulman@sandiego.edu> wrote: > More generally, all colimits other than coproducts are HITs (of the > "non-recursive" variety). This includes both homotopy colimits and > ordinary colimits of sets (obtained by 0-truncating homotopy > colimits). Having colimits of sets is fairly essential for nearly all > ordinary set-based mathematics, even for people who don't care about > homotopy theory or higher category theory in the slightest. There > aren't really papers specifically about this, because it's so vast, > and because there's not much to say other than the observation that > colimits exist, since at that point you can just appeal to the > long-known fact that once the category of sets satisfies certain basic > properties (Lawvere's "Elementary Theory of the Category of Sets") it > suffices as a basis on which to develop a large amount of mathematics. > The verification of these axioms in HoTT with HITs can be found in > section 10.1 of the HoTT Book. (Before HITs, people formalizing > set-based mathematics in type theory used "setoids" to mimic quotients > and other colimits.) > > Beyond this, in set-based mathematics HITs are used to construct free > algebraic structures, as Niels said. Some free algebraic structures > (free monoids, free groups, free rings, etc.) can be constructed based > only on the axioms of ETCS, but for fancier (and in particular, > infinitary) algebraic structures one needs more. In fact there are > algebraic theories for which free algebraic structures cannot be > constructed in ZF (at least, under a large cardinal assumption): the > idea is to use a theory to encode the existence of large regular > cardinals, which cannot be constructed in ZF (see Blass's paper > "Words, free algebras, and coequalizers"). But HITs suffice to > construct even free infinitary algebras of this sort; see e.g. section > 9 of my paper with Peter Lumsdaine, "Semantics of higher inductive > types". Thus, HITs can be useful for doing (universal) algebra > constructively, where here "constructively" can even mean "with > classical logic but without the axiom of choice". > > On Thu, Aug 8, 2019 at 1:18 PM Steve Awodey <steveawodey@gmail.com> wrote: > > > > quotients by equivalence relations. > > see HoTT Book 6.10 > > > > On Aug 8, 2019, at 2:32 PM, Timothy Carstens <intoverflow@gmail.com> > wrote: > > > > Sorry for the broad & naive question. I'm a geometer by training but > have been working in compsci for most of my career (with lots of time spent > in Coq verifying programs). > > > > I've got a naive question that I hope isn't too inappropriate for this > list: can anyone suggest some papers that show applications of HITs? I'm > embarrassed to admit it, but I don't know any applications outside of > synthetic homotopy theory and higher categories. > > > > Perhaps categorical semantics? But even still I'm not personally aware > of any applied results from that domain (contrast with operational > semantics; but I am extremely ignorant, so please correct me!) > > > > All my best and apologies in advance if this is off-topic for this list, > > -t > > > > > > -- > > 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/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%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/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.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/CAOvivQyYyPzpT0Y04vi27gdg6Un147RkJ4tyPcCRC_Tsed5PMA%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/CAJGt_zH1qWjaQYy-jOGfuxm--cLw3AJ6y6WPheqHmA8Dr1B%2Bww%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 6890 bytes --]

More generally, all colimits other than coproducts are HITs (of the "non-recursive" variety). This includes both homotopy colimits and ordinary colimits of sets (obtained by 0-truncating homotopy colimits). Having colimits of sets is fairly essential for nearly all ordinary set-based mathematics, even for people who don't care about homotopy theory or higher category theory in the slightest. There aren't really papers specifically about this, because it's so vast, and because there's not much to say other than the observation that colimits exist, since at that point you can just appeal to the long-known fact that once the category of sets satisfies certain basic properties (Lawvere's "Elementary Theory of the Category of Sets") it suffices as a basis on which to develop a large amount of mathematics. The verification of these axioms in HoTT with HITs can be found in section 10.1 of the HoTT Book. (Before HITs, people formalizing set-based mathematics in type theory used "setoids" to mimic quotients and other colimits.) Beyond this, in set-based mathematics HITs are used to construct free algebraic structures, as Niels said. Some free algebraic structures (free monoids, free groups, free rings, etc.) can be constructed based only on the axioms of ETCS, but for fancier (and in particular, infinitary) algebraic structures one needs more. In fact there are algebraic theories for which free algebraic structures cannot be constructed in ZF (at least, under a large cardinal assumption): the idea is to use a theory to encode the existence of large regular cardinals, which cannot be constructed in ZF (see Blass's paper "Words, free algebras, and coequalizers"). But HITs suffice to construct even free infinitary algebras of this sort; see e.g. section 9 of my paper with Peter Lumsdaine, "Semantics of higher inductive types". Thus, HITs can be useful for doing (universal) algebra constructively, where here "constructively" can even mean "with classical logic but without the axiom of choice". On Thu, Aug 8, 2019 at 1:18 PM Steve Awodey <steveawodey@gmail.com> wrote: > > quotients by equivalence relations. > see HoTT Book 6.10 > > On Aug 8, 2019, at 2:32 PM, Timothy Carstens <intoverflow@gmail.com> wrote: > > Sorry for the broad & naive question. I'm a geometer by training but have been working in compsci for most of my career (with lots of time spent in Coq verifying programs). > > I've got a naive question that I hope isn't too inappropriate for this list: can anyone suggest some papers that show applications of HITs? I'm embarrassed to admit it, but I don't know any applications outside of synthetic homotopy theory and higher categories. > > Perhaps categorical semantics? But even still I'm not personally aware of any applied results from that domain (contrast with operational semantics; but I am extremely ignorant, so please correct me!) > > All my best and apologies in advance if this is off-topic for this list, > -t > > > -- > 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/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%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/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.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/CAOvivQyYyPzpT0Y04vi27gdg6Un147RkJ4tyPcCRC_Tsed5PMA%40mail.gmail.com.

[-- Attachment #1: Type: text/plain, Size: 1924 bytes --] quotients by equivalence relations. see HoTT Book 6.10 > On Aug 8, 2019, at 2:32 PM, Timothy Carstens <intoverflow@gmail.com> wrote: > > Sorry for the broad & naive question. I'm a geometer by training but have been working in compsci for most of my career (with lots of time spent in Coq verifying programs). > > I've got a naive question that I hope isn't too inappropriate for this list: can anyone suggest some papers that show applications of HITs? I'm embarrassed to admit it, but I don't know any applications outside of synthetic homotopy theory and higher categories. > > Perhaps categorical semantics? But even still I'm not personally aware of any applied results from that domain (contrast with operational semantics; but I am extremely ignorant, so please correct me!) > > All my best and apologies in advance if this is off-topic for this list, > -t > > > -- > 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+unsubscribe@googlegroups.com>. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%40mail.gmail.com <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%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/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.com. [-- Attachment #2: Type: text/html, Size: 3038 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1803 bytes --] Some established applications of HITs outside of synthetic homotopy theory: - Partiality monad, see "Partiality Revisited" by Altenkirch, Danielsson, and Kraus - Type Theory in Type Theory, see 'Type Theory in Type Theory with Quotient Inductive Inductive Types' and 'Normalization by evaluation for dependent types' by Altenkirch and Kaposi - Free algebraic structures, see HoTT book 6.11 and the paper "Finite Sets in Homotopy Type Theory" by Frumin, Geuvers, Gondelman, Van der Weide - Patch theory, see 'Homotopical Patch Theory' by Angiuli, Morehouse, Licata, and Harper On Thursday, August 8, 2019 at 8:33:06 PM UTC+2, Timothy Carstens wrote: > > Sorry for the broad & naive question. I'm a geometer by training but have > been working in compsci for most of my career (with lots of time spent in > Coq verifying programs). > > I've got a naive question that I hope isn't too inappropriate for this > list: can anyone suggest some papers that show applications of HITs? I'm > embarrassed to admit it, but I don't know any applications outside of > synthetic homotopy theory and higher categories. > > Perhaps categorical semantics? But even still I'm not personally aware of > any applied results from that domain (contrast with operational semantics; > but I am extremely ignorant, so please correct me!) > > All my best and apologies in advance if this is off-topic for this list, > -t > > -- 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/bc0fb45d-fe21-4380-bfcb-70cc58fbeef2%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 2446 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1127 bytes --] Sorry for the broad & naive question. I'm a geometer by training but have been working in compsci for most of my career (with lots of time spent in Coq verifying programs). I've got a naive question that I hope isn't too inappropriate for this list: can anyone suggest some papers that show applications of HITs? I'm embarrassed to admit it, but I don't know any applications outside of synthetic homotopy theory and higher categories. Perhaps categorical semantics? But even still I'm not personally aware of any applied results from that domain (contrast with operational semantics; but I am extremely ignorant, so please correct me!) All my best and apologies in advance if this is off-topic for this list, -t -- 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/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 1589 bytes --]

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

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

[-- 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://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. > > > 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/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. > 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. [-- Attachment #2: Type: text/html, Size: 9642 bytes --]

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. > > 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/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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSLoX8gKy54NQM6SNoi43wVA0A1Ad59qKs6prULkh6zBw%40mail.gmail.com.

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