HoTT/UF in MSC2020

HoTT/UF in MSC2020

[Ulrik Buchholtz]

[-- 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 --]

Re: [HoTT] HoTT/UF in MSC2020

[Michael Shulman]

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.

Re: [HoTT] HoTT/UF in MSC2020

[Michael Shulman]

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.

Re: [HoTT] HoTT/UF in MSC2020

[Michael Shulman]

It looks like this month is the end of the first comment/suggestion
period for MSC2020.  Some category theorists have put together a nice
draft proposal incorporating higher category theory into a new 3-digit
18H:
https://www.dropbox.com/s/yr400e893uhhctm/MSC2020.pdf?dl=0
Of relevance to us it includes "18H45 Categories of fibrations,
relations to K-theory, relations to type theory".

There is also apparently a suggestion to add a classification for
"Computer-assisted proofs" to 68 (computer science).

However, I don't see any current proposals to make much change to 03.
What about the following as a concrete proposal?

Add to 03B:
03B16 Dependent type theories
03B17 Homotopy type theories

Rename 03F to just "Proof theory"

New 3-digit grouping 03I "Mathematics in alternative foundations":
03I05 Constructive mathematics (broadly construed, e.g. BISH)
(includes previous 03F65)
03I10 Brouwerian intuitionistic mathematics (e.g. INT) (moved from 03F55)
03I15 Constructive recursive mathematics (e.g. RUSS) (moved from 03F60)
03I20 Paraconsistent and relevant mathematics
... maybe others?
03I25 Univalent mathematics


On Thu, Jan 11, 2018 at 2:35 AM, Michael Shulman <shulman@sandiego.edu> wrote:
> Is there a good place to put "Computer formalization of mathematics"?
>
> On Thu, Jan 11, 2018 at 2:00 AM, Michael Shulman <shulman@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
>> <ulrikbuchholtz@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.