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