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

## January 31, 2021

### Structured vs Decorated Cospans

#### Posted by John Baez

Some of us just finished a paper clarifying the connection between two approaches to describing open systems—that is, systems that can interact with their environment, and can be composed to form larger open systems:

• John Baez, Kenny Courser and Christina Vasilakopolou, Structured versus decorated cospans.

And, next week I’m giving a talk about it at YAMCaTS! This is not a conference for felines who like sweet potatoes: it’s the Yorkshire and Midlands Category Seminar, organized by Simona Paoli, Nicola Gambino and Steve Vickers.

Posted at 12:38 AM UTC | Permalink | Followups (2)

## January 30, 2021

### Nishan Canagarajah Screws Up

#### Posted by John Baez

The Vice-Chancellor of the University of Leicester, Nishan Canagarajah, wants to lay off all 8 of their pure mathematicians, including the only 2 women with permanent positions, and then rehire just 3 of these mathematicians — to do teaching, but not research. He and his flunkies claim:

[…] to ensure a future research identity in AI, computational modelling, digitalisation and data science requires ceasing research in Pure Mathematics […]

Protest by signing these petitions:

Posted at 6:42 AM UTC | Permalink | Followups (10)

## January 24, 2021

### Open Systems: A Double Categorical Perspective (Part 3)

#### Posted by John Baez

Back to Kenny Courser’s thesis:

Last time I explained the problems with decorated cospans as a framework for dealing with open systems. I vaguely hinted that Kenny’s thesis presents two solutions to these problems: so-called ‘structured cospans’, and a new improved approach to decorated cospans. Now let me explain these!

Posted at 12:44 AM UTC | Permalink | Followups (2)

## January 20, 2021

### Postdoctoral Position in HoTT at the University of San Diego

#### Posted by Mike Shulman

The University of San Diego invites applications for a postdoctoral research fellowship in homotopy type theory beginning Fall 2021, or earlier if desired. This is intended as a two-year position with potential extension to a third year, funded by the second AFOSR MURI grant for HoTT, entitled “Synthetic and Constructive Mathematics of Higher Structures in Homotopy Type Theory”.

## January 19, 2021

### Categories of Nets (Part 2)

#### Posted by Mike Shulman

Now that John gave an overview of the Petri nets paper that he and I have just written with Jade and Fabrizio, I want to dive a bit more into what we accomplish. The genesis of this paper was a paper written by Fabrizio and several other folks entitled Computational Petri Nets: Adjunctions Considered Harmful, which of course sounds to a category theorist like a challenge. Our paper, and particularly the notion of $\Sigma$-net and the adjunction in the middle column relating $\Sigma$-nets to symmetric strict monoidal categories, is an answer to that challenge.

Posted at 5:38 PM UTC | Permalink | Followups (2)

## January 17, 2021

### Categories of Nets (Part 1)

#### Posted by John Baez

I’ve been thinking about Petri nets a lot. Around 2010, I got excited about using them to describe chemical reactions, population dynamics and more, using ideas taken from quantum physics. Then I started working with my student Blake Pollard on ‘open’ Petri nets, which you can glue together to form larger Petri nets. Blake and I focused on their applications to chemistry, but later my student Jade Master and I applied them to computer science and brought in some new math. I was delighted when Evan Patterson and Micah Halter used all this math, along with ideas of Joachim Kock, to develop software for rapidly assembling models of COVID-19.

Now I’m happy to announce that Jade and I have teamed up with Fabrizio Genovese and Mike Shulman to straighten out a lot of mysteries concerning Petri nets and their variants:

This paper is full of interesting ideas, but I’ll just tell you the basic framework.

Posted at 8:49 PM UTC | Permalink | Followups (11)

## January 12, 2021

### This Week’s Finds (1–50)

#### Posted by John Baez

Take a copy of this!

This Week’s Finds in Mathematical Physics (1-50), 242 pages.

These are the first 50 issues of This Week’s Finds of Mathematical Physics. This series has sometimes been called the world’s first blog, though it was originally posted on a “usenet newsgroup” called sci.physics.research — a form of communication that predated the world-wide web. I began writing this series as a way to talk about papers I was reading and writing, and in the first 50 issues I stuck closely to this format. These issues focus rather tightly on quantum gravity, topological quantum field theory, knot theory, and applications of n-categories to these subjects. There are, however, digressions into elliptic curves, Lie algebras, linear logic and various other topics.

Posted at 5:13 PM UTC | Permalink | Followups (30)

## January 3, 2021

### Postdoctoral Position in HoTT at Johns Hopkins University

#### Posted by Emily Riehl

The Department of Mathematics at Johns Hopkins University solicits applications for one two-year postdoctoral fellowship beginning Summer 2021 (with some flexibility in the start and end dates). The position is funded by the Air Force Office of Scientific Research (AFOSR) through the Multidisciplinary University Research Initiative (MURI) program. This position is open to anyone who is able to obtain a visa to come and work in the US, but it is necessary to be physically in the US to receive funding from this grant. (Johns Hopkins will sponsor and pay for a visa application, if required.)

The $n$-Category Café has recently hosted a lively discussion on the ethics of military funded mathematics and US military funding in particular. This is the first time I’ve collaborated on a military funded grant, so I have limited experience in this area. But every year, I’m heartbroken to disappoint the dozens of highly-qualified postdoctoral applicants I come in contact with. My department also offers university-funded postdoctoral positions (though one could argue that military funding provides some support for all employees at Johns Hopkins) but at some point I calculated that it would be “my turn” to make an offer to my first choice candidate exactly once a decade, and I wanted to try to find a way to hire others in the meanwhile.

## January 2, 2021

### Applied Category Theory 2021 Adjoint School

#### Posted by John Baez

Do you want to get involved in applied category theory? Are you willing to do a lot of work and learn a lot? Then this is for you:

There are four projects to choose from, with great mentors. You can see descriptions of them below!

By the way, it’s not yet clear if there will be an in-person component to this school — but if there is, it’ll happen at the University of Cambridge. ACT2021 is being organized by Jamie Vicary, who teaches in the computer science department there.

## December 29, 2020

### Azat Miftakhov

#### Posted by John Baez

Azat Miftakhov is a finishing graduate student in Mathematics at Moscow State University, and is a political activist. In February 2019 he was arrested and charged with terrorist activity and the production of explosives. These charges were quickly dropped, but he is nevertheless still in pre-trial detention, now under the charge of having participated in a group act of vandalism resulting in a broken window on a building belonging to the United Russia party.

Many disturbing signs of violation of his due legal process have been reported by the press and by human rights activists. These include torture, harassment of his relatives by local police, and a smear campaign involving homophobic slurs in the media. He has also been denied access to his scientific work. It is difficult to see how the charge of minor vandalism could warrant a year of pre-trial detention and this mistreatment. “Memorial”, the oldest Russian human rights organization, lists Azat Miftakhov as a political prisoner.

Please join many prominent mathematicians and sign a petition protesting Azat Miftakhov’s treatment here! The text above is not my own, but copied from the American Mathematical Society, who is also protesting this outrage. For more information go here.

Posted at 1:32 AM UTC | Permalink | Followups (4)