## 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.

$\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.

## February 15, 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:

## 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 $(\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)

and

• 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)