Institute of Information Science, Academia Sinica

In a total programming language, such as the dependently typed functional language Agda, every program is required to terminate. This makes it easier to reason about program behaviour, and also means that programs can express proof information a la constructive logic -- Agda can also be used as a proof assistant. However, it can sometimes be difficult to prove that a program you have written actually always terminates. In traditional mathematics built on classical logic and set-theory, so-called ordinals can be used to show that processes terminate, so it would be great to convert the theory of ordinals to constructive logic, so that they could be used to prove more programs terminating and thus expressible in for example Agda. Developing ordinal theory in a constructive setting comes with additional challenges, though, as many classically equivalent definitions and constructions of ordinals split apart constructively, with different advantages and disadvantages for each. I will give an introduction to a few different notions of ordinals in the context of homotopy type theory, tell you which one is useful for what, and how they relate. The use of concepts from homotopy type theory such as the univalence axiom and quotient inductive types sometimes crucial for the developments, but I will not assume that the audience is familiar with either homotopy type theory or the classical theory of ordinals.
This is joint work with Tom de Jong, Nicolai Kraus, and Chuangjie Xu.