Mathematics and Computation

Jacques Carette asked on Twitter for a refence to the fact that countable choice holds in setoids. I then spent a day formalizing facts about the axiom of choice in setoids in Agda. I noticed something interesting that is worth blogging about.

→ continue reading (4 comments)

Proof assistant communities have grown quite a bit lately. They have active Zulip chats: Lean, Coq, Agda, Isabelle. These are good for discussions, but less so for knowledge accumulation and organization, and are not indexed by the search engines.

I have therefore created a proposal for a new “Proof assistants” StackExchange site. I believe that such a site would complement very well various Zulips dedicated to specific proof assistants. If you favor the idea, please support it by visiting the proposal and

• becoming a follower (you have to be a registered user with a verified email account),
• asking sample questions, and
• upvoting good sample questions.

To pass the first stage, we need 60 followers and 40 questions with at least 10 votes to proceed to the next stage.

→ continue reading (2 comments)

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:

• Keynote presentation, viewable online in your browser. Turn on the speaker notes by clicking on the rectangular icon in the top-left corner.
• Slides with speaker notes (PDF). Unfortunately, Keynote does not make the hyperlinks active when exporting PDF.
• Video recording of the talk.

→ continue reading (3 comments)

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

1. we developed our mathematics constructively,
2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
3. we pressed a button, and
4. after a few seconds we saw the integer we expected in front of us.

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

→ continue reading

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

We use the Burali-Forti argument 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 an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.

→ continue reading

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

→ continue reading

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present 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 a setting might reduce the burden of constructing large proofs. In this talk, I will present the proof assistant homotopy.io, which allows direct construction of composites in a finitely-generated semistrict (infty,infty)-category. The terms of the proof assistant have a geometrical interpretation as string diagrams, and interaction with the proof assistant is entirely geometrical, by clicking and dragging with the mouse, completely unlike more traditional computer algebra systems. I will give an outline of the underlying theoretical foundations, and demonstrate use of the proof assistant to construct some nontrivial homotopies, rendered in 2d and 3d. I will close with some speculations about the possible interaction of such a system with more traditional type-theoretical approaches. (Joint work with Lukas Heidemann, Nick Hu and David Reutter.)

References:

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

→ continue reading

The preprint version of the paper A general definition of dependent type theories has finally appeared on the arXiv! Over three years ago Peter Lumsdaine invited me to work on the topic, which I gladly accepted, and dragged my student Philipp Haselwarter into it. We set out to give an answer to the queation:

What is type theory, precisely?

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

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

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

1. We wanted to stay close to traditional syntax.
2. We gave a complete and precise definition.
3. We aimed for a level of generality that allows useful meta-theory of a wide range of type theories.

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 ultimate judges will be our readers, or lack of them. You are kindly invited to take a look at the paper.

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 repository general-type-theories at GitHub.

→ continue reading

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

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 been extended with a cubical mode which provides extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically to proof assistants based on dependent type theory which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. In the talk I will discuss how Agda was extended to a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. I will also show a variety of examples of how to use Cubical Agda in practice to reason 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.

→ continue reading

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. I find 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 design emphasizes 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 to contort their thinking to that of the proof assistant. In this talk, my goal is to convince you that you want similar capabilities in a proof assistant, and explain and demonstrate 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.

→ continue reading