From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBBVU5XLOQKGQELO2O6HA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 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-qt1-x83e.google.com (mail-qt1-x83e.google.com [IPv6:2607:f8b0:4864:20::83e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c7a2c537 for ; Fri, 28 Sep 2018 20:28:07 +0000 (UTC) Received: by mail-qt1-x83e.google.com with SMTP id i11-v6sf5509790qtm.5 for ; Fri, 28 Sep 2018 13:28:06 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538166486; cv=pass; d=google.com; s=arc-20160816; b=0N2DEu0+6MhCEAd/gXeBiQ4XBNv+SyhOaqpk4VTtMXRpnKbDYzBEdqdqyZtATmF0qJ 3wJBs6gFctSg1fpXk2DeMfMpfX2dSRShx3zSymMIteJrMcwaZ4g9CKY5siLctQIbne6f 7HKYcamLZct0I3xz+XJ9XDCQRTC5hBA03wHW2D9+Ku8s62b7NBk8qqeqM3fWSJJYIXnG 7JfUMgLGeUhrY3iZUm1ofkSuoIfXEeSgoUp3HWLv59BCvFsYV/CzsHEoeR8/IfClyude JMU3BLQjY6huZXUcsZVJCdEnQegrISV4Vof1IXdNvbDYLOI+JYOyVSxrlExJ2NglhLrf Raqw== 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=bey7qswxDXOaVTbpPDDtfReBUpkjF3NNRkIDVN/AYQY=; b=CZS5hIKj3dKNyjdTFuAECwEWRexg/SbLEX4FclFEFbwiLmm2HiUegx1FjMkFzdufdl EaKKggE3t4QJjslHaMV3ank8bKWCvY6X9Pfx6fuKB2YQvf8j30shkP06+dOAtLq+dvvl bhCJ7HBv6gHWIwhqwomhSHKh2D/FJx2Izfs6qiSSEt6BhhKDRfsPhXpmRyLxWXHJ0XrV AVQ3J6ubhsyVRyENZzz5weed2AJOtRE31aZ9DSnCFQl17cvFcznVCwvzYfrE9uXQADcj UW/FsV3/wxsGwy37bztjp3OLuZzc2XKMBYU9JVcEDbrv4tIiPXrTRioj5IE9Uxi1rFR0 k5bQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ME5HwL8V; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=josephcmac@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=bey7qswxDXOaVTbpPDDtfReBUpkjF3NNRkIDVN/AYQY=; b=kEIuOOxLoCOSM1goatfKoWpg7/joU31sHydkgGEPTEVUXCgLhU3q8nEI6IaH/6Oocu Uu31GJd/Nh+4sC4xYecbTBflC3egVxqxBiFoFXV7YbrDBXAt5Aw8FtGxIqsK0yguintD ODO/AacPF8zL3QOJKJe7Y24EcL0q81v0V5Pecxn93f++zh0fYd+wcgVujhbS//SNFBLK +882fXCqR8uD15gYYU4H6a7kizuZkAMb3dAldR/PTPcr8O/rHFtwXvFKbTugScB5iDDs AmakPEJ2LQydx54L1nfKJXB1Jc5cMSP6xPGUspgmyY+UYOGu+fMyxT7PZ6AgIQZMVMya DBxQ== 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=bey7qswxDXOaVTbpPDDtfReBUpkjF3NNRkIDVN/AYQY=; b=pFzu82VFJIHe6nJbFdli6ZdppBf6AChuOpwwo/HTVP6LKK5T0LItv012LxG5FZp6mu ZNbvuVPi+Q9OQjwTmfNwu84Q5MXlU26Y4rmLlOa9oMkZdXuWqohCF1POLnJaWizXmWEH hjN+pYg7zJKQ9TOMA6I0ZBgxFnPpvQ9SwPTH2WFr4VuRmVtME95TxjKT4e0MAmoPDbFj 3HTmQcsmI84X+T4OBEt0PSRXp4Df3ENUUMjBkq7tR/D0vyO6H/FxIcXihxXavvjG9wQQ QqhN/8L7CJJMNyKi7bcZ0T4EEVgIqaROKF4Yb9gSvfpd6TrXRmUqyAOR3BLQOvEjpmYa 8n+Q== 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=bey7qswxDXOaVTbpPDDtfReBUpkjF3NNRkIDVN/AYQY=; b=XdITV5wKv8KPhun63rXnvpbDG6dDQz2PIBIWI47imNk1VZbvwDU7zBatoi57zkkG3R ySBvc/DQCQxbLfoj5BIlTefLAb6gHMWB8IMy/8p+4YRP0M7llPp7loF7w8d2jvPBZcBk IuUmvJTsQiYEk9W6wb4XXJTazUJhADGY3dSM2/4tCtKnX7PWKMXFJ/74+UOlrswA4tXN 9RDhUtOr0IoypBqDylyXrmvmI6IdeYYOFK2OSspbnWVodr9lpxTbcWOJjN2B5sIrMho/ 0yuA7/kuDS5vwU84QlenrsY8Oo+0uxweDQggdQHAdtKwKkf/GmATfmKBDIVHNkoMAOa+ g8Lg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogwl0mCQ/A6weGwoLeNIVD4Z1gRKmsBO85PhevRAJES77qJrK/W RKzfUyvdwqVY6XDdZEAWe/E= X-Google-Smtp-Source: ACcGV61Y+KmxEl7T7RVPLDciXzQpYvcQztmQXoIMY06ZJHxPe083/cQ2fXlnVeESpqhl3L0BnEU96w== X-Received: by 2002:a37:171b:: with SMTP id i27-v6mr2249qkh.1.1538166486141; Fri, 28 Sep 2018 13:28:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:f782:: with SMTP id s2-v6ls3082659qvn.9.gmail; Fri, 28 Sep 2018 13:28:05 -0700 (PDT) X-Received: by 2002:a0c:8b48:: with SMTP id d8-v6mr201461qvc.3.1538166485903; Fri, 28 Sep 2018 13:28:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538166485; cv=none; d=google.com; s=arc-20160816; b=PancKcGeVmaMJQ/K1Mi/QTTIlOB0XWsBokEoY3k0cc+qRAjnX4WymR9KXdRLM2ApSC hxMtFnwII4MsxEWIaISrNUkmnq0wMo+3L2JeOMCh7PlpSkunN1cnmmRusZ9KZqL1/Jf/ t4zWFdHJPvkyieG6/GafPkNX0VxqW1RiEjsZfbg6sR5ZhxeKjBgg6BtKqEoQ28sPneOW anpkelzLrH6Yf72EY0kwafMTybhepTeNFG6KrRciSRvR2VEzMv0K5uqou6lUDWGQlhuE MVwKVqR8mF3h9DXA60S/qiweazN5hQBnQ5BMuVI+6aFC/mJXX4h1sDxocMp1nEdRBm1w gUSA== 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=vemVA/v5m5CgLJjDGvW/2ICHvgF8VXR0oZJDIO89T5s=; b=aiptrLON/N09kUurZIlL+kzInQ5SPb84P9ZfOYFAwLPegxyjHTDphTna+/B+FXd/P+ giPhaHF2viw2GlPI8/eoNIHPayueWAFSUQaKOPSAM/zCdAjTzrFILAVuPXaEQlak61j6 Q8mzGM4On+CE6MEBGMlTvx3TY7NJMGLer8yJiyqb/0GaUeeeuRek56iw2Hb2e/337oTp Ifxm1cp+S06ATQsncIBcuYu/n/HMWI7Sf7rWWu1P1jYeegBjHshTdmBn10IwOT5KqP6V gTMzhQxSr33Rq6d+CT0zmQWvfTZH27JTIwmSHTRXX/Gze16ub3QcmNno1CJfQ8L/dQcx +cKg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ME5HwL8V; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x129.google.com (mail-it1-x129.google.com. [2607:f8b0:4864:20::129]) by gmr-mx.google.com with ESMTPS id x41-v6si96971qth.2.2018.09.28.13.28.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 28 Sep 2018 13:28:05 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) client-ip=2607:f8b0:4864:20::129; Received: by mail-it1-x129.google.com with SMTP id w200-v6so4233523itc.4 for ; Fri, 28 Sep 2018 13:28:05 -0700 (PDT) X-Received: by 2002:a02:4f89:: with SMTP id r9-v6mr294632jad.6.1538166485126; Fri, 28 Sep 2018 13:28:05 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> In-Reply-To: From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Fri, 28 Sep 2018 16:27:54 -0400 Message-ID: Subject: Re: [HoTT] the weak infinite groupoid in Simple Type Theory To: HomotopyTypeTheory@googlegroups.com Cc: Joshua Chen Content-Type: multipart/alternative; boundary="000000000000f3989a0576f44a38" X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ME5HwL8V; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=josephcmac@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: , --000000000000f3989a0576f44a38 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Mike, Thank you for the elucidation with respect to my confusions concerning type theory and proof assistants. I use Isabelle/HOL in a practical way in order to formalize my own mathematical results in number theory and language theory, but I am a beginner with respect to the theory behind proof assistants. I watched some lectures of Voevodsky using topological reasoning in homotopy type theory, e.g., talking about the homotopy fiber and drawing some pictures. I like the topological language, because I am mathematician rather than computer scientist. So, it would be wonderful for me to use topological language and maybe topological intuition when I am programming in Isabelle/HOL (simple type theory). But I am not sure if this is possible= . Kind Regards, Jose M. El vie., 28 sept. 2018 a las 15:21, Michael Shulman (= ) escribi=C3=B3: > It sounds like there are several misconceptions here. > > Firstly, many different type theories are used in the subject of > homotopy type theory, but CiC is not really one of them. In addition > to inductive types, CiC is distinguished by a primitive impredicative > universe of propositions, whereas (almost?) all work in HoTT instead > defines the "propositions" to be the homotopy (-1)-types. Coq is a > proof assistant that implements CiC, and Coq is also often used to > formalize HoTT -- but only by ignoring the universe Prop (indeed, we > had to get the Coq developers to implement a special flag for HoTT to > *enable* us to ignore Prop). So even though HoTT is often formalized > in Coq, I think it's misleading to say that CiC is so used. UniMath > is a particular library which formalizes a particular approach to HoTT > in Coq, using roughly only the MLTT core plus univalence; other > libraries for Coq in HoTT also use inductive types and axioms for > HITs. > > Secondly, I expect you probably know this even better than I do, but > Isabelle (or Isabelle/Pure) is distinct from Isabelle/HOL: > Isabelle/Pure is a "logical framework" in which one can specify and > work with many different object theories, of which HOL is only one. > It appears that Josh's development is such a theory, so rather than > "HoTT in Isabelle/HOL" it is "HoTT in Isabelle/Pure", or one might say > "Isabelle/HoTT" -- it's not really related at all to Isabelle/HOL > except that they are both formalized in the same logical framework. > > Finally, specifying HoTT inside of a logical framework does not make > the logical framework "isomorphic" to HoTT (I'm not even sure what > that would mean), nor does it directly give a topological or > higher-groupoidal interpretation of the framework. In particular, > Josh's Isabelle encoding of HoTT is (like the earlier encoding > Isabelle/CTT of an extensional dependent type theory, > https://isabelle.in.tum.de/dist/library/CTT/index.html) what some > LF-theorists call "synthetic" > (https://ncatlab.org/nlab/show/logical+framework#Synthetic), which > means that it is an encoding of the *untyped syntax* together with the > typing judgments. So I think it is not very different, from a > semantic perspective, from formulating the syntax of HoTT inside, say, > ZFC; in particular it doesn't imply any relationship between the > semantics of the object-language and the meta-language. (The > advantage of a logical framework like Isabelle/Pure over ZFC for this > purpose is the availability of higher-order abstract syntax to > represent variable binding.) > > If one uses a logical framework "analytically" instead > (https://ncatlab.org/nlab/show/logical+framework#Analytic), then there > can be a closer connection between the semantics of the framework and > the object language. However, I believe that such an encoding of a > *dependent* type theory is only possible in a framework that is also > dependently typed, unlike Isabelle. > > I hope this helps answer your questions; if I misunderstood what you > were asking, please ask again! > > Mike > > On Thu, Sep 27, 2018 at 10:59 PM Jos=C3=A9 Manuel Rodriguez Caballero > wrote: > > > > Recently a user of Isabelle provided his version of HoTT here: > https://github.com/jaycech3n/Isabelle-HoTT > > > > A brief description from the author: > > > >> Joshua: > >> This logic implements intensional Martin-L=C3=B6f type theory with uni= valent > cumulative Russell-style universes, and is > >> polymorphic. > > > > > > This version of HoTT involves some axiomatization in addition to > univalence, e.g., Sum.thy and Prod.thy. > > > > HoTT is traditionally developed in CiC, whereas UniMath is > traditionally developed in the Martin-L=C3=B6f type theory (as part of Ci= C in > Coq). As a user of Isabelle/HOL, interested in homotopy type theory, I > would like to know the topological interpretation, as a weak infinite > groupoid, of Simple Type Theory (the type theory behind Isabelle/HOL) and > how it becomes isomorphic to HoTT by means of the axiomatization (maybe > there is some topological intuition related to this transformation, cutti= ng > and pasting). > > > > Thank you in advance, > > Jos=C3=A9 M. > > > > > > -- > > 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. > --=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. For more options, visit https://groups.google.com/d/optout. --000000000000f3989a0576f44a38 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Mike,
=C2=A0 Thank you for the= =C2=A0elucidation with respect to my confusions concerning type theory and = proof assistants. I use Isabelle/HOL in a practical way in order to formali= ze my own mathematical results in number theory and language theory, but I = am a beginner with respect to the theory behind proof assistants.

I watched some lectures of Voevodsky using topological reas= oning in homotopy type theory, e.g., talking about the homotopy fiber and d= rawing some pictures. I like the topological language, because I am mathema= tician rather than computer scientist. So, it would be wonderful for me to = use topological language and maybe topological intuition when I am programm= ing in Isabelle/HOL (simple type theory). But I am not sure if this is poss= ible.

Kind Regards,
Jose M.


El vie., 28 sept. 2018 a las 15:21, Michael Shulman (<shulman@sandiego.edu= >) escribi=C3=B3:
It sounds like= there are several misconceptions here.

Firstly, many different type theories are used in the subject of
homotopy type theory, but CiC is not really one of them.=C2=A0 In addition<= br> to inductive types, CiC is distinguished by a primitive impredicative
universe of propositions, whereas (almost?) all work in HoTT instead
defines the "propositions" to be the homotopy (-1)-types.=C2=A0 C= oq is a
proof assistant that implements CiC, and Coq is also often used to
formalize HoTT -- but only by ignoring the universe Prop (indeed, we
had to get the Coq developers to implement a special flag for HoTT to
*enable* us to ignore Prop).=C2=A0 So even though HoTT is often formalized<= br> in Coq, I think it's misleading to say that CiC is so used.=C2=A0 UniMa= th
is a particular library which formalizes a particular approach to HoTT
in Coq, using roughly only the MLTT core plus univalence; other
libraries for Coq in HoTT also use inductive types and axioms for
HITs.

Secondly, I expect you probably know this even better than I do, but
Isabelle (or Isabelle/Pure) is distinct from Isabelle/HOL:
Isabelle/Pure is a "logical framework" in which one can specify a= nd
work with many different object theories, of which HOL is only one.
It appears that Josh's development is such a theory, so rather than
"HoTT in Isabelle/HOL" it is "HoTT in Isabelle/Pure", o= r one might say
"Isabelle/HoTT" -- it's not really related at all to Isabelle= /HOL
except that they are both formalized in the same logical framework.

Finally, specifying HoTT inside of a logical framework does not make
the logical framework "isomorphic" to HoTT (I'm not even sure= what
that would mean), nor does it directly give a topological or
higher-groupoidal interpretation of the framework.=C2=A0 In particular,
Josh's Isabelle encoding of HoTT is (like the earlier encoding
Isabelle/CTT of an extensional dependent type theory,
https://isabelle.in.tum.de/dist/library/CTT/in= dex.html) what some
LF-theorists call "synthetic"
(https://ncatlab.org/nlab/show/logical+fra= mework#Synthetic), which
means that it is an encoding of the *untyped syntax* together with the
typing judgments.=C2=A0 So I think it is not very different, from a
semantic perspective, from formulating the syntax of HoTT inside, say,
ZFC; in particular it doesn't imply any relationship between the
semantics of the object-language and the meta-language.=C2=A0 (The
advantage of a logical framework like Isabelle/Pure over ZFC for this
purpose is the availability of higher-order abstract syntax to
represent variable binding.)

If one uses a logical framework "analytically" instead
(https://ncatlab.org/nlab/show/logical+fra= mework#Analytic), then there
can be a closer connection between the semantics of the framework and
the object language.=C2=A0 However, I believe that such an encoding of a *dependent* type theory is only possible in a framework that is also
dependently typed, unlike Isabelle.

I hope this helps answer your questions; if I misunderstood what you
were asking, please ask again!

Mike

On Thu, Sep 27, 2018 at 10:59 PM Jos=C3=A9 Manuel Rodriguez Caballero
<josephcmac@gm= ail.com> wrote:
>
>=C2=A0 =C2=A0Recently a user of Isabelle provided his version of HoTT h= ere: https://github.com/jaycech3n/Isabelle-HoTT
>
>=C2=A0 =C2=A0A brief description from the author:
>
>> Joshua:
>> This logic implements intensional Martin-L=C3=B6f type theory with= univalent cumulative Russell-style universes, and is
>> polymorphic.
>
>
> This version of HoTT involves some axiomatization in addition to univa= lence, e.g., Sum.thy and Prod.thy.
>
>=C2=A0 =C2=A0HoTT is traditionally developed in CiC, whereas UniMath is= traditionally developed in the Martin-L=C3=B6f type theory (as part of CiC= in Coq). As a user of Isabelle/HOL, interested in homotopy type theory, I = would like to know the topological interpretation, as a weak infinite group= oid, of Simple Type Theory (the type theory behind Isabelle/HOL) and how it= becomes isomorphic to HoTT by means of the axiomatization (maybe there is = some topological intuition related to this transformation, cutting and past= ing).
>
> Thank you in advance,
> Jos=C3=A9 M.
>
>
> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

--
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.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000f3989a0576f44a38--