From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.7.11 with SMTP id b11mr5405954pfd.53.1515666958798; Thu, 11 Jan 2018 02:35:58 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.98.81.71 with SMTP id f68ls2302365pfb.4.gmail; Thu, 11 Jan 2018 02:35:57 -0800 (PST) X-Received: by 10.99.112.73 with SMTP id a9mr5350640pgn.153.1515666957802; Thu, 11 Jan 2018 02:35:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1515666957; cv=none; d=google.com; s=arc-20160816; b=jPpq/1RNS5Etgs7hO7eQ4os6YZvKZAU3CN3ZhbxakWlCqi7XRTGLYf0leMOGToWciU r+HR4EaaKpmOgISSlN78TuknTPAGzGupqbUWYTATy7O0+66U+JnsVGx/fg4kun1B30aW dFDPthvVlP+WgLaXob0+JGjXkGUl6PgDCs/UU4Gc4zyX54/HuYygJ7P3QdznGGlFfwOV QdKMK6NHjgvw1JW24+2n916T5gO0i9FLS7jB9QKIcs5myD0M5MpOWo0+rzb6DLtuFjmN kj8gYioTVqqYrymecm4VCG4SBcNA2lBxYMRnUqR9xcr0X7okf4Iul6uRaU5vM+8IzNLp ym2Q== 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=Yg82CMSNuTxY24q6B7IUGTRn6ETZGjPpqCXWIEpyX7g=; b=c/WEqmFF4ERQvpja1pcCHvZbJu9uejSwKZdbUZ1sPvbAaRiQQf8/mVLUnWdIgiFqBy H1TZ3uZNPjlqm0pOa3lP0fB4qDFCqJ+0a6v4DEkC37C7//mAbotWg1lx7WwsU2F4V/oM kQTGFjhyZpgQXL+PX+x6c5Xz9BTZuI9HGDFmbbUUaxB6LGjr6EJJxZZi4cmKBroKCcss 6seSpQRDnnteJk3XSAQoLGAQ8pgDelPALc5l959AJFkX9u9E7V/+QPivbCGcROoq08YP Emr0jr7pQt36VudEb9auegAbntyA/UtGp29K4EM1PgwzXvGNRaImSIiIL0jPk+2d5c6h OkwQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xrE8NfRP; spf=neutral (google.com: 2607:f8b0:4003:c0f::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-ot0-x233.google.com (mail-ot0-x233.google.com. [2607:f8b0:4003:c0f::233]) by gmr-mx.google.com with ESMTPS id d15si489568plj.4.2018.01.11.02.35.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 11 Jan 2018 02:35:57 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c0f::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c0f::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xrE8NfRP; spf=neutral (google.com: 2607:f8b0:4003:c0f::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-ot0-x233.google.com with SMTP id w4so1718983otg.3 for ; Thu, 11 Jan 2018 02:35:57 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=Yg82CMSNuTxY24q6B7IUGTRn6ETZGjPpqCXWIEpyX7g=; b=xrE8NfRPCjIVtNi0/dsybUBVKOTrNFCekc9zWf5EWMqPoz4qC5lgunF1uc1C5KKCa3 +x8rmIubc3Grl9YTylkD8Vfl7gbNzDq8anDz9vrBqDRVo1nTGpazd1S0nNSEWgx5vkah 55r/ujTCaVpV56uBApg93VnAgo2NCJ/khD1ypEm30+6xpjS3BDhHKbMEdzB90Ar8pOee gFyziMwicVk8ujVme6hKrSJysAyaobUWz/zqAzGuvCEBxZEe1E0+BG+UMYXBOIHmFkdq P81S44RVvsDfpyZQfyv9nQV9FXLDS1n6wblyjQc6AZZB5XVQYk19Ze36XZMFg1p+nxzZ hkYw== X-Gm-Message-State: AKwxytcyDj9Y/jw7wQGer/Bqnpyg/dJjESc2xcCT4N0rxjbKt+7ZTFqZ cA+DHXlVSUvlPStzAwvrQQ6IB/HO X-Received: by 10.157.58.99 with SMTP id j90mr13383916otc.1.1515666957067; Thu, 11 Jan 2018 02:35:57 -0800 (PST) Return-Path: Received: from mail-ot0-f169.google.com (mail-ot0-f169.google.com. [74.125.82.169]) by smtp.gmail.com with ESMTPSA id u32sm8223504otb.0.2018.01.11.02.35.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 11 Jan 2018 02:35:56 -0800 (PST) Received: by mail-ot0-f169.google.com with SMTP id a24so1712533otd.4 for ; Thu, 11 Jan 2018 02:35:56 -0800 (PST) X-Received: by 10.157.51.25 with SMTP id f25mr4847542otc.41.1515666956299; Thu, 11 Jan 2018 02:35:56 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.11.178 with HTTP; Thu, 11 Jan 2018 02:35:35 -0800 (PST) In-Reply-To: References: <3f6e7a02-9086-4722-95d4-50bd2c30c364@googlegroups.com> From: Michael Shulman Date: Thu, 11 Jan 2018 02:35:35 -0800 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 Is there a good place to put "Computer formalization of mathematics"? On Thu, Jan 11, 2018 at 2:00 AM, Michael Shulman wrot= e: > 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 f= or >> 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, and= I >> was hoping that we could have a discussion about that here, and then sub= mit >> 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 general= ) >> [or Martin-L=C3=B6f type theory], and 03B17 Homotopy type theories (Depe= ndent >> type theories from a homotopical point of view) >> >> Under 03F Proof theory and constructive mathematics, we add: 03F57 Univa= lent >> mathematics >> >> [With cross references.] >> >> But what about 18 Category Theory and 55 Algebraic Topology? Infinity-to= pos >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout.