Here are the slides of my talk "The dawn of formalized mathematics" from the 8th European Congress of Mathematics, which is taking place online and in Protorož, Slovenia, from June 20 to 26, 2021:

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.

We use theBurali-Fortiargument to show that, in homotopy type theory and univalent foundations,the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe$\mathcal{U}$ into its successor $\mathcal{U}^+$ is not anequivalence. We also establish this for the types of sets, magmas, monoids andgroups. The arguments in this post are also written inAgda.

It is my pleasure to have the opportunity to speak at the University of Wisconsin Logicseminar. The hosts are graciously keeping the seminar open for everyone.I will speak about a favorite topic of mine:

Speaker: Andrej Bauer (University of Ljubljana)
Location: University of Wisconsin Logic seminar
Time: February 8th 2021, 21:30 UTC (3:30pm CST in Wisconsin, 22:30 CET in Ljubljana)
Video link: the Zoom link is available at the seminar page

Abstract:

According to Felix Klein, “synthetic geometry is that which studies figures as such, without recourse toformulae, whereas analytic geometry consistently makes use of such formulae as can be written down after the adoption ofan appropriate system of coordinates”. To put it less eloquently, the synthetic method axiomatizes geometry directly byconstruing points and lines as primitive notions, whereas the analytic method builds a model, the Euclidean plane, fromthe real numbers.

Do other branches of mathematics posses the synthetic method, too? For instance, what would “synthetic topology” looklike? To build spaces out of sets, as topologists usually do, is the analytic way. The synthetic approach must construespaces as primitive and axiomatize them directly, without any recourse to sets. It cannot introduce continuity as adesirable property of functions, for that would be like identifying straight lines as the non-bending curves.

It is indeed possible to build the synthetic worlds of topology, smooth analysis, measure theory, and computability. Ineach of them, the basic structure – topological, smooth, measurable, computable – is implicit by virtue of permeatingeverything, even logic itself. The synthetic worlds demand an economy of thought that the unaccustomed mind findsfrustrating at first, but eventually rewards it with new elegance and conceptual clarity. The synthetic method is stillfruitfully related to the analytic method by interpretation of the former in models provided by the latter.

We demonstrate the approach by taking a closer look at synthetic computability, whose central axiom states that thereare countably many countable subsets of the natural numbers. The axiom is validated and explained by its interpretationin the effective topos, where it corresponds to the familiar fact that the computably enumerable sets may be computablyenumerated. Classic theorems of computability may be proved in a straightforward manner, without reference to anynotion of computation. We end by showing that in synthetic computability Turing reducibility is expressed in terms ofsequential continuity of maps between directed-complete partial orders.

The slides and the videorecording of the talk are now available.

After a short pause, our next talk in the series will be given by Jamie Vicary, who willpresent a proof assistant in which the proofs are drawn!

Introducing homotopy.io: A proof assistant for geometrical higher category theory

Time: Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)
Location: online at Zoom ID 989 0478 8985
Speaker: Jamie Vicary (University of Cambridge)
Proof assistant: homotopy.io

Abstract:

Weak higher categories can be difficult to work with algebraically,with the weak structure potentially leading to considerable bureaucracy.Conjecturally, every weak infty-category is equivalent to a"semistrict" one, in which unitors and associators are trivial; such asetting might reduce the burden of constructing largeproofs. In this talk, I will present the proof assistant homotopy.io,which allows direct construction of composites in a finitely-generatedsemistrict (infty,infty)-category. The terms of the proof assistanthave a geometrical interpretation as string diagrams, and interactionwith the proof assistant is entirely geometrical, by clicking anddragging with the mouse, completely unlike more traditional computeralgebra systems. I will give an outline of the underlying theoreticalfoundations, and demonstrate use of the proof assistant to constructsome nontrivial homotopies, rendered in 2d and 3d. I will close withsome speculations about the possible interaction of such a system withmore traditional type-theoretical approaches. (Joint work with LukasHeidemann, Nick Hu and David Reutter.)

References:

David Reutter, Jamie Vicary: High-level methods for homotopy construction inassociative n-categories, arXiv:1902.03831preprint, February 2019. homotopy.io at Lab

The preprint version of the paper A general definition of dependent typetheories has finally appeared on the arXiv! Over threeyears ago Peter Lumsdaine invited me to work on thetopic, which I gladly accepted, and dragged my student PhilippHaselwarter into it. We set out to give an answer tothe queation:

What is type theory, precisely?

At least for me the motivation to work on such a thankless topic came from VladimirVoevodsky, who would ask the question to type-theoretic audiences. Some took him to be atroll and others a newcomer who just had to learn more type theory. I was among thelatter, but eventually the question got through to me – I could point to any number ofspecific examples of type theories, but not a comprehensive and mathematically precisedefinition of the general concept.

