From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vs1-xe37.google.com (mail-vs1-xe37.google.com [IPv6:2607:f8b0:4864:20::e37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 87a665dd for ; Thu, 8 Aug 2019 14:45:34 +0000 (UTC) Received: by mail-vs1-xe37.google.com with SMTP id o23sf1518561vsj.6 for ; Thu, 08 Aug 2019 07:45:34 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565275533; cv=pass; d=google.com; s=arc-20160816; b=fZn1VuRxDGZF3tm/DJiLFtU60VQDdwnCvAa1yeSQxqG1vZVoqev4hgeSC4RDwQ7Xuu eoTiwM8gfNhV74IJKku0LgsaVX/yc21YCmqIzF9tBMWZwAAX9q5mQgPgY4uTUHcnDxcs YsDxWEO45B1Ore4uB4a/IbqdGhW+iStYvbj3TPLrOPZYjMWDy6vBjh8pygpsa0U03WwQ 94jWpQk6d+W+BSGl7tBdyUsP9W0JhuLlQ6hy0ooIhs3FLtH6+HiQSatKo8QWMCghhZse EmUgUvZZz1c7xEPAyDCY3kfplrJgnRHS/rykML58NlUZVE04f3q7sgIiO6Wiw4n1Z9nu sQPg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=EZ+Hm4SxeRaHZuoo9bM0zEfIlZ3DfX4WWNIZo1ncI0M=; b=Fpm3bb+m6aq0GjAxkbO0NIBxfUivGlcLEeDpwEgzx9+T6bJSMrLLVZciW1+f2rOp4m yqoUbnMyglrlFt1yhuOVSOn+qqI0C674gx0SlnQSbz+bl+y288VUhu7kNSS8JyW5UI7q pe0t6/vJQksILDp5aBfYODMNGjsB78jAy7iJAb5G/9sgF7kyZQA9TYyZCZmM8Ls7/Jwq Mo1MTBKlb8eR/tQN+rnMS5fH6wAQ9dILJMwD7/oaZWOJTqoIqn+VvL7lzhi9GTdCnBF3 +d76ASaa2azdAArGBrbBGbqqJnrGI5jm5CKYRBFsIODo7UxC3dvzfmVm9JiRV7zngOEE 2trw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="ot/5oGef"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32e as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=EZ+Hm4SxeRaHZuoo9bM0zEfIlZ3DfX4WWNIZo1ncI0M=; b=BIPwuWsnwzOmkdmC33jTK3F2RAom8OY5PQYJ1dM13ZeMP+oq9Zs9e/IxlKaUEEQbd4 goey6UCiLLC0zwpynyirqvhoVyDjj6F2Nl8RhNs5Gv4IWkOUOJ7AiQdtqtx1fQVQu4NL F1akFcnxsaigpCf1MGoIAb1MhenDatOJtvr/Pp7yAe89XcyWIUVc/0OFB/2TAGh7Qcc8 UpgIgyD6+p0O+CgcrlzLL5rM3CP8PcvwWhjN4Y2U9UrlaIYQyoqEjW9r8oKXM4n/mxI8 7NYP8T6tmmCOgsfyVME2PBZUkYqEa9WlUu9up8v8IEmsnwVkbMVXnFD2LwJcqv6jIFYm op2g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=EZ+Hm4SxeRaHZuoo9bM0zEfIlZ3DfX4WWNIZo1ncI0M=; b=tL9K20DLK1hbfSWRSkzU5ZWWIWhrMAg4tu+LIiTnox2cjpiVe9A+7ni/sVxuf/AsSK +vlrygMDfFxePeFFsyZwzshhqfJO75rd6LUelQMCGRtlQvKbhgOemV33IQE4F7sETjjF RJyRvrtMIivwQ71disU6dRZ1GENPPvIIwhoKjHcjOZgMkazyaVw1kKDuDU7nf9tjZ2r8 EoTkJiLuCnJz8pAMJDDRONqZt4KarFGb8u4xZtVjzGJ0Q25AtJYjCXLG2b6/3Twsa+U0 0bABpAHmbn6Rej15NnK1Zp8ubCwGVtU5Y1zWmWmYaQBC4/d5kE57prRfKcfW/Cb6jVb/ 5rxg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=EZ+Hm4SxeRaHZuoo9bM0zEfIlZ3DfX4WWNIZo1ncI0M=; b=Ol/j4J2eg3w38G4DTJ5QAvIBTmmoZZy+T9TdpG58+Q4KZdyea/ZuC63PIvSK57xpNp 4MzpC4xNtGU4CBHkq6R6yJe2JCH3ed8zkh6OB4Ub9U48UhXHeeoei2lxoN1ACgjvwu9T j6PcYiRh+9I0zQEtoqyhdWd+ohI3FRLndxJKa2J+LNEhyc1cAoe7TET384vMvTko39qh 4SJI08Z0qyb0HzL630rZG25wdnJGMAmbzjBNgld9RsY1HuHdVBUEBF6795GBVECjloNU Jv+5/XcnK0GEgjI7JVquod8ozt1XmBIWci68UfbR2f2wQsmF1uBhYEaPUvjCfyLNl46Z GCfw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUoEudmMWb83cqjEZEj47KCJoi/2msGCvgPvKQPlCJboYXVy+mf dcyYs6XEZ3hypIh4unpi4fc= X-Google-Smtp-Source: APXvYqzqxtxxci8powaPL1DclP8b9iE+RBoW4RbDoKdrCmgt2JIBjU012/Z7ezXDP581Afs17lpSCg== X-Received: by 2002:a67:fc45:: with SMTP id p5mr9452948vsq.179.1565275533484; Thu, 08 Aug 2019 07:45:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:8e47:: with SMTP id q68ls221521vsd.10.gmail; Thu, 08 Aug 2019 07:45:33 -0700 (PDT) X-Received: by 2002:a67:f84d:: with SMTP id b13mr10065860vsp.151.1565275533124; Thu, 08 Aug 2019 07:45:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565275533; cv=none; d=google.com; s=arc-20160816; b=K2S58cC4xjqQKvAKFQsKszDmq7RVygBdj21fPQjyivy5mlTpVOfOwADbuRNjpUFK92 9iQsbHfZTUUa0cHm6MXfG2eg65Fpa9wy9rAYHu0uw2fK3VmP4d1yp7crVxSKhVyaVPIs nUN1N4BjRaLA71ELcOB2rUzizroXnavuAFGMRZlY4/jChtgO1r3GcK4feg9+E0riRCCr yEPFZTiZGtQfHMwi196fAUzZYVO+ULBERigHmMM4HuVZNYn/IyB3nrb8Fghe+OeK/CML eEztpRIf+jF4DvoOF3uLkWqo3QoNZV0mCLbusQH8IhEK/lSsRLAfbnw/MenEBCwFS1Gz Gt2Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=3ZgLGi5mD/A9jGYP6Qywp6dGSJEEGkVG7ig2jrYmH/A=; b=Mvd/dXBbZRWUYdlfGfoeqGLTkj0p2r2xLWgi0V0jpUxIROWW3+IikhqRDq87dSamYc j49dD0M8hTHUiCggFqdpvGnS0F+lhDde/OPL2DIIOYQK9DjehraxfcBCEWaJKXwY2geX x7jsc5gBNwSFGzSqzwTcCOlpWMlvhBubEO5wOU5PpWuUCR8c7xeCDti1ag4ibgdFpFi2 JeQ9jTCuUAxbXD/wG+ifE6b9sv5jws/jqDbr3n55zBPksvkD1hjcu/y5DPnJEbYUfZFI sPbNIhvlctrEdSjawOQaXJqB2ume9EyvZYQrqZ8DrlcLCO5b2a40Kik8vH+OXTQxMlCO X4jA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="ot/5oGef"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32e as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x32e.google.com (mail-ot1-x32e.google.com. [2607:f8b0:4864:20::32e]) by gmr-mx.google.com with ESMTPS id z67si4500667vsb.1.2019.08.08.07.45.33 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 07:45:33 -0700 (PDT) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32e as permitted sender) client-ip=2607:f8b0:4864:20::32e; Received: by mail-ot1-x32e.google.com with SMTP id q20so119440997otl.0 for ; Thu, 08 Aug 2019 07:45:33 -0700 (PDT) X-Received: by 2002:a5e:de0d:: with SMTP id e13mr6091791iok.144.1565275532539; Thu, 08 Aug 2019 07:45:32 -0700 (PDT) MIME-Version: 1.0 References: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> <06e24c98-7409-4e75-88ee-a6e1bb891e1e@www.fastmail.com> In-Reply-To: From: Valery Isaev Date: Thu, 8 Aug 2019 17:44:56 +0300 Message-ID: Subject: Re: [HoTT] New theorem prover Arend is released To: Bas Spitters Cc: Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Content-Type: multipart/alternative; boundary="00000000000017c775058f9c1c45" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="ot/5oGef"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::32e as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --00000000000017c775058f9c1c45 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 : 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 =D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 15:29, Bas Spitters= : > 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 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, bu= t > 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, =D0=92=D0=B0=D0=BB=D0=B5=D1=80=D0=B8= =D0=B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 wrote: > > > Arend is a new theorem prover that have been developed at JetBrains > > > for quite some time. We are proud to > > > announce that the first version of the language was released! To lear= n > > > more about Arend, visit our site . > > > > > > Arend is based on a version of homotopy type theory that includes som= e > > > of the cubical features. In particular, it has native higher inductiv= e > > > 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 shoul= d > > > be convenient to use. That is why we also developed a plugin for > > > IntelliJ 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 au= to > > > 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 > > > . You can also learn a lo= t > > > from studying the standard library > > > . 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 w= hy > > > we implemented IntelliJ Arend > > > . 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 a= n > > > 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 . Questions, suggestions, and > > > comments 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, se= nd > > > 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-9= c22-f28261ad3b33%40googlegroups.com > < > https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9= c22-f28261ad3b33%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter > >. > > > > -- > > 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-8= 8ee-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/CAOoPQuSLoX8gKy54NQM= 6SNoi43wVA0A1Ad59qKs6prULkh6zBw%40mail.gmail.com > . > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAA520ft6xBR1fJz4N0c5NvB%2BpWD%2B14RPCu5g32cxv%2BYdbEmd0= g%40mail.gmail.com. --00000000000017c775058f9c1c45 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Yes, Arend implements the theory described in this do= cument. Semantically, the additional constructions of this theory correspon= d to the assumption that the model has a fibrant object I such that maps &l= t;id,left> : X -> X \times I have the left lifting property with resp= ect to fibrations, and the path object functor is given by (-)^I. So, the u= sual interpretation in model categories (and other similar models) of HoTT = extends to an interpretation of this theory if the model category is a Cart= esian model category.

=
Regards,
Valery Isaev


=D1=87=D1=82, 8 =D0=B0=D0=B2=D0=B3. 2019 =D0=B3. =D0=B2 15:29, B= as 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/foru= m/#!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 for= ward 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 w= hat type theory Arend implements --- I am not necessarily looking for somet= hing super precise, but it would be great to have a high-level gloss that w= ould help experts in the semantics of HoTT understand where Arend's typ= e theory lies. For instance, I can see that Arend uses an interval, but thi= s 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 math= ematics behind Arend?
>
> Nice work! And I look forward to hearing and reading more.
>
> Best,
> Jon
>
>
> On Tue, Aug 6, 2019, at 6:16 PM, =D0=92=D0=B0=D0=BB=D0=B5=D1=80=D0=B8= =D0=B9 =D0=98=D1=81=D0=B0=D0=B5=D0=B2 wrote:
> > Arend is a new theorem prover that have been developed at JetBrai= ns
> > <https://www.jetbrains.com/> for quite some time. We a= re proud to
> > announce that the first version of the language was released! To = learn
> > more about Arend, visit our site <https://arend-lang.githu= b.io/>.
> >
> > Arend is based on a version of homotopy type theory that includes= some
> > of the cubical features. In particular, it has native higher indu= ctive
> > types, including higher inductive-inductive types. It also has ot= her
> > features which are necessary for a theorem prover such as univers= e
> > polymorphism and class system. We believe that a theorem prover s= hould
> > be convenient to use. That is why we also developed a plugin for<= br> > > IntelliJ IDEA <https://www.jetbrains.com/idea/> t= hat turns it into a
> > full-fledged IDE for the Arend language. It implements many stand= ard
> > features such as syntax highlighting, completion, auto import, an= d 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):
> >=C2=A0 * Why do we need another theorem prover? We believe that a = theorem
> > prover should be convenient to use. This means that it should hav= e 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. Tha= t is
> > why Arend is based on homotopy type theory and has features such = as an
> > impredicative type of propositions and a powerful class system. > >=C2=A0 * Does Arend have tactics? Not yet, but we are working on i= t.
> >=C2=A0 * Does Arend have the canonicity property, i.e. does it eva= luate
> > 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<= br> > > twitter <https://twitter.com/ArendLang>. Questions,= suggestions, and
> > comments are welcome at google groups
> > <https://groups.google.com/forum/#!fo= rum/arend-lang>.
> >
> >=C2=A0 --
> >=C2=A0 You received this message because you are subscribed to the= Google
> > Groups "Homotopy Type Theory" group.
> >=C2=A0 To unsubscribe from this group and stop receiving emails fr= om it, send
> > an email to HomotopyTypeTheory+unsubscribe@googlegrou= ps.com.
> >=C2=A0 To view this discussion on the web visit
> > https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23= 061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com <https://groups.google.com/d/msgid/Homot= opyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com?utm_m= edium=3Demail&utm_source=3Dfooter>.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://group= s.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuSLoX8gKy54NQM6SNoi43wVA0A1Ad= 59qKs6prULkh6zBw%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAA520ft6xBR1fJz4N0c5NvB%2B= pWD%2B14RPCu5g32cxv%2BYdbEmd0g%40mail.gmail.com.
--00000000000017c775058f9c1c45--