From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBSH6XHOQKGQEZDE6A2A@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 autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qt1-x837.google.com (mail-qt1-x837.google.com [IPv6:2607:f8b0:4864:20::837]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 117e71f7 for ; Fri, 28 Sep 2018 19:21:46 +0000 (UTC) Received: by mail-qt1-x837.google.com with SMTP id a15-v6sf6593756qtj.15 for ; Fri, 28 Sep 2018 12:21:46 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538162505; cv=pass; d=google.com; s=arc-20160816; b=PdxHMNuCPGJd0sWGsWevy3B3f+aIAqDFJzRhHu/CNpvw0KrqBzBfCrVUeTsKzBaEeE OAcRf9KIqTxNSQ+J7SGRKom03nPvZD/9yhfp9rknHP/CXCsJb0DV5oqIH7IT8wcrsG2Q 6yg8KWgKMWWmvtskP9T1JeDuAJ/y03kvLJg00Y7qRzLDL41+5FaFBfqRllRsNFYKrFmv LybDImZyrQzDD3yFPpDvSzfAwIyk4UUU353OHlP15GU7zI0cLCmHfu9pyR97D8blfYMg kSQfvdxGNveGZN0GSSE5cm7QyZzl+qxyKwBlfrGfnrIj1PoyGulJIaYjkaQ/3GFvXPwg q55g== 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=p42GtzaVJVMQrzcqL9kZh6fXHoyOqBqBJMpY6OihcX4=; b=SXwYSoTG9TjB5MYC1KQxNZQD+WETjF7W5/0jwqWWj+/2X1gyUs4zZZHKmbOSyCQttF 0EeYgywgrfQ1saEsrUoertOMdrr+Y4V7RaovovIyofW+nu0SsdpHjtn4CkMnGFX8PPjg 0j7xm4vMfbrLg/PHgZvfnEprGR57Wtr5lKef/xDf+xQBh9szTPVC+EWhvt0j0yJBP58q dub0xhYpcLG3gHzdNwblQSflrJM8Ge1sn8IvIpY4zMVYdcCiXRWhW4oLfo+HkyCzYOmf ZautGRsVxngR3fr3e4UiXsOtrl8n3x1QMV6+Fvg617lN3UDTmNNL6XRsb+w3rTHpKjBB 4Scw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=2RRXSrgq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2e 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=p42GtzaVJVMQrzcqL9kZh6fXHoyOqBqBJMpY6OihcX4=; b=Ahw/4AWB2u1EE5wl64ybNicHjMNZLlo5gAgKZpWjnEcVqzOwpJmSPQubBIY4teV++2 XLyoz7MTHglL1ud8lCDllWQMxvfahFtqm/QvV3LASprND45CWt4LtxEHIoY/FyMyElAe 3dAQ7QTliqJczlTWGMUKmaqPduZ6uOnj5pBY3/yfyqmE4slCb83ENt1upIYJu6i/1f8x QSk6pzhhuHFxwP9S0SB+Z0aq/WtMjxvaHRERfsYL5a1Yz5mRZHxwuCmBcZZZkHDH2JNf 8oJ7z2ftjGMYDYWgbk9kAOOQkjoH4ds3/jieZZaoqqqpGAZCjF064zEorwnwxHjlNIdO oNaQ== 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=p42GtzaVJVMQrzcqL9kZh6fXHoyOqBqBJMpY6OihcX4=; b=l7TisGdFrp691zI2RDAxiHrJ5DQDEOFKvk0PxQ1NIPPb6SvxxS8BKxe81Ak7iTs7XX asV3ezcEmdzFIzlXEEkGTxG9RtodBJMRxpH/ZD7H1XdqfqhslTecJQ014MtjqYz5swi6 OqmvGb5WL3xHFDew4kSMo5Ic1t2JQcXDBlQYjyfkVcrJiamclKrUWJBIO2Hyshr69Idk 8lPYAuH/y5Ncy/dU+cW+c7LeRXHQcFAq0JF99QVl96VoIwrawQNlQEkK8ilSe86SGAA+ hOH5nGS8Iox8ZadmOXJrm5IE60I4zJK1804FsgnPWUPeQ8rAVE1FAcJiwMqku1jBZdZR Lt5g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogQUkkfTngoXqx3yVapPG7NuUw/lT8gKEPbSnlMPKKquAysxE8S /GCOwf77MrzKia5NlqBImXk= X-Google-Smtp-Source: ACcGV60bsr6xzqNQFqvtgFTRhpLYHjy3IwF4AZhakBqS+NV/fpydoPA2swmAkgs1eKhTZ0DSIcI9Kw== X-Received: by 2002:a37:851:: with SMTP id 78-v6mr826qki.0.1538162504934; Fri, 28 Sep 2018 12:21:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:6105:: with SMTP id v5-v6ls2732680qkb.13.gmail; Fri, 28 Sep 2018 12:21:44 -0700 (PDT) X-Received: by 2002:a37:a50b:: with SMTP id o11-v6mr30878qke.30.1538162504665; Fri, 28 Sep 2018 12:21:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538162504; cv=none; d=google.com; s=arc-20160816; b=hKPNAfvtaPUoWU3jK34u4u1qbWK1lX1b0QU+okgdVY2YF9ALb9inWa1fFSRBYRiw/I p6QUDWbLwNAa4cimtzdkPFDX9djPBXTbqN30htwp37VqzJE8HHOFtgo6bM1rBy6gNTC9 veypwB4M3tQFWSPhdtHQz/E3NRhusjOo7iJa4JizbwKxUpHCBT70H5n18YcWETeaxZOu QfBOMoU04JuQ+/ERmw27xJMHazYSqbsOUia3JYaHadxDFYTcL5Z4bAhAP6PE1TNvDxZg ZmPrYETloRtBP8ErvvKcwbIiiweD+Q5WBSaj71B4+y+ZQ5Hnjy47KmVdgp1+MiI7OKQt 3TpA== 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=DOr+YyqzNs7ROCJU45AidXE1fTP1OX+g5eZKeg7c1Y8=; b=jIl8sXuOT8JP/aqIGJMljTsXQ6YEaIWbPkkCjUm49Cv03qUy8ate0rCTK7tT6/JbSx kk2f/xUUJVyrJYWYXQEWLCqYD+E2ACTESfCgTOC2Vkmpu2Zpzm1DL/MronNSWi+R03UR BTDvspJzUCiXpVcJ6yNvLKx2AuogY6kLNrV+4P0Ec4e4d6jrLPmKyuv7oNltC2pj5e/N 7B90Z7uLKGDbFmkedhoNF1Ry4Q21Ktoi/P9mEXt3lNQI7PMIe/LCVyUsq5TBHDN+qYOU OHJghZ2897EVKMxeHfpx/Re5hkBs/jMiT8SCSdpDThl1m/0JDtDB61Qa3ygMN5WeGL9o speA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=2RRXSrgq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2e as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2e.google.com (mail-yb1-xb2e.google.com. [2607:f8b0:4864:20::b2e]) by gmr-mx.google.com with ESMTPS id o3-v6si346375qkl.4.2018.09.28.12.21.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 28 Sep 2018 12:21:44 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2e as permitted sender) client-ip=2607:f8b0:4864:20::b2e; Received: by mail-yb1-xb2e.google.com with SMTP id o8-v6so3095785ybk.13 for ; Fri, 28 Sep 2018 12:21:44 -0700 (PDT) X-Received: by 2002:a25:390d:: with SMTP id g13-v6mr57631yba.88.1538162504222; Fri, 28 Sep 2018 12:21:44 -0700 (PDT) Received: from mail-yw1-f41.google.com (mail-yw1-f41.google.com. [209.85.161.41]) by smtp.gmail.com with ESMTPSA id z20-v6sm7731912ywz.75.2018.09.28.12.21.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 28 Sep 2018 12:21:43 -0700 (PDT) Received: by mail-yw1-f41.google.com with SMTP id v1-v6so3093052ywv.6 for ; Fri, 28 Sep 2018 12:21:43 -0700 (PDT) X-Received: by 2002:a81:6846:: with SMTP id d67-v6mr15129ywc.189.1538162503294; Fri, 28 Sep 2018 12:21:43 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Fri, 28 Sep 2018 12:21:31 -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=2RRXSrgq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2e 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: , 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 univa= lent cumulative Russell-style universes, and is >> polymorphic. > > > This version of HoTT involves some axiomatization in addition to univalen= ce, e.g., Sum.thy and Prod.thy. > > HoTT is traditionally developed in CiC, whereas UniMath is traditionall= y 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 Simpl= e Type Theory (the type theory behind Isabelle/HOL) and how it becomes isom= orphic to HoTT by means of the axiomatization (maybe there is some topologi= cal 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 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.