From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 22502 invoked from network); 30 Apr 2023 00:43:30 -0000 Received: from mail-pf1-x43e.google.com (2607:f8b0:4864:20::43e) by inbox.vuxu.org with ESMTPUTF8; 30 Apr 2023 00:43:30 -0000 Received: by mail-pf1-x43e.google.com with SMTP id d2e1a72fcca58-63b57ad54a1sf743293b3a.3 for ; Sat, 29 Apr 2023 17:43:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682815409; cv=pass; d=google.com; s=arc-20160816; b=shmZx6IULyN10DoZHhy+7MR6WhYKiqOs+73gBQkTPAWwQB2j3WuFTJwwch4J5OZrz5 LCRDCTMgErXVSeLYRVveOPm7cdY58IrD+8AH7hZhfchkau7zPphG9qt65tWsGBo/1mZC wOwHJcXx8l6Pu3n8m5cz0WktQPmT7pmAKRTpz+1e7HG1YtoSCoDJKiIh6ryxAnGWC60A iBP0pLIlKPHxR+W6xvuiscuN+xrwThfKF4R5AgU9KmIEJckYt1mgVg3upHK6yyemAb/7 nnrA1m6j0W19Ydo5K1PBJSa3w2v3BWEOmAVo8Vd6mZLuNYqw/X81TqennsEP43YqQYOL 3HYQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe: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; bh=wcJtW4InyhzR/5nAF362aztPQbLvJ3SQvQ5Uhot3mEc=; b=u0bkkE7rqn/8WpkYakqrlrd+fnLelkp52PADsKeqvA18VuCddeRUNDitisdvheSo54 wn1MsdDOpNwMND7uYFWEnyLgq2qdgvp2yJiIJeRsyF6nUnLXhAoYP9KcYRykeb6sy3wJ wQsvcZDngvMyCikEZgXy9ggmsOTU1SxFP2NPIIWam6/POAZn5KiJn3ENA6qZS46BDJfx gquINlRR6ZT7Lwq4Rydu6WxzxEQulf59ZLAiNPOplKJESU1dBgW0QwgBL7MqdBohIvQh iQW7Y9hvuVGXc8+WWVyuPRfIEsNSfTdXjShrbNqNXl+QYSwHmmmdEmhOxgEyDGjNgY3d tbqg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SeyHEyGh; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682815409; x=1685407409; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=wcJtW4InyhzR/5nAF362aztPQbLvJ3SQvQ5Uhot3mEc=; b=JZcHj3He7BKRvx7xSjzeV0Qnx3srLrZpr4ioAfBAfh2V1flFI7lZp8DIQdvjuOCp6P wvNkD80gvALy0TdioX5niVwzXEeJGiFgA+4YwCmCjcxCwpxksi5U+uGcqK37yoRDATlY icJeU+AY+UUCI4pzVLFzl5ozFTge7W9kZ0eoemhe91+udfq6z1RxsUkC1bEbn+f1Rv0R nWvj+hoHdKIdSffbiMw21077K3tNGP5HeBjmhD3GwzmAU971CCVvSFdONHvi3kQmjJzH SUsVZiQ7icjzPAqNoqrtY8VCa3NlFSOoLkmnE7S0r291NK2WYLT44p6vPsAJCobNUlJW VLKA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682815409; x=1685407409; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=wcJtW4InyhzR/5nAF362aztPQbLvJ3SQvQ5Uhot3mEc=; b=E348cMOlRqrlm1s2ioH0/D1ndVy0aay6KxpPAsNRt1+Yf/vNUzuiUENpDVwYa269m5 UnIvjlRK+spVeGegDClc3szOdWmxUlDETNk/ZvjQDIslSYdrKhMqYvIrr243xJCORRls pGRrmb+wik7715R7v4QtKTqsoSBB5oC93glMKA93hwL3u16Ek2ziNypgU3Ko09cUjTOX i2WUiVkUuQIt9Uqp0KmJg6fJ7VbQhU7g5AS6/tw68n2eU8RLSuCF6Eep0MI1T0MG8Hg8 wUOMH8OYY81bsPiBRJeAt6hBI+yN4EjGTcCLQid4zGrNJLABS0TWYdvrrzHtR40axkA6 j3nQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDxRdhOV8kYzP7h3xpjcdqONjMBHr38p7UhaDERcQh9l2+Rxohq4 iL+AfI4an7+twdmsPgbuJYE= X-Google-Smtp-Source: ACHHUZ4v7hCpc5Uvn0qgiOjqEUw4tO9pEMkSN5tIHIaqIB3REuqWpfGlFUPEOfF3QyGrr+GcP6IUfA== X-Received: by 2002:a05:6a00:d56:b0:641:31b1:e787 with SMTP id n22-20020a056a000d5600b0064131b1e787mr1542794pfv.5.1682815409319; Sat, 29 Apr 2023 17:43:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:903:22c9:b0:194:d87a:ffa6 with SMTP id y9-20020a17090322c900b00194d87affa6ls7909838plg.1.-pod-prod-gmail; Sat, 29 Apr 2023 17:43:27 -0700 (PDT) X-Received: by 2002:a17:902:f707:b0:19f:2dff:21a4 with SMTP id h7-20020a170902f70700b0019f2dff21a4mr9541810plo.16.1682815407166; Sat, 29 Apr 2023 17:43:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1682815407; cv=none; d=google.com; s=arc-20160816; b=iLn9+USM3Z1XUJf2X6kGYxanzibvM/J+VJ7s02lGPJwd5/IFqGfJ4doRDpcyUxQHld CY+/3MQkgXYK3tPPdFMguJwyfDIulnUYRCv1e/oCYMMc/PgSmJn8p3G7f8Wjv8BIByvv mNKYv6HMzMbteKnQX8Ut/gWjq/dvKBCwVeE1KBj1m4fCl29YMz/v9vA+UEZYTLUKxe5e OvsqSd6VJ+PyoM1+OimsiI1ILzmM/Yb+LTBPx1St9bgMj55f7cb/6+4RljSl95O/vCxL kvfRC3fGwcKcLqWJnmWFYQNPgyXfZRkRZ0WfFUpFFetvvfv8IzFm5Bn6mB4eJ9LxxH2l c+Ug== 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=lTvW3OJbsDyxLl02IijfjDFqXUnQspGqfXNUwKMuNWU=; b=F4WLjRfHdL4aLEwlsMxytFgRxY4Q7O7AkSRTalzbx/OQ75uJTJVtBfaRcCL7bXurNz ghkJVftBTdxV1zaZZK/6Xcyd2+c8wz2d0B65O7wFsaheSAo7amXEA5y69T1hKpOLBd6z O7mDf+jJ/BKqZcUwtMEo5dTaXomDNZSX55c6dc6qYVgRy6Q66QdB7caC8Wwah9pBVrOz rwzzDmO5yLAKFE3gEDtkWRqfHHJHLfdUdK5z+o6Se3fa0nbhbsHX6ZHQbQzjVvhmu6aB h2mKgrcluZMBMCguEzeeq891vvlCEV+U7wwdimnEREaqi+aIPTnH6xej77GvgHm3QPOT nqTQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SeyHEyGh; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yb1-xb31.google.com (mail-yb1-xb31.google.com. [2607:f8b0:4864:20::b31]) by gmr-mx.google.com with ESMTPS id k15-20020a170902d58f00b001a963644ebdsi909494plh.11.2023.04.29.17.43.27 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 29 Apr 2023 17:43:27 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) client-ip=2607:f8b0:4864:20::b31; Received: by mail-yb1-xb31.google.com with SMTP id 3f1490d57ef6-b9d8730fe5aso1928694276.1 for ; Sat, 29 Apr 2023 17:43:27 -0700 (PDT) X-Received: by 2002:a25:4143:0:b0:b99:370f:a35c with SMTP id o64-20020a254143000000b00b99370fa35cmr8713141yba.35.1682815406343; Sat, 29 Apr 2023 17:43:26 -0700 (PDT) MIME-Version: 1.0 References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> <5D0912E6-075B-47EE-87B8-8B5118DDF07C@gmail.com> In-Reply-To: <5D0912E6-075B-47EE-87B8-8B5118DDF07C@gmail.com> From: Michael Shulman Date: Sat, 29 Apr 2023 17:43:15 -0700 Message-ID: Subject: Re: [HoTT] Free higher groups To: Steve Awodey Cc: Ulrik Buchholtz , Dan Christensen , "homotopytypetheory@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000084a98205fa82fedb" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=SeyHEyGh; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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: , List-Unsubscribe: , --00000000000084a98205fa82fedb Content-Type: text/plain; charset="UTF-8" Bringing this thread back to David's original announcement of his new result, one thing that intrigues me about it is that proceeds by constructing successive approximations to the desired path space and then taking a sequential colimit. This reminds me of some other sequential constructions that also achieved surprising (to me) things, like Egbert's join construction for building propositional truncation out of nonrecursive HITs, and the splitting of a quasi-idempotent by a sequential (co)limit that Lurie used in higher category theory and I then adapted to HoTT. I wonder if there are other surprising applications of this principle. -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpzinvAW_PgLUPbp4NyykJxhEbmBsQSC6rQroZWCcFg9xw%40mail.gmail.com. --00000000000084a98205fa82fedb Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Bringing this thread back to David's original announce= ment of his new result, one thing that intrigues me about it is that procee= ds by constructing successive approximations to the desired path space and = then taking a sequential colimit.=C2=A0 This reminds me of some other seque= ntial constructions that also achieved surprising (to me) things, like Egbe= rt's join construction for building propositional truncation out of non= recursive HITs, and the splitting of a quasi-idempotent by a sequential (co= )limit that Lurie used in higher category theory and I then adapted to HoTT= .=C2=A0 I wonder if there are other surprising applications of this princip= le.

--
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.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CADYavpzinvAW_PgLUPbp4NyykJxhEbmB= sQSC6rQroZWCcFg9xw%40mail.gmail.com.
--00000000000084a98205fa82fedb--