Posts in the year 2022
Two 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)