Happy birthday, Dana!
 11 October 2022
 News
Today Dana Scott is celebrating the 90th birthday today. Happy birthday, Dana! I am forever grateful for your kindness and the knowledge that I received from you. I hope to pass at least a part of it onto my students.
On the occasion Steve Awodey assembled selected works by Dana Scott at CMUHoTT/scott
repository. It is an amazing collection of papers that had deep impact on logic, set theory, computation, and programming languages. I hope in the future we can extend it and possibly present it in better format.
As a special treat, I recount here the story the invention of the famous $D_\infty$ model of the untyped $\lambda$calculus. I heard it first when I was Dana's student. In 2008 I asked Dana to recount it in the form of a short interview.
→ continue reading (1 comment)One syntax to rule them all
 20 May 2022
 Talks
I am at the Syntax and Semantics of Type Theory workshop in Stockholm, a kickoff meeting for WG6 of the EuroProofNet COST network, where I am giving a talk “One syntax to rule them all” based on joint work with Danel Ahman.
→ continue readingTwo new doctors!
 12 January 2022
 News
Within a month two of my students defended their theses: Dr. Anja Petković Komel just before Christmas, and Dr. Philipp Haselwarter just yesterday. I am very proud of them. Congratulations!
Philipp's thesis An Effective Metatheory for Type Theory has three parts:

A formulation and a study of the notion of finitary type theories and standard type theories. These are closely related to the general type theories that were developed with Peter Lumsdaine, but are tailored for implementation.

A formulation and the study of contextfree finitary type theories, which are type theories without explicit contexts. Instead, the variables are annotated with their types. Philipp shows that one can pass between the two versions of type theory.

A novel effectful metalanguage Andromeda metalanguage (AML) for proof assistants which uses algebraic effects and handlers to allow flexible interaction between a generic proof assistant and the user.
Anja's thesis Metaanalysis of type theories with an application to the design of formal proofs also has three parts:

A formulation and a study of transformations of finitary type theories with an associated category of finitary type theories.

A userextensible equality checking algorithm for standard type theories which specializes to several existing equality checking algorithms for specific type theories.

A general elaboration theorem in which the transformation of type theories are used to prove that every finitary type theory (not necessarily fully annotated) can be elaborated to a standard type theory (fully annotated one).
In addition, Philipp has done a great amount of work on implementing contextfree type theories and the effective metalanguage in Andromeda 2, and Anja implemented the generic equality checking algorithm. In the final push to get the theses out the implementation suffered a little bit and is lagging behind. I hope we can bring it up to speed and make it usable. Anja has ideas on how to implement transformations of type theories in a proof assistant.
Of course, I am very happy with the particular results, but I am even happier with the fact that Philipp and Anja made an important step in the development of type theory as a branch of mathematics and computer science: they did not study a particular type theory or a narrow family of them, as has hitherto been the norm, but dependent type theories in general. Their theses contain interesting nontrivial metatheorems that apply to large classes of type theories, and can no doubt be generalized even further. There is lots of lowhanging fruit out there.
→ continue readingIs every projective setoid isomorphic to a type?
 12 January 2022
 Constructive mathematics, Type theory, Formalization
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)The proposal for a proof assistants StackExchange site
 20 November 2021
 General, Proof assistant
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)The dawn of formalized mathematics
 24 June 2021
 Talks, Formalization
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 topleft corner.
 Slides with speaker notes (PDF). Unfortunately, Keynote does not make the hyperlinks active when exporting PDF.
 Video recording of the talk.
Computing an integer using a Grothendieck topos
 18 May 2021
 Constructive mathematics, Type theory, Formalization
A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,
 we developed our mathematics constructively,
 we formalized our mathematics in MartinLöf type theory, in Agda notation,
 we pressed a button, and
 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 readingThe BuraliForti argument in HoTT/UF
 22 February 2021
 Type theory, Constructive mathematics
This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.
We use the BuraliForti 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 readingSynthetic mathematics with an excursion into computability theory
 03 February 2021
 Talks, Synthetic computability
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 mathematics with an excursion into computability theory
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 to formulae, whereas analytic geometry consistently makes use of such formulae as can be written down after the adoption of an appropriate system of coordinates”. To put it less eloquently, the synthetic method axiomatizes geometry directly by construing points and lines as primitive notions, whereas the analytic method builds a model, the Euclidean plane, from the real numbers.
Do other branches of mathematics posses the synthetic method, too? For instance, what would “synthetic topology” look like? To build spaces out of sets, as topologists usually do, is the analytic way. The synthetic approach must construe spaces as primitive and axiomatize them directly, without any recourse to sets. It cannot introduce continuity as a desirable property of functions, for that would be like identifying straight lines as the nonbending curves.
It is indeed possible to build the synthetic worlds of topology, smooth analysis, measure theory, and computability. In each of them, the basic structure – topological, smooth, measurable, computable – is implicit by virtue of permeating everything, even logic itself. The synthetic worlds demand an economy of thought that the unaccustomed mind finds frustrating at first, but eventually rewards it with new elegance and conceptual clarity. The synthetic method is still fruitfully 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 there are countably many countable subsets of the natural numbers. The axiom is validated and explained by its interpretation in the effective topos, where it corresponds to the familiar fact that the computably enumerable sets may be computably enumerated. Classic theorems of computability may be proved in a straightforward manner, without reference to any notion of computation. We end by showing that in synthetic computability Turing reducibility is expressed in terms of sequential continuity of maps between directedcomplete partial orders.
The slides and the video recording of the talk are now available.
→ continue readingEvery proof assistant: introducing homotopy.io – a proof assistant for geometrical higher category theory
 24 November 2020
 Talks, Every proof assistant
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!
→ continue readingIntroducing 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.ioAbstract:
Weak higher categories can be difficult to work with algebraically, with the weak structure potentially leading to considerable bureaucracy. Conjecturally, every weak inftycategory 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 finitelygenerated 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 typetheoretical approaches. (Joint work with Lukas Heidemann, Nick Hu and David Reutter.)
References:
 David Reutter, Jamie Vicary: Highlevel methods for homotopy construction in associative ncategories, arXiv:1902.03831 preprint, February 2019.
 homotopy.io at Lab