Two new papers have recently appeared online:
- Brouwer’s fixed-point theorem in real-cohesive homotopy type theory by me, and
- Adjoint logic with a 2-category of modes, by Dan Licata with a bit of help from me.
Both of them have fairly chatty introductions, so I’ll try to restrain myself from pontificating at length here about their contents. Just go read the introductions. Instead I’ll say a few words about how these papers came about and how they are related to each other.
Cohesive homotopy type theory is something that I’ve been working on with Urs Schreiber since some 3-4 years ago, involving an adjoint string of modalities ʃ
In March I gave a talk about this at CMU, in which I introduced an enhancement of cohesive HoTT called “real-cohesive HoTT” and proved in it that the “shape” ʃ (the cohesive incarnation of the fundamental
The problem with cohesive type theory is that the comodality
There followed a very productive back-and-forth in which Dan developed the metatheory with an eye towards a proof-theoretically well-behaved calculus, while I cast around for a version of the theory that would make for a perspicuous presentation of real-cohesion. We ended up with an idea for a very general kind of “adjoint type theory”, which is not yet worked out in full; the real-cohesion paper uses only one particular case of it, while the adjoint logic paper develops the metatheory of the general case but in a very simplified way (no dependent types and only one-variable contexts).
Dan coded up a simple sequent calculus for this theory in Agda and proved some nice theorems about it. Meanwhile I generalized it to dependent type theory in the special case of cohesion and used it to write up the two circles theorem, and also a synthetic version of the classical homotopy-theoretic proof of Brouwer’s fixed-point theorem as a proof of concept. I’m very excited about real-cohesion, and also adjoint type theory more generally; I think it has a lot of untapped potential. A few possibilities are mentioned in the paper.
Unfortunately there is one fly in the ointment: cohesive type theory done in this way can’t be formalized directly in existing proof assistants. One can describe the theory using a proof assistant as the metatheory, of course. For actually proving things in the theory, this works pretty well for basic theorems in a 1-variable sequent calculus (see the Agda code accompanying the adjoint logic paper), but for more complicated results in a richer language it would become quite tedious, running into the common problems with representing languages with variable binding and dependent types. At one point I entertained notions that Coq’s modules would help; but at the moment I’m kind of down on that idea because modules have a lot of “features” that make them at best annoying to use in this way (which, to be fair, is not at all how they were intended to be used). So formalization may have to wait until someone implements an adjoint-type-theory proof assistant directly. (Anyone developing a proof assistant feel like incorporating it?)