From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.93.11 with SMTP id r11mr9432389ywb.103.1515664826594; Thu, 11 Jan 2018 02:00:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.37.102.10 with SMTP id a10ls263163ybc.11.gmail; Thu, 11 Jan 2018 02:00:25 -0800 (PST) X-Received: by 10.129.135.7 with SMTP id x7mr3955274ywf.59.1515664825712; Thu, 11 Jan 2018 02:00:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1515664825; cv=none; d=google.com; s=arc-20160816; b=zYMwy+h4jaeVDisuyIh8Bia7hBDtluOu9XqYc4YV9IHLhUNGHn9B0i1skQoXLj/aLl rBVomPd8Y0lTNUfep7xknkCJS09EWDS0aeRwp8LlB9+0B8Ml/Qq1De5atmPN/6TAQ53K jtOJMb/oV2UyxmYJMO5FuGrDqBN8XWMrMoyaD3AqyuoXPJIPhFxytxX2JA2PaeGt2/4X RO/0Pk5IXdyJ3aQSVGi0IBNXqjCmgdWFp9aeWi04vXXwkDbMDCkbZMs0cVP7FsY86zKi Wg1yBLmvZbJzwzSRLz54JyZtvrrez+aw0/DxPNld+8dER2J3Yv3pK4NjpoGO5N8TEVSp pFiw== 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=B1ZzYxhISvI1YVTKEfivDU7751AuUHJ9VVZrbqg7zMI=; b=LfARpOxUcfTI3s0GAebnarAFnbiHnXdWb2SilJquT1MXzeTN5csa122GWBBoytGEZH NWprGYB0YucP4IQwHAHEw4Rpa0IASaHKQ/ughBC3dZG93vkAFHGdD7ASUBfJwfI8Qs6d d0IbM8x7qziBFnyxetxiDgOXjZYQ8Wey6VyKYcEH6H2pBafk4LPqIT8RBzePMdmAcKoP g4euLw5vyqsYAqWUCZ/merq/XU0vwDitBfMMrf/GpSVq2DAcT4H+BIKwi49cAQr2iS+m l6OnFx9wP4QOdM1bAZL19vgFAFsqy5JDaNqZFUj3PijuT4EkZuq4RIa8LL10sJnyxWfy MSnQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1qgYfAnp; spf=neutral (google.com: 2607:f8b0:4003:c0f::22f is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-ot0-x22f.google.com (mail-ot0-x22f.google.com. [2607:f8b0:4003:c0f::22f]) by gmr-mx.google.com with ESMTPS id u194si569722ywu.2.2018.01.11.02.00.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 11 Jan 2018 02:00:25 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4003:c0f::22f is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4003:c0f::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1qgYfAnp; spf=neutral (google.com: 2607:f8b0:4003:c0f::22f is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-ot0-x22f.google.com with SMTP id 37so1632043otv.6 for ; Thu, 11 Jan 2018 02:00:25 -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=B1ZzYxhISvI1YVTKEfivDU7751AuUHJ9VVZrbqg7zMI=; b=1qgYfAnpOPBauYAT/wRv1wvtpNcGO8wGPsB+MT+VSeDspzDOa7wY9KORiPGvQqR9MJ 0RH8KS+xflF565SRnU4InHN0T2yo8fgqFoQyge9hUko36LFxxEyUv2mC0kKL3CCtZErg kqEw+sIAUvDaY5qBxQpXwlwG+yLIaue/4QOQaHtaCxW9a/YdEVcs68jkqTYrkYhXWVSI BFTXVORGU+8sBcr7EAAOXQ6uE3Io4Yjag/SyNCTgk233RoIH3oT16siSdYNoEqJyautQ sCWiFVSWk1MzJZCh/tcEnLvimDyWHxzi6Uq0uaPN9V/XV2CHnzoXPmyGLmobSO2ap3Wf wxxA== X-Gm-Message-State: AKwxyteWbc3OkALJIcginGU8QznWhfQj9JJZhNQlzd72PON6n0zQRfX/ UsnAvGEXstSSupfDK0Mo85cI5+eY X-Received: by 10.157.47.242 with SMTP id b47mr8909134otd.232.1515664824853; Thu, 11 Jan 2018 02:00:24 -0800 (PST) Return-Path: Received: from mail-oi0-f45.google.com (mail-oi0-f45.google.com. [209.85.218.45]) by smtp.gmail.com with ESMTPSA id j9sm1705020oiy.47.2018.01.11.02.00.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 11 Jan 2018 02:00:24 -0800 (PST) Received: by mail-oi0-f45.google.com with SMTP id y141so1279481oia.0 for ; Thu, 11 Jan 2018 02:00:24 -0800 (PST) X-Received: by 10.202.81.84 with SMTP id f81mr4326832oib.332.1515664823870; Thu, 11 Jan 2018 02:00:23 -0800 (PST) MIME-Version: 1.0 Received: by 10.157.11.178 with HTTP; Thu, 11 Jan 2018 02:00:03 -0800 (PST) In-Reply-To: <3f6e7a02-9086-4722-95d4-50bd2c30c364@googlegroups.com> References: <3f6e7a02-9086-4722-95d4-50bd2c30c364@googlegroups.com> From: Michael Shulman Date: Thu, 11 Jan 2018 02:00:03 -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 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 fo= r > 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 i= s > 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 subm= it > 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 (Depen= dent > type theories from a homotopical point of view) > > Under 03F Proof theory and constructive mathematics, we add: 03F57 Unival= ent > mathematics > > [With cross references.] > > But what about 18 Category Theory and 55 Algebraic Topology? Infinity-top= os > 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 Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.