From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBMHFZDOQKGQE6LBQ4RI@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.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73c.google.com (mail-qk1-x73c.google.com [IPv6:2607:f8b0:4864:20::73c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 214e21b0 for ; Mon, 1 Oct 2018 14:44:02 +0000 (UTC) Received: by mail-qk1-x73c.google.com with SMTP id n64-v6sf14575504qkd.10 for ; Mon, 01 Oct 2018 07:44:01 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538405040; cv=pass; d=google.com; s=arc-20160816; b=0mL8eCy5Kicnb5lM1moXNpztmw8bcNNwXKRIKnKcL4ehkLS6R6oAJ2xqIyErtz7KZu FgwJCSxE8P1OGf36BpuU0bM2k+KEIlD+Elbpr3XHO5X0LVE3odMarFXl55lqe3hPy+zy pOVoE4nK1VFGQKMvhPngJEK4j+TsVtkw3bU0fwQ11JwvRjx39z9JS38hg2fhMoQycabJ XdscOd+R9aQQKbmzPvtmLqRHPtufh2KdT9wYoEXVxSMYidiqejBOEQbTt53jfyacRkjB iMpsEdIfcIAj5CMu5qfIvaH4c878mY1Gqjiu0cxcrT/ClFBLJERV+oO+Wfkmt33jjnaV jmrw== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=wBdrT8GO1KArmYdOC246ORvrAokD57HcvhAQEPiAJCk=; b=V9R5FtLG0/jDJDA/YFZ9cLBri15D3UF921AsuIH0dFpBsaHewtqKBRTZImvb+vinkk KmAYuaubuLv86hLzG+Rn9xzY7gCJLbb8SS0WfZWFwqSZDFl/b5OdglD2bml/7uV4wDHH hc34/LR2DJ8g2vgjEwQOKZXpkGnmKfHLRhxZJV8I7nX79UejamCeCn7JbioIe5fgeYsE UKYuyKyMm4DSEOLCuRzIr79hD8H0AgB90Ik22yekO0HKCE+vRw9teHlV8TGewQaKBI/c XJTHGav9BunTHBXnlCwY7YnSrP0ULmy64cjBuu3pFTpvTv/XmWaM3qIrZzQmiL1N3b4Y TBtA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=y3SjJGMD; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b42 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=wBdrT8GO1KArmYdOC246ORvrAokD57HcvhAQEPiAJCk=; b=gizV5m/W3OhM5Jr7JoypS5KySaZKQsKtlcP0rqzjI6J2KgNPzSWeRfts+lHErCGmc0 xO7LiTVNROaBxlY1AbGmHozXjY7twviXFtZQuhk5P6Qc5l/woJHItDNrY0vx5kJmdKIv Y097eSi/7pMWh0kD7mQNEo/iMjmvgQBxoICLS6iRW4CfWKnrafrlyvPuAvy9eMuM8oWk 7ssTvnSrPY93Uw613J7CFZSKSxEkH/xfK47T4fxS3se/YF1Reppr6oZxYDALG4WmwLNz wOOea24Gpr1q+vspynpfF08PxIp/yFyE2gnETTDrl9T/LylbjOwO95lmtugezgWI/rVF 2EDw== 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:content-transfer-encoding :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=wBdrT8GO1KArmYdOC246ORvrAokD57HcvhAQEPiAJCk=; b=TaClJjSNhtJpoqlPkags83OkEIZVV8aUgXjusTrAtzF3ECy4uckVdiJkv+fXAVrZFV 6wCBKixJoRgEAS1PMY8rF/ZDdth0HePbLkJH6I5HyDWttOKOkGrzQknvHfVsW6NhHmXP y+XaPmQFvq5ebYAPmivcngz4bRZSo75hQY357dGhWUazE14oY50yIbFKYdGDoAQ5MN3i t0PXxNj552pNeIr968fnsD5sxdpOASvZeMpiVMKy8XKZmYzLWrg854BZTo2JKtZ4Rmt3 yeBBLj1qK4uaKoq953v1AOCeWubIqTXpbOCdzXNePDX1QM5J8ozq2k24UfGNnh+gK+bR tGMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfoitlh1JkhdZ9NlCpiQZNp+rck2I9lfyIZxCRMHlOSgTvaKQoGPc lb8PkFbsTDBYX4gh4t9pTPI= X-Google-Smtp-Source: ACcGV62TP8MPzsm10gUsYbS7m3OXw0GxvZWp9NaTPaoct2PiUYKTe6WBfNlUZNmZr/whEeyPM6vRxg== X-Received: by 2002:aed:364a:: with SMTP id e68-v6mr79410qtb.3.1538405040370; Mon, 01 Oct 2018 07:44:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:fd90:: with SMTP id p16-v6ls585907qvr.10.gmail; Mon, 01 Oct 2018 07:44:00 -0700 (PDT) X-Received: by 2002:a0c:91ac:: with SMTP id n41-v6mr8755527qvn.30.1538405039997; Mon, 01 Oct 2018 07:43:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538405039; cv=none; d=google.com; s=arc-20160816; b=aJ8CBDiveeeWFeNcurdta1/t113d6XKqi0vn45q+6kVdZp+Zrm4wS0Uwdo9PHE4eo6 yJhQfCp7nGDIlzb07Sp9ytie6iKIyxZFn20yFHVgM5OC3bEv/LOmz0JFZ92PgzAzmw5f 3Yh5RaV+T3/107Y6vOU9ApyI0ryZxlnRxO/+5Cvko29sTMVAlUVauXf0NdIoN5X9vkWJ QwSZ4yLGm32czsJ+u1SiOaYC5W8CdSC179ylq4j/KifU5DCFiH+uS3m4RMkLMA/PAXr9 L+Rn5VZRl6wxr5utzXJaL5lb1tupwPTvzYoLgh17epZzU0nEXPvKIxUMlVktbpe3ldFP r1XA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=nxXnJUzt/SkHnefUh7Zms25UmXkHiIHnX0wAB3/SQ9k=; b=SyfdB0E7NJA0PTHP+BybZpG1RtJA+NI8B4DJM59CK6d0m9u2UK/foa232KMKW6z1xK ruL2neOkea77gYItA5piUkxVwgAHvZ6u4EypxaCpSu1wcZqAKuDyjVZRZmCI6c1I7iXw u3eiyEom1PQE7wAdwovfMObvRh7ARmfCV1QJ13cMexVv5MFtL1oDnyWKLUeHQdJlWscG wh5RMCaOVC9y2b5mLO7+BraE8EMvOQqNzeynsZHRoxb6zx78BgAyI9KVDi3ty8X7kft8 uYly759ESCsnXgXjnACN03imh/KR61pxiOohz46gqGnazz9u9jLQfMHnIh/I5XkLRCcU RcnQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=y3SjJGMD; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b42 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb42.google.com (mail-yb1-xb42.google.com. [2607:f8b0:4864:20::b42]) by gmr-mx.google.com with ESMTPS id o3-v6si739581qkl.4.2018.10.01.07.43.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 01 Oct 2018 07:43:59 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b42 as permitted sender) client-ip=2607:f8b0:4864:20::b42; Received: by mail-yb1-xb42.google.com with SMTP id u88-v6so1375620ybi.0 for ; Mon, 01 Oct 2018 07:43:59 -0700 (PDT) X-Received: by 2002:a25:a40a:: with SMTP id f10-v6mr930990ybi.159.1538405039535; Mon, 01 Oct 2018 07:43:59 -0700 (PDT) Received: from mail-yb1-f178.google.com (mail-yb1-f178.google.com. [209.85.219.178]) by smtp.gmail.com with ESMTPSA id d128-v6sm2739291ywe.18.2018.10.01.07.43.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 01 Oct 2018 07:43:58 -0700 (PDT) Received: by mail-yb1-f178.google.com with SMTP id 5-v6so5688680ybf.3 for ; Mon, 01 Oct 2018 07:43:58 -0700 (PDT) X-Received: by 2002:a25:ba0f:: with SMTP id t15-v6mr5944478ybg.334.1538405037903; Mon, 01 Oct 2018 07:43:57 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Mon, 1 Oct 2018 07:43:46 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] the weak infinite groupoid in Simple Type Theory To: josephcmac@gmail.com Cc: "HomotopyTypeTheory@googlegroups.com" , joshua.chen@uni-bonn.de Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=y3SjJGMD; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b42 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Simple type theory also has topological / homotopical models, but less of the structure is visible to them. If you think of the types as topological spaces up to homeomorphism, then you get something approaching "synthetic topology", where the "predicates" can be (depending on the rules) either injective continuous functions or subspace embeddings. (Note that this approach is incompatible with classical logic, which I believe is built into Isabelle/HOL.) If you think of the types as spaces up to homotopy, then you get sort of a truncated version of HoTT, where the predicates are unions of connected components, and in which probably not very much that's actually homotopical can be said without dependent types. On Fri, Sep 28, 2018 at 1:28 PM Jos=C3=A9 Manuel Rodriguez Caballero wrote: > > 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 languag= e theory, but I am a beginner with respect to the theory behind proof assis= tants. > > I watched some lectures of Voevodsky using topological reasoning in homot= opy type theory, e.g., talking about the homotopy fiber and drawing some pi= ctures. I like the topological language, because I am mathematician rather = than computer scientist. So, it would be wonderful for me to use topologica= l language and maybe topological intuition when I am programming in Isabell= e/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 un= ivalent 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. >> > >> > HoTT is traditionally developed in CiC, whereas UniMath is tradition= ally 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 groupoid, of Si= mple Type Theory (the type theory behind Isabelle/HOL) and how it becomes i= somorphic to HoTT by means of the axiomatization (maybe there is some topol= ogical intuition related to this transformation, cutting and pasting). >> > >> > 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= "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.