From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBUFVZ3OQKGQE4XMDSIA@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=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-yw1-xc40.google.com (mail-yw1-xc40.google.com [IPv6:2607:f8b0:4864:20::c40]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3d1a8910 for ; Tue, 2 Oct 2018 16:20:34 +0000 (UTC) Received: by mail-yw1-xc40.google.com with SMTP id b70-v6sf604561ywh.3 for ; Tue, 02 Oct 2018 09:20:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538497232; cv=pass; d=google.com; s=arc-20160816; b=q/p9yfrL76M4UVdnIRtOYndzgR/bS+I8Lx3MGie9KcKfoXoz7/wtV1UM7Z7wnXENRu K03PRj4imKACH+p+XFEOjGLTFAVL1pKWnm+yxvf9ZTelyeD+uWE+7mveOGrtyPbSm6fD 0ZkKO++1sGK7b9YAfWngRX8yD5MbumDxK1rKBJHkqBazj9ZObhE4FOLevxQjoNutUheC Izt5IB+mvv1FM/E+cgrRvn/TdLMvE5htIRfSkQKslrjuxLhqmwhHhR72R+E6K5B910Af 9wExDKR+6ITVyhFovPa4nXkfei0cQDPbyc08LB9R9Dw5YTsHvNurMUHgDJMurXPC5aNW o9FA== 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=Zs6ib+U5mowSgX7u+P8CDJABG1Z/qs0JFuJc70Tl6TQ=; b=hg6V2jJg1LGLQjz4GADJfpTuF4/dnK9VKgxWQPIlpd6wRt4RKyKOOb2Fq5ndnartfJ leJ5Wm2wSxTkz0LDJYbAjlAo82PwMHg8kWa6Nif8ioRmsu8zRYJmL6TdIA2btdAaE7Vy McCjzhVHCJSimAuqY3CsnAgLnuMb0CXa2McFpxOviNkWBGlU/HiiM1ZJqvPQjU5yp6Ra hVcG8uj5/rjw1ENsLiuVIyYnH94rofV0b7v9oSLPzoQXJmS4lhwgKHH0RLOgTETIuyCv PEGhhcEQbCUGITSaxOquI39gh7ubFAnbq6sWapksFkfd7+vuVu9GPT9Ajf6B2ll3MRmy /qgQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=wPC+pOh4; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a 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=Zs6ib+U5mowSgX7u+P8CDJABG1Z/qs0JFuJc70Tl6TQ=; b=PvDrAANTANNukJjy+f/vVrBwMi52wo9DNClHLYI4FLCqKe6oWxD+W7Uss7nhCZ5HfP mVnl8MbbMOfF8FEH7bb1QAAOrFZWUzsSNUbc2mssSB6W6keQKTwu54mrjggOpNG+jUu+ iUV6yVbyPqMIUhUWVMr7I0rEQDSFPYRTcPz8pSSNscRDALnTWHieRYwILk5t+MO/zHcw 4BSOV8w2i3xCsem4Lf+XcYSmBhtxdS3sQPNfyUsiEeFxHSHKBmHWvFmY6kErZtsSlR0Y dGRAJEq/enuWWy6TsVadFB18MixBQ3iBnVazsoLf2W1j8KXAY2sFmIU5XNo0hZxwW5VP A8bA== 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=Zs6ib+U5mowSgX7u+P8CDJABG1Z/qs0JFuJc70Tl6TQ=; b=RB9PV73O7jDk1tuye398ajGJu303sYsM3gdlKzsuM3Vj+nbQGHwhF6qcFjJez3AhGb 4lriEh5X7aL8hw+UZArcMVuMN0dO72CJ0ymANwek6gyzI7Dzif3vHBG6MOLmvwx6SLxQ 02kE8Z0Oj8N+W5UXST8mnRmhKxMA8yKqEX9irXnlu+InNy6JK8eYJFiGN0jT5hc5yjSX cJjpbgxJoMjgQG712oaKYpwhSXh/s/iyrcx3DbYpeFAHcl+HM5us6N4WxWBzqhv/u734 5wH5alfty5qMfw7ApYjLXpAcRlwOKy3jOSMTK+w3fCGeBjbIcM/xsIcbO/1O267SX/u9 xyUQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogTwqxkJ4DQZkNce3seW9Tt6vnfdKHZ5d7uI7jZtmkTW9mqjI6t XHYkDupuU9j7K9nbncoRC8U= X-Google-Smtp-Source: ACcGV62NULvXUzxqAxd81X6nw7Re2h9CyL4YHxYsT8lXN3c/J2dkCH5VFthMDVJpi5aAJMIlkkgSrw== X-Received: by 2002:a25:50c7:: with SMTP id e190-v6mr196924ybb.1.1538497232674; Tue, 02 Oct 2018 09:20:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:5502:: with SMTP id j2-v6ls4706310ybb.7.gmail; Tue, 02 Oct 2018 09:20:32 -0700 (PDT) X-Received: by 2002:a5b:408:: with SMTP id m8-v6mr9129512ybp.63.1538497232354; Tue, 02 Oct 2018 09:20:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538497232; cv=none; d=google.com; s=arc-20160816; b=JvO0KC9p1ow0AR3KWG5KM4CTFNtt2c+R1FVdQxrJ+1AZ7AXKCTc0GtgIHBx7kldZLG 55Vy45TdEKKjQJZXXin8DMoQdezAU1qOSz1B3fYyJqQMak3MUe+2pMLq2I0+9cVBHktW 8XRc6XITkUDPc9LslyJLaxeIiDYIqLykUws2TO5lN3JbeghT6A3dEs8H2Bo1XNM70v4C 7WmXlogeDpz7w/fcY7t4wQ0nf4f7CYNBKi7dB9t7KUH5DL4pWwiGG64DCwn+5+LbAsqJ G9BiStteYp97lFlNi9kiELrtGgpErJqQNRChTTVgceomtU06qSDgHM4GsusY7olGVN81 kyJQ== 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=Ewwt7Rb8emLGBdVuNqSkUw2LQqJKeJlrUscGpxI1ns8=; b=E8QyqJniL1nE52rVAkMcJSIFmOFZhLQnto23208Pmh7lgHiu3rTNgj0CoRh3QxV+Ns 01ece4/8/v6G7D/F6dipnktkA8YsrLcerSvtX9xgC0QeETNofxEeCW3AHkCM0jfQScOi ulTvpX1Eko9WnM54WH8eenXiOsYFyiTF9nAXp1UMe7Y8BjB4Vt2rHQCZaEsvuAVlFBda Z/y2vIyijBLm8ccZ1EEySwD94bpvqVGs+eqL+kRGD28XNHFpmp2WJJPd7eW9pnij6yuS nacv/Eug3N6UiBBqvhxhyof/eZgFiox7L6OutO/CBvMyBk2nubhSUWq51S0Uyl2SzJSs Kolg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=wPC+pOh4; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id f77-v6si839073yba.5.2018.10.02.09.20.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 Oct 2018 09:20:32 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id x5-v6so1010798ybl.11 for ; Tue, 02 Oct 2018 09:20:32 -0700 (PDT) X-Received: by 2002:a25:c2:: with SMTP id 185-v6mr8876146yba.451.1538497231863; Tue, 02 Oct 2018 09:20:31 -0700 (PDT) Received: from mail-yb1-f182.google.com (mail-yb1-f182.google.com. [209.85.219.182]) by smtp.gmail.com with ESMTPSA id f5-v6sm6679644ywa.39.2018.10.02.09.20.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 Oct 2018 09:20:30 -0700 (PDT) Received: by mail-yb1-f182.google.com with SMTP id p74-v6so1016740ybc.9 for ; Tue, 02 Oct 2018 09:20:30 -0700 (PDT) X-Received: by 2002:a25:ba0f:: with SMTP id t15-v6mr8906973ybg.334.1538497230237; Tue, 02 Oct 2018 09:20:30 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> <6535A055-1DC4-42AD-A0EB-37B1D523ECA1@cmu.edu> In-Reply-To: From: Michael Shulman Date: Tue, 2 Oct 2018 09:20:18 -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=wPC+pOh4; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a 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: , These lemmas are just standard facts of set-level mathematics; nothing fancy or univalent is required to formalize them in HoTT. If you replace the equivalences by equalities, then that would be using univalence. On Mon, Oct 1, 2018 at 4:15 PM Jos=C3=A9 Manuel Rodriguez Caballero wrote: >> >> Mike wrote: >> 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. > > > Indeed, I think that the lemma > > lemma card_permutations: > assumes "card S =3D n" > and "finite S" > shows "card {p. p permutes S} =3D fact n" > > in HOL/Library/Permutations.thy > > is a truncation of the following theorem due to Voevodsky > > Theorem weqfromweqstntostn ( n : nat ) : ( (=E2=9F=A6n=E2=9F=A7) =E2=89= =83 (=E2=9F=A6n=E2=9F=A7) ) =E2=89=83 =E2=9F=A6factorial n=E2=9F=A7. > > which can be found here: https://github.com/UniMath/UniMath/blob/master/U= niMath/Combinatorics/StandardFiniteSets.v > > By the way, I do not know if the project of developing combinatorics from= homotopy type theory, started by Voevodsky, continues today or if it stopp= ed. > > Kind Regards, > Jos=C3=A9 M. > > > El lun., 1 oct. 2018 a las 10:53, Steve Awodey () escribi= =C3=B3: >> >> of course, there are also topological models of simple type theory resp.= HOL, and extensional MLTT, which are then not homotopical. >> See e.g.: >> >> https://arxiv.org/abs/math/9707206 >> >> Steve >> >> On Oct 1, 2018, at 10:43 AM, Michael Shulman wrot= e: >> >> 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 homo= topy type theory, e.g., talking about the homotopy fiber and drawing some p= ictures. I like the topological language, because I am mathematician rather= than computer scientist. So, it would be wonderful for me to use topologic= al language and maybe topological intuition when I am programming in Isabel= le/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 univa= lent cumulative Russell-style universes, and is >> polymorphic. >> >> >> >> This version of HoTT involves some axiomatization in addition to univale= nce, 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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n 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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n 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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n 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.