Posts with this logo use 
February 20, 2021
Native Type Theory (Part 1)
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.
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.
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:
- Fourth Annual International Conference on Applied Category Theory (ACT 2021), July 12–16, 2021, online and at the Computer Laboratory of the University of Cambridge.
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
Isadore Singer, 1924-2021
Posted by John Baez
The great mathematician Isadore Singer died on Thursday February 12, 2021:
- Isadore Singer, who bridged a gulf from math to physics, dies at 96, New York Times.
February 12, 2021
The Mess at Leicester
Posted by John Baez
The LMS has taken a stand on the mess at Leicester:
- London Mathematical Society, Mathematics at the University of 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 -categorification of the former, comparison becomes more pressing:
- Kristine Bauer, Matthew Burke, Michael Ching, Tangent -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).