Re: [HoTT] HoTT/UF in MSC2020

[Michael Shulman <shu...@sandiego.edu>]

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
<ulrikbu...@gmail.com> 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, and I
> was hoping that we could have a discussion about that here, and then submit
> 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öf type theory], and 03B17 Homotopy type theories (Dependent
> type theories from a homotopical point of view)
>
> Under 03F Proof theory and constructive mathematics, we add: 03F57 Univalent
> mathematics
>
> [With cross references.]
>
> But what about 18 Category Theory and 55 Algebraic Topology? Infinity-topos
> 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.