Re: [HoTT] HoTT/UF in MSC2020

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

Is there a good place to put "Computer formalization of mathematics"?

On Thu, Jan 11, 2018 at 2:00 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> 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.