HoTT/UF in MSC2020

[Ulrik Buchholtz <ulrikbu...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1138 bytes --]

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


[-- Attachment #1.2: Type: text/html, Size: 1345 bytes --]