Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 20, 2021

Native Type Theory

Posted by John Baez

guest post by Christian Williams

Native Type Theory is a new paper by myself and Mike Stay. We propose a unifying method of reasoning for programming languages: model a language as a theory, form the category of presheaves, and use the internal language of the topos.

languageΛcategory𝒫toposΦtypesystem\mathtt{language} \xrightarrow{\;\Lambda\;} \mathtt{category} \xrightarrow{\;\mathscr{P}\;} \mathtt{topos} \xrightarrow{\;\Phi\;} \mathtt{type\; system}

Though these steps are known, the original aspect is simply the composite and its application to software. If implemented properly, we believe that native types can be very useful to the virtual world. Here, I want to share some of what we’ve learned so far.

Posted at 1:59 AM UTC | Permalink | Followups (11)

February 17, 2021

Applied Category Theory 2021

Posted by John Baez

The big annual applied category theory conference is coming! It’s the fourth one: the first three were at Leiden, Oxford and (virtually) MIT. This one will be online and also, with luck, in person—but don’t make your travel arrangements just yet:

It will take place after the Applied Category Theory Adjoint School, which will—with luck—culminate in a meeting July 5th-9th at the same location.

You can now submit a paper! As in a computer science conference, that’s how you get to give a talk. For more details, read on.

Posted at 7:49 PM UTC | Permalink | Post a Comment

February 15, 2021

Isadore Singer, 1924-2021

Posted by John Baez

The great mathematician Isadore Singer died on Thursday February 12, 2021:

Posted at 7:52 PM UTC | Permalink | Followups (6)

February 12, 2021

The Mess at Leicester

Posted by John Baez

The LMS has taken a stand on the mess at Leicester:

Posted at 7:48 PM UTC | Permalink | Post a Comment

February 2, 2021

Tangent ∞-Categories and Cohesion

Posted by David Corfield

I’ve been wondering for a while about the relationship between Robin Cockett, Geoff Cruttwell, and colleagues’ categorical approach to differential calculus and differential geometry, and similar constructions possible in the setting provided by cohesive (∞,1)-toposes.

Now with the appearance of a (,1)(\infty, 1)-categorification of the former, comparison becomes more pressing:

  • Kristine Bauer, Matthew Burke, Michael Ching, Tangent \infty-categories and Goodwillie calculus (arXiv:2101.07819)


  • Michael Ching, Dual tangent structures for infinity-toposes, (arXiv:2101.08805).

In the first of these the authors write

we might speculate on how the Goodwillie tangent structure fits into the much bigger programme of ‘higher differential geometry’ developed by Schreiber [Sch13, 4.1], or into the framework of homotopy type theory [Pro13], though we don’t have anything concrete to say about these possible connections. (p. 13)

Presumably we’d need cohesive HoTT/linear HoTT.

Anyone interested might take a look also at nLab: infinitesimal cohesive (∞,1)-topos, nLab: tangent cohesive (∞,1)-topos, nLab: twisted cohomology, nLab: jet (∞,1)-category.

There’s modal HoTT work in this area, here.

No doubt useful too is

  • Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal, Goodwillie’s Calculus of Functors and Higher Topos Theory (arXiv:1703.09632).
Posted at 8:12 AM UTC | Permalink | Followups (13)