From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB3VWRLNQKGQEO2YTBBA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-it0-x239.google.com (mail-it0-x239.google.com [IPv6:2607:f8b0:4001:c0b::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2f295b25 for ; Thu, 2 Aug 2018 05:49:36 +0000 (UTC) Received: by mail-it0-x239.google.com with SMTP id l138-v6sf1180583itb.7 for ; Wed, 01 Aug 2018 22:49:36 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1533188974; cv=pass; d=google.com; s=arc-20160816; b=MdEamdwButAv8gTu3eQEBI4mI22ZTVtp/ypKrne0bCFC8zkGQ0Wq6Nt7kcrLzfAIa7 Z8Hr0OeAMeJEeIcypnrKznrFf6Spw1DiS1Kp7F0D4IUgYy/4Oq8paRlAEZQJlhXj3+UY 7oL/kEEpGxfXNj3+BW5FVQsOHB7N/5kczrr2pS/xnXvvVWCfJLdt4DBJmPlEloNUixN8 rPGqCaSPukPBcK3GmZbl0E2RKvf0HfQid0FU3rKKzu+RYdeZjRx/K/S2p8acgG2ifABC R6SKfBngsT+t3lj5GQZqFWhU+6wkTYIIDaZIVfDhHMKK8HvtPyY8Yw802QmiVIDyA1ei 8eFQ== 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:references:in-reply-to:mime-version :arc-authentication-results:arc-message-signature:sender :dkim-signature:arc-authentication-results; bh=Aw43Ia42hkMf3P1G1fyoR7Et9uqoR2AkOoPZzJN5Ens=; b=VBdZvyvYbYeL/h4sdFSo/49mvqdajtFqVeat8SkrkEtP2hfyZhl6NywAuuKkllYVb8 SCFfoGwSwBRvoXGeWLkjzyD/elS4QJxKdBZN0jSyUWO1GIKDTlz5bil8IX8jREbTRP+i hF6g5X/1TD3EeZSdRMvBuYGS+qWS5m02LrLB6kPEsR9FtJiufrR8ocAha1MOYzHg8eF5 uaGlBf3NXe2RNuTHfrS8tFCYpx+M9yTHIPZ7cEvJi+7qKCESwR+dgCIEE8dLzGwmhrZl 7bU9YLIVweNs51TfbJL1EW9ggNHt1lAH7a2LoYCBmjxdQbXq9bWrS87o03z0xv3CcpmS dNgw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IRZqkrsr; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:in-reply-to:references: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=Aw43Ia42hkMf3P1G1fyoR7Et9uqoR2AkOoPZzJN5Ens=; b=JUlwUxUxcko03DwYrKsF1tdmoPLefpSh8DU/y4NTqiYVYP/WdGa3NRgOK5xQD5AYpu hrEDwfN7BdyufUvoGRTQOW696XtBst7H5tHKxRF74+JgGooOQ0CQdmKLxaqQO+IJc1wy kMp4hMoLyxE0QlB7RYKDYz0Z1/NXQ+xfq6T0YWsVmJiGzzFHAntOSww9GywJlgU+s8DY S92NEEtEkkuP7kOhrZ0s8E+z6cs7HPQ8XVn9Qsj5F8JV0Kvo1wN/xbgcLwPSXBAOlopU l+S9uJAkONGQwYAU3VsNXrdaZ+be0RBaTyeKGDvkpYBtEJ4XDSRKUJA85nd+v8F7gtmN tPVQ== 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:in-reply-to:references: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=Aw43Ia42hkMf3P1G1fyoR7Et9uqoR2AkOoPZzJN5Ens=; b=IpTn6GFxbYxa7nBf+KekH4DvDqot1n7M7uEUwuKWSyX/Mgb1N61OgE5hbfC+Qn/Itj 6CxhSZ1IBrbGe8a23LeSQh7pdVIdX2hZKFsVuyA364pYYJ2q57QmgiYJNqs4hTVxsJxH 6UVFRzUPnHry6GE6S4cpNp5Iv3tCxos2fmyZPoLC/SE9hxFTvi9lNWz/X2y4JqG07W/B S901SLW1FwIgsKKHpiL60eSJYn1ZgMUciP5XfpXjQJSrOdKh8LFUdacGcACpSJzxMXoz tKJ/o6EMDHTioN6CtSpBTTUiF/bVCU2NtW8WCMhFnVaBMmI+JfY5vGE1PvB0cd1S6SJX HpDQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHgGiqdl5XHXa4mT8HMLvweDpHDYzDDbsCwzPYyVTfDbY9stWEm irhWXQspE7sSMaL0DWLlQMk= X-Google-Smtp-Source: AAOMgpdCbYPVc1B2afRDVTjjmT6UW69bMv61FBT5GRKS9De6vbGciJC5SZ24MDAUqdrOxsH92ERgOg== X-Received: by 2002:a02:a485:: with SMTP id d5-v6mr7158jam.7.1533188974450; Wed, 01 Aug 2018 22:49:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5e:de01:: with SMTP id e1-v6ls142338iok.11.gmail; Wed, 01 Aug 2018 22:49:34 -0700 (PDT) X-Received: by 2002:a6b:8ec5:: with SMTP id q188-v6mr582061iod.2.1533188974116; Wed, 01 Aug 2018 22:49:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1533188974; cv=none; d=google.com; s=arc-20160816; b=ysKAnsPXThmgJDsqkzQ/9DTnAjVaVvGuVlXfRW11hnOjWYRy3gckHOKeLQHz8ZrBeb /QVHCp1+50yViTsNK5DuyFSwUGX9ZOr8du4P6wlI+7yxhbGFTzl9iM6oon5HWatbuyN6 D8cRFHQnVCDY/nEeXWGF3npap7DhnB77ZoACm67aLCxnG9chXNQw4BkxL5vsPY/7Ph0V HFt5cul2Plh3CAYnyhU6IC6KY9eolvwz8eBeYZ0BYdLXnmrc/bJzZDvqx99jmy+XAmL3 zt91omfTbCkbArgXoBrsag5X9/nysJmEkD5efJv4zhx1k1GJHd4Zx4PWg6bSMLe4VAjb 6Y5g== 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 :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=h5QAxynNvx5aDPBGTyBuUyGWXaiz9IOXEvUacWCOsRw=; b=rg4pmGC86icKfHoLEum70C9ngeM+JusYeuWFj6HbHJMy0r5voWqVLtLV/O4RpfISiU J9pG0C+HzUGcNrciF6JjcRtGI0mgmhhZTzHuRPsIivYEQx6mum3r1Lo/FE1EOy+hsgIE G0h9l00/Zkaw5R52Ssn0Xxs9XrQ6VOK50Uwdq0Py4bmPlj42GRlIydiVfcEE48p8CSY4 Cjx8iopyrOtrZiEN2dl68l+cNo5aspn6WOmyE2WSegBYFElhGaZHlPoexWGM19cC//Xo BOESJ6OU+rdSEztJIm2sD8TYNYlYAMwgitQtQ/3aTwkI89KeyG+8LZVatkn/LX/iZ5kb ZOdQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IRZqkrsr; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb0-x229.google.com (mail-yb0-x229.google.com. [2607:f8b0:4002:c09::229]) by gmr-mx.google.com with ESMTPS id l15-v6si47012iom.1.2018.08.01.22.49.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 01 Aug 2018 22:49:33 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c09::229; Received: by mail-yb0-x229.google.com with SMTP id c3-v6so382746ybi.13 for ; Wed, 01 Aug 2018 22:49:33 -0700 (PDT) X-Received: by 2002:a25:bb04:: with SMTP id z4-v6mr623003ybg.238.1533188973288; Wed, 01 Aug 2018 22:49:33 -0700 (PDT) Received: from mail-yw0-f173.google.com (mail-yw0-f173.google.com. [209.85.161.173]) by smtp.gmail.com with ESMTPSA id t4-v6sm385672ywg.98.2018.08.01.22.49.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 01 Aug 2018 22:49:32 -0700 (PDT) Received: by mail-yw0-f173.google.com with SMTP id y203-v6so385044ywd.9 for ; Wed, 01 Aug 2018 22:49:32 -0700 (PDT) X-Received: by 2002:a81:84cb:: with SMTP id u194-v6mr642717ywf.246.1533188971760; Wed, 01 Aug 2018 22:49:31 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Wed, 1 Aug 2018 22:49:11 -0700 (PDT) In-Reply-To: References: <3f6e7a02-9086-4722-95d4-50bd2c30c364@googlegroups.com> From: Michael Shulman Date: Wed, 1 Aug 2018 22:49:11 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] HoTT/UF in MSC2020 To: Ulrik Buchholtz 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=IRZqkrsr; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shulman@sandiego.edu) 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 looks like this month is the end of the first comment/suggestion period for MSC2020. Some category theorists have put together a nice draft proposal incorporating higher category theory into a new 3-digit 18H: https://www.dropbox.com/s/yr400e893uhhctm/MSC2020.pdf?dl=3D0 Of relevance to us it includes "18H45 Categories of fibrations, relations to K-theory, relations to type theory". There is also apparently a suggestion to add a classification for "Computer-assisted proofs" to 68 (computer science). However, I don't see any current proposals to make much change to 03. What about the following as a concrete proposal? Add to 03B: 03B16 Dependent type theories 03B17 Homotopy type theories Rename 03F to just "Proof theory" New 3-digit grouping 03I "Mathematics in alternative foundations": 03I05 Constructive mathematics (broadly construed, e.g. BISH) (includes previous 03F65) 03I10 Brouwerian intuitionistic mathematics (e.g. INT) (moved from 03F55) 03I15 Constructive recursive mathematics (e.g. RUSS) (moved from 03F60) 03I20 Paraconsistent and relevant mathematics ... maybe others? 03I25 Univalent mathematics On Thu, Jan 11, 2018 at 2:35 AM, Michael Shulman wro= te: > Is there a good place to put "Computer formalization of mathematics"? > > On Thu, Jan 11, 2018 at 2:00 AM, Michael Shulman w= rote: >> I agree with proposing adding "dependent type theories" to 03B, >> although one could argue that it fits under 03B15 "Higher-order logic >> and type theory". >> >> I don't think I would put homotopy type theories in 03B, though; it >> seems too specific. Syntactic study of homotopy type theories could >> go under your 03B16, while semantic study could go under 18C50 >> "Categorical semantics of formal languages" and/or 03G30 "Categorical >> logic, topoi". For higher categories/toposes themselves there are >> 18D05 "Double categories, $2$-categories, bicategories and >> generalizations" (although that should be renamed to something like >> "higher categories", and maybe moved to somewhere other than 18D >> "Categories with structure") and 18B25 "Topoi" (which I would >> interpret to include higher topoi as well -- although I don't >> understand why 18B25 is under 18B "Special categories"). >> >> I might propose replacing 55U35 "Abstract and axiomatic homotopy >> theory" and 55U40 "Topological categories, foundations of homotopy >> theory" with three topics like "Model categories and generalizations", >> "Homotopy theory in higher categories (see also 18D05)", and >> "Synthetic homotopy theory (see also 03B16, 18C50, 03G30)". >> >> What seems to me like the really egregious mistake is lumping together >> "Proof theory and constructive mathematics" in 03F, since most >> constructive mathematics has nothing to do with proof theory. What >> about proposing a new three-digit [sic] classification like "03I >> Mathematics done using alternative foundations", which could contain >> things like 03I01 "Constructive mathematics" and 03I02 "Univalent >> mathematics" -- distinguishing the *use* of such foundations from >> their *metatheoretic* study (which is what most 03 "Mathematical logic >> and foundations" seems to be about). >> >> Overall, it's unclear to me what the criteria should be for giving a >> subject its own three- or five-digit classification. The community of >> univalent mathematics and synthetic homotopy theory is still quite >> small relative to all of mathematics, so we might not be justified in >> asking for our own five-digit classification(s). On the other hand, >> many of the existing five-digit classifications seem to me, as an >> outsider of the fields in question, to be *extremely* narrow. It >> would be useful to have some data regarding how much mathematics is >> being done under existing classifications; are there existing >> five-digit subjects whose communities are the same size as HoTT/UF or >> smaller? Is there any good way to get (or approximate) such data? >> >> >> >> >> On Wed, Jan 10, 2018 at 11:45 AM, Ulrik Buchholtz >> wrote: >>> MR (Mathematical Reviews) and zbMATH are currently soliciting comments = for >>> the upcoming MSC (Mathematics Subject Classification) 2020 at >>> https://msc2020.org/ >>> >>> I would like to suggest some new entries for the work that we do, as it= is >>> not always a perfect fit for the old MSC 2010 system. (To put it mildly= !) >>> >>> But what should we suggest? This wasn't entirely clear to me either, an= d I >>> was hoping that we could have a discussion about that here, and then su= bmit >>> our consensus proposal (if we can get one) at msc2020.org. >>> >>> To get started, what do you think of the following: >>> >>> Under 03B General Logic, we add: 03B16 Dependent type theory (in genera= l) >>> [or Martin-L=C3=B6f type theory], and 03B17 Homotopy type theories (Dep= endent >>> type theories from a homotopical point of view) >>> >>> Under 03F Proof theory and constructive mathematics, we add: 03F57 Univ= alent >>> mathematics >>> >>> [With cross references.] >>> >>> But what about 18 Category Theory and 55 Algebraic Topology? Infinity-t= opos >>> theory and the relations to HoTT/UF don't really fit in the existing >>> categories there, either. >>> >>> Looking forward to your comments, >>> Ulrik >>> >>> -- >>> You received this message because you are subscribed to the Google Grou= ps >>> "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.