From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Wed, 10 Jan 2018 11:45:12 -0800 (PST)
From: Ulrik Buchholtz <ulrikbu...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <3f6e7a02-9086-4722-95d4-50bd2c30c364@googlegroups.com>
Subject: HoTT/UF in MSC2020
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_355_893948800.1515613512391"

------=_Part_355_893948800.1515613512391
Content-Type: multipart/alternative; 
	boundary="----=_Part_356_1740087207.1515613512391"

------=_Part_356_1740087207.1515613512391
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

MR (Mathematical Reviews) and zbMATH are currently soliciting comments for=
=20
the upcoming MSC (Mathematics Subject Classification) 2020=20
at https://msc2020.org/

I would like to suggest some new entries for the work that we do, as it is=
=20
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=
=20
was hoping that we could have a discussion about that here, and then submit=
=20
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)=
=20
[or Martin-L=C3=B6f type theory], and 03B17 Homotopy type theories (Depende=
nt=20
type theories from a homotopical point of view)

Under 03F Proof theory and constructive mathematics, we add: 03F57=20
Univalent mathematics

[With cross references.]

But what about 18 Category Theory and 55 Algebraic Topology? Infinity-topos=
=20
theory and the relations to HoTT/UF don't really fit in the existing=20
categories there, either.

Looking forward to your comments,
Ulrik


------=_Part_356_1740087207.1515613512391
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">MR (Mathematical Reviews) and zbMATH are currently solicit=
ing comments for the upcoming MSC (Mathematics Subject Classification) 2020=
 at=C2=A0https://msc2020.org/<div><br></div><div>I would like to suggest so=
me new entries for the work that we do, as it is not always a perfect fit f=
or the old MSC 2010 system. (To put it mildly!)</div><div><br></div><div>Bu=
t what should we suggest? This wasn&#39;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.</div><div><br=
></div><div>To get started, what do you think of the following:</div><div><=
br></div><div>Under 03B General Logic, we add: 03B16 Dependent type theory =
(in general) [or Martin-L=C3=B6f type theory], and 03B17 Homotopy type theo=
ries (Dependent type theories from a homotopical point of view)</div><div><=
br></div><div>Under 03F=C2=A0Proof theory and constructive mathematics, we =
add: 03F57 Univalent mathematics</div><div><br></div><div>[With cross refer=
ences.]</div><div><br></div><div>But what about 18 Category Theory and 55 A=
lgebraic Topology? Infinity-topos theory and the relations to HoTT/UF don&#=
39;t really fit in the existing categories there, either.</div><div><br></d=
iv><div>Looking forward to your comments,</div><div>Ulrik</div><div><br></d=
iv></div>
------=_Part_356_1740087207.1515613512391--

------=_Part_355_893948800.1515613512391--