From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:9b8f:: with SMTP id y15mr11790926plp.148.1589137084488; Sun, 10 May 2020 11:58:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:a717:: with SMTP id w23ls4028894plq.7.gmail; Sun, 10 May 2020 11:58:03 -0700 (PDT) X-Received: by 2002:a17:902:b491:: with SMTP id y17mr12359933plr.9.1589137082948; Sun, 10 May 2020 11:58:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589137082; cv=none; d=google.com; s=arc-20160816; b=aCeDNF59P3A56ImQbJbz38s2tyDGqAsgeV1v3l3mSmBzEzTk7h3Svbjx9NpGIvLLRc uim0yrKKepFZqyqynI7LAOEOq7u8U24LgakUhCyKTe6TABKL1D4aliQ6MUujy0nYideK 4r73TxsRbUu8yckRh9GhRUjpHfJVI5w7J5hNEqTK6doUMLGX1zXFwvT2Vk2emOuJD86Q M0LLiAQic+gM2AAiz6+UfbY5/UixRRygODf5d2w9MnxWWcQHNkWBmqMuQ2U4Ru8ltBzW FsKXdGP4x2fIaCjG6DUxjG4Qy8CSMsxPEOR3UE7W5OeqKz/Gl4yWrLkKI5wafLHngVHZ LP5w== 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=gJYHFP+sUeXKTHRs21HmxDugjDh9ceCijPlNILIlMTI=; b=TJoRulSVAgUvDQv5IgkoPyDUbUaFP9IAlk4/1wHHHeUPssEvKRN+0cGQ8mNpedZiiA HBsLlfbDUrKqzI6fuDrYzakT4L6UnU9Y+P3pKz+oje72dmkOPjrMH1INSMR3aIk/5OWS zG+78urOliAyzPZHVCShXs3daFoaOk52ZXUlxuhGslp9wXMaN8nO4qooA/a1eLuOHMwS Etb5N5IyltD1p6IFBc8goklO1FrWSb5/5yw/F+py5FThjQEDh99tXwPV+55A/cn3TZWL nVP6WALIJKG4No7c9aKdZlvCgf+Q4qmwO+FNEYyqAsQnLz+K2W+QVInKGtc449jSkF9v Yo+g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pmJNNNLe; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32b as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-ot1-x32b.google.com (mail-ot1-x32b.google.com. [2607:f8b0:4864:20::32b]) by gmr-mx.google.com with ESMTPS id l10si339360pgh.3.2020.05.10.11.58.02 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 11:58:02 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32b as permitted sender) client-ip=2607:f8b0:4864:20::32b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pmJNNNLe; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32b as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x32b.google.com with SMTP id j26so5842617ots.0 for ; Sun, 10 May 2020 11:58:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=gJYHFP+sUeXKTHRs21HmxDugjDh9ceCijPlNILIlMTI=; b=pmJNNNLeqZXglQ21xIpVgc+wzqOYRXGw6Y7RphyCcEIEvcsluHLesudl/dpO/FEFsv UiuCWibTik6/3j8VN6Bz4lHkzNjpOa66KunEoyGe99/ZB4I+aV9iuWd1hAtP4VritBxC gYEMbFvK+R3tKx+y5bv5ZWXxGnAhOzONLjX1MFjh2f0YTVcFHIlev3sKHPxg90bCJpdC KRbqy8L8VG1Ypu4LLlxsj08mvzVRXphLf730tMFBGwCAUv2XEyp4qhUgdwgfoLnEFWjD fXli8GxwbD1C2MqTPB8w4SzArTTj+9BsiyP/g2IeOY8iRAa27FcRIKFWMT/qOmHVt7Tz 3f2Q== X-Gm-Message-State: AGi0PuY43LRekBg/Pz+Z56b1I44s0ZxCRNEyi/z7uRAoHnHJBh7qNfdA VhNBYFge23c+2eFrsngW4MC5rk+LBltNSsIkHELJI2pUdd7YX6xeX7orXaqkWmZRKT3B08vo7tP w21OvzNYl0kVU0D4gufN88wT68fNv9bO4P9ePTHAoJf7CpR/U92Orw6VkiA56PZOTem3GeOZjyO HZSRyEaLQ6 X-Received: by 2002:a9d:1441:: with SMTP id h59mr10115926oth.192.1589137081884; Sun, 10 May 2020 11:58:01 -0700 (PDT) Return-Path: Received: from mail-ot1-f51.google.com (mail-ot1-f51.google.com. [209.85.210.51]) by smtp.gmail.com with ESMTPSA id d5sm2208213oom.22.2020.05.10.11.58.00 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 11:58:00 -0700 (PDT) Received: by mail-ot1-f51.google.com with SMTP id z17so5806058oto.4 for ; Sun, 10 May 2020 11:58:00 -0700 (PDT) X-Received: by 2002:a9d:170e:: with SMTP id i14mr10310395ota.283.1589137080207; Sun, 10 May 2020 11:58:00 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> In-Reply-To: From: Michael Shulman Date: Sun, 10 May 2020 11:57:47 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Nicolai Kraus Cc: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , Thomas Streicher , David Roberts , Thorsten Altenkirch , Steve Awodey , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" On Sun, May 10, 2020 at 9:51 AM Nicolai Kraus wrote: > It's easy to change the second definition to > define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 , > arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there > is a nice way for the first definition. On the other hand, it's easy to change the first definition to define monoids/semigroups/rings/fields/lattices/universal-algebras/etc., and impossible to do the same for the second. I think the fact that groups are part of the general theory of algebraic structures on sets is more important to incorporate in a definition. The equivalence between groups and connected pointed 1-types is better viewed as a theorem than a definition. And hence, the "definition" of oo-groups as connected pointed types is more of a hack than a true definition. In an ideal world, that would be a theorem too. (And the corresponding theorem in classical mathematics has important content: there are important oo-groupoids that are obtained by delooping oo-groups nontrivially.)