It is too easy to dismiss the question by claiming that type theory is an open-ended conceptwhich therefore cannot be completely captured by any mathematical definition. Ofcourse it is open-ended, but it does not follow at all that we should not evenattempt to define it. If geometers were equally fatalistic about the open-ended notion ofspace we would never have had modern geometry, topology, sheaves – heck, half of 20thcentury mathematics would not be there!

Of course, we are neither the first nor the last to give a definition of type theory, andthat is how things should be. We claim no priority or supremacy over other definitions andviews of type theory. Our approach could perhaps be described as "concrete" and"proof-theoretic":

One can argue each of the above points, and we have done so among ourselves many times.Nevertheless, I feel that we have accomplished something worthwhile – but the ultimatejudges will be our readers, or lack of them. You are kindly invited to take a look at thepaper.

Download PDF: arxiv.org/pdf/2009.05539.pdf

I should not forget to mention that Peter, with modest help from Philipp and me,formalized almost the entire paper in Coq! See the repositorygeneral-type-theories atGitHub.

I am happy to announce that we are restarting the "Every proof assistants" series of talkswith Anders Mörtberg who will talk about Cubical Agda. Note that we are moving the seminartime to a more reasonable hour, at least as far as the working people in Europe areconcerned.

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types

Time: Thursday, September 17, 2020 from 15:00 to 16:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Anders Mörtberg (Stockholm University)
Proof assistant: Cubical Agda

Abstract:The dependently typed programming language Agda has recently beenextended with a cubical mode which provides extensionality principlesfor reasoning about equality, such as function and propositionalextensionality. These principles are typically added axiomatically toproof assistants based on dependent type theory which disrupts theconstructive properties of these systems. Cubical type theory providesa solution by giving computational meaning to Homotopy Type Theory andUnivalent Foundations, in particular to the univalence axiom andhigher inductive types. In the talk I will discuss how Agda wasextended to a full-blown proof assistant with native support forunivalence and a general schema of higher inductive types. I will alsoshow a variety of examples of how to use Cubical Agda in practice toreason about mathematics and computer science.

The talk video recording is available.

We have more talks in store, but we will space them out a bit to give slots to our local seminar.

We shall finish the semester with a "Every proof assistant" talk by William Bowman.Note that we start an hour later than usual, at 17:00 UTC+2.

Cur: Designing a less devious proof assistant

Time: Thursday, June 25, 2020 from 17:00 to 18:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: William J. Bowman (University of British Columbia)
Proof assistant: Cur

Abstract:

Dijkstra said that our tools can have a profound and devious influence on our thinking. Ifind this especially true of modern proof assistants, with "devious" out-weighing"profound". Cur is an experiment in design that aims to be less devious. The designemphasizes language extension, syntax manipulation, and DSL construction and integration.This enables the user to be in charge of how they think, rather than requiring the user tocontort their thinking to that of the proof assistant. In this talk, my goal is toconvince you that you want similar capabilities in a proof assistant, and explain anddemonstrate Cur's attempt at solving the problem.

The talk video recording and slides with notes and demo code are available.

Upcoming talks: Anders Mörtberg's talk on Cubical Agda will take place in September 2020.

This week shall witness a performance by Conor McBride.

Epigram 2: Autopsy, Obituary, Apology

Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: Epigram 2

Abstract:"A good pilot is one with the same number of take-offs and landings."runs the old joke, which makes me a very bad pilot indeed. The Epigram2 project was repeatedly restarted several times in the late 2000s andnever even reached cruising altitude. This talk is absolutely not anattempt to persuade you to start using it. Rather, it is anexploration of the ideas which drove it: proof irrelevantobservational equality, first class datatype descriptions, nontrivialequational theories for neutral terms. We may yet live to see suchthings. Although the programming language elaborator never happened,the underlying proof engine was accessible via an imperative interfacecalled "Cochon": we did manage some interesting constructions, atleast one of which I can walk through. I'll also explore the reasons,human and technological, why the thing did not survive the long dark.

The video recording of the talk.

Upcoming talks:

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract:redtt is an interactive proof assistant for Cartesian cubical type theory, a version ofMartin-Löf type theory featuring computational versions of function extensionality, higherinductive types, and univalence. Building on ideas from Epigram, Agda, and Idris, redttintroduces a new cubical take on interactive proof development with holes. We will firstintroduce the basics of cubical type theory and then dive into an interactivedemonstration of redtt’s features and its mathematical library.

After this we will catch a first public glimpse of the future of redtt, a new prototypethat our team is building currently code-named “cooltt”: cooltt introduces syntax tosplit on disjunctions of cofibrations in arbitrary positions, implementing the fulldefinitional eta law for disjunction. While cooltt is still in the early stages, italready has full support for univalence and cubical interactive proof development.

The video recording of the talk.

Upcoming talks: