From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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-x73e.google.com (mail-qk1-x73e.google.com [IPv6:2607:f8b0:4864:20::73e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1a2ca545 for ; Thu, 8 Aug 2019 21:49:58 +0000 (UTC) Received: by mail-qk1-x73e.google.com with SMTP id e18sf83727548qkl.17 for ; Thu, 08 Aug 2019 14:49:57 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565300996; cv=pass; d=google.com; s=arc-20160816; b=slDvO5MbWgEhGW6058qu9VN1SGzFwhhXP/Qil7W1bop/89ryoonIWD26UQD5vLDE0Z D0SDlUmmtsNkcf0hU7M0O2BeLEKh/iT+VRBwO83mOuS8WAe7EsGX94KTnq5OEBnyIx0N C3janyaGrMbwKXhbFKLC6b6hETDh1hx1HUAnvdf9MqRMhSAUa4lXyl4OoJO0fD7lk2xe qkumoBCzi60512ssClw2trf7HnjRTS8DOwJuOgxOThfaTZVD90duRBoje4RLHDsUG56z oA9ttSOee8bFtpl5adwCNgWXK4hgQQR7izr5E+22ffiOhOjsyMYhxuVLAcsRMpuLvje2 4qsA== 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=q5npnP66MuOLuZGYE04c+lP/cBc0HpcEZD8hUp8r/nE=; b=sQbZsfvuKwtIpjBjvfWxwHu3qQPCXxxwt9RAJYcxjYHG2FizS7VZewjTHm/nrhRBi9 upCJxvy+IzoQu1X9U/jHUeY6iYksH3UDPffHTqxDxsTP/2sWBhlpuxroLWeKmnsbYn9b DStbtjfZX9bBEciy7rEDKqo9nCyIxYf1bm6IV+pAJvdgWgbMeb6u9I8l3fKTuMvtdt6j m/TisyxWkoTgohuR/euw8PBZJWty1cCMer7Xmo740jIiDyapjffGUyMw+mmZFynzi4Vr 11WW+gAdJgnvpKET2yKQtZXlAVeUsEoQ5v/NU7ACQho/KzVpDqBjueP/CjqDApN/p4vw jQdA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=VvsnL7gS; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f 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=q5npnP66MuOLuZGYE04c+lP/cBc0HpcEZD8hUp8r/nE=; b=FfB3ElaiBAndDQfEsMSezjpyAgyRKI6/wpo7IUq5puPESz5pBI/DZNTkrFK4d5tNed Wmi2M1v1xg7W6C7uOf/ZLzW2JdxMJ+WrshxjIWlNAIAS5cErJSMKbPW1DYR2bPeBZmsb nJCzDuTG1fSmlrPRhAP5Bc5FtU+FmiBvXVO+qj+BE/XYChFJn1nkSd0HZuCCM979R5bL 7UnIuGNAZ/jqbpgpcvEyxNKPfvA5zjr6xpfHvhvpFdURnjEo5wYlr8ExTJXSPbeMdx/1 jAg9nV4a6+4o3y5guD8geHTvQBFwrlTkucabjZqHt0eGburd9kGstakqO+ML+I9g+x8k 21Qg== 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=q5npnP66MuOLuZGYE04c+lP/cBc0HpcEZD8hUp8r/nE=; b=hGUYvKaykFz51y+jZaWO5TzbGhJ/HDmyztXpEavoFNIBlP/rCV9ysoeXK2iGp8iQk9 6xRDUatEeGAzaOc/NUirFeHI418Hly3SlYpQy5aqhW4T+W+B7UxMKkxWV88KTzeFlh04 mPsRi2kH/ZT373tnkIi6ArOBVfOdjR/q/QH1YPxhvPZhp+TIsLsfmSmT3aK8snUeCaGr HIlwpllqDFDDNCqjlwWZRIFXGEScHMIYPInEkcUWhaK4Csj2dP9SlkzBSCJMta2gmeTm DssBr4piSANpwNqvka5qsO4GhzfyhVMJCcf9GBV7QTXj8gjcQsusXVXnDcA8Ie413uLX /CCw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXZWP9jqzROmq+Ev7dvFJ84fcFYDx8LmzNbwfhEP7FZP/jUAJBY U/IImXoQDpqSzJW2xzr/cJY= X-Google-Smtp-Source: APXvYqxPvbUfaVorxDJe+kWYtgyqxIZ1d4o27hZfZTjTIKnakCbr+4lJtAxC+qOAdViyoTTwaMWNMQ== X-Received: by 2002:ac8:488a:: with SMTP id i10mr14271720qtq.93.1565300996480; Thu, 08 Aug 2019 14:49:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:bf42:: with SMTP id p63ls2826947qkf.14.gmail; Thu, 08 Aug 2019 14:49:56 -0700 (PDT) X-Received: by 2002:a37:9844:: with SMTP id a65mr15157065qke.500.1565300996191; Thu, 08 Aug 2019 14:49:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565300996; cv=none; d=google.com; s=arc-20160816; b=RUM3SYyTLYKOGA/hiTAhDXW+kH3I7nqrKS3AgbL0EEhEzNFHuJt+p8X2pLplBtOTDp vD93EfKfbeLdqbYFl2Spy/0Yd150dhEPex/I1F1C0i99wYSjKvraLrBcg8wyPjtcicyb Y0L/a82OeYa/tVLe5+VSCogYpI6UN4cqhqS51trTbUprVquhdbZMnanELkOC/ex3jOca bBc15BJrjwAcHkY+4an9Llaxd/MXCapHQ4DEhENg3ThK4yESmTXEI8xP6tMUNtEkhC2T 4c1e8duoNu3yV8DQgrYaUiauT8c275qPKvag3Uuo0WdtZG12ttvY6nIzWsYhj+2ltXZI q2Hw== 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=DY9iq+uOz7BPjfTD/zP/l1JEXAXWvId0rRZx+J6OPCs=; b=ndb5n+HRlkSSNLbQOHvMRyLf7ULK9ahopkp2h/TN1EjK/rQKpzLvFhw5r1S5BMTL9l 0FKmMIfIi0z4YVMaTzl5+a3844ETLiCs+0JNTAsJFirKvk/RUo+a43Dwu/tEf+8SSxYx A658fI40DdNWuqjj31JzM2ZFriDs3pApUhiuzmB5r/+7GUwWVsQctMmYlfbU2Au1zGe7 EnUfUYDu3/5b/GZbpTgxZM/ChKLeGq30AA3jfhRDnE2FevG1C0j3PC3RT2zgHc1nr9lv U3ASkONQMzD+nKdLiL3KU5Fs+TZ2g9aBqC3M3mXNujE/pdmpukXBECVL+wLyuKXRMClU thCQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=VvsnL7gS; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2f.google.com (mail-yw1-xc2f.google.com. [2607:f8b0:4864:20::c2f]) by gmr-mx.google.com with ESMTPS id z145si4321743qka.3.2019.08.08.14.49.56 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 14:49:56 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f as permitted sender) client-ip=2607:f8b0:4864:20::c2f; Received: by mail-yw1-xc2f.google.com with SMTP id i138so34693131ywg.8 for ; Thu, 08 Aug 2019 14:49:56 -0700 (PDT) X-Received: by 2002:a81:3b8e:: with SMTP id i136mr11205282ywa.493.1565300994938; Thu, 08 Aug 2019 14:49:54 -0700 (PDT) Received: from mail-yw1-f46.google.com (mail-yw1-f46.google.com. [209.85.161.46]) by smtp.gmail.com with ESMTPSA id u7sm2092404ywl.80.2019.08.08.14.49.43 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 14:49:46 -0700 (PDT) Received: by mail-yw1-f46.google.com with SMTP id x67so33352479ywd.3 for ; Thu, 08 Aug 2019 14:49:43 -0700 (PDT) X-Received: by 2002:a0d:c804:: with SMTP id k4mr11105100ywd.63.1565300982904; Thu, 08 Aug 2019 14:49:42 -0700 (PDT) MIME-Version: 1.0 References: <728FA1EA-014C-4242-8B34-33A17D7B9208@gmail.com> In-Reply-To: <728FA1EA-014C-4242-8B34-33A17D7B9208@gmail.com> From: Michael Shulman Date: Thu, 8 Aug 2019 14:49:28 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] (Beginner's question) Uses of HITs beyond homotopy theory To: Timothy Carstens Cc: Homotopy Type Theory 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=VvsnL7gS; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f 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: , More generally, all colimits other than coproducts are HITs (of the "non-recursive" variety). This includes both homotopy colimits and ordinary colimits of sets (obtained by 0-truncating homotopy colimits). Having colimits of sets is fairly essential for nearly all ordinary set-based mathematics, even for people who don't care about homotopy theory or higher category theory in the slightest. There aren't really papers specifically about this, because it's so vast, and because there's not much to say other than the observation that colimits exist, since at that point you can just appeal to the long-known fact that once the category of sets satisfies certain basic properties (Lawvere's "Elementary Theory of the Category of Sets") it suffices as a basis on which to develop a large amount of mathematics. The verification of these axioms in HoTT with HITs can be found in section 10.1 of the HoTT Book. (Before HITs, people formalizing set-based mathematics in type theory used "setoids" to mimic quotients and other colimits.) Beyond this, in set-based mathematics HITs are used to construct free algebraic structures, as Niels said. Some free algebraic structures (free monoids, free groups, free rings, etc.) can be constructed based only on the axioms of ETCS, but for fancier (and in particular, infinitary) algebraic structures one needs more. In fact there are algebraic theories for which free algebraic structures cannot be constructed in ZF (at least, under a large cardinal assumption): the idea is to use a theory to encode the existence of large regular cardinals, which cannot be constructed in ZF (see Blass's paper "Words, free algebras, and coequalizers"). But HITs suffice to construct even free infinitary algebras of this sort; see e.g. section 9 of my paper with Peter Lumsdaine, "Semantics of higher inductive types". Thus, HITs can be useful for doing (universal) algebra constructively, where here "constructively" can even mean "with classical logic but without the axiom of choice". On Thu, Aug 8, 2019 at 1:18 PM Steve Awodey wrote: > > quotients by equivalence relations. > see HoTT Book 6.10 > > On Aug 8, 2019, at 2:32 PM, Timothy Carstens wrot= e: > > Sorry for the broad & naive question. I'm a geometer by training but have= been working in compsci for most of my career (with lots of time spent in = Coq verifying programs). > > I've got a naive question that I hope isn't too inappropriate for this li= st: can anyone suggest some papers that show applications of HITs? I'm emba= rrassed to admit it, but I don't know any applications outside of synthetic= homotopy theory and higher categories. > > Perhaps categorical semantics? But even still I'm not personally aware of= any applied results from that domain (contrast with operational semantics;= but I am extremely ignorant, so please correct me!) > > All my best and apologies in advance if this is off-topic for this list, > -t > > > -- > 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/msgi= d/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3= D-A%40mail.gmail.com. > > > -- > 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/msgi= d/HomotopyTypeTheory/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.com. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQyYyPzpT0Y04vi27gdg6Un147RkJ4tyPcCRC_Tsed5PMA%40ma= il.gmail.com.