On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory

Sammanfattning: Martin Löf Type Theory, having put computation at the center of logical reasoning, has been shown to be an effective foundation for proof assistants, with applications both in computer science and constructive mathematics. One ambition though is for MLTT to also double as a practical general purpose programming language. Datatypes in type theory come with an induction or coinduction principle which gives a precise and concise specification of their interface. However, such principles can interfere with how we would like to express our programs. In this thesis, we investigate more flexible alternatives to direct uses of the (co)induction principles. As a first contribution, we consider the n-truncation of a type in Homo- topy Type Theory. We derive in HoTT an eliminator into (n+1)-truncated types instead of n-truncated ones, assuming extra conditions on the underlying function. As a second contribution, we improve on type-based criteria for termination and productivity. By augmenting the types with well-foundedness information, such criteria allow function definitions in a style closer to general recursion. We consider two criteria: guarded types, and sized types. Guarded types introduce a modality ”later” to guard the availability of recursive calls provided by a general fixed-point combinator. In Guarded Cu- bical Type Theory we equip the fixed-point combinator with a propositional equality to its one-step unfolding, instead of a definitional equality that would break normalization. The notion of path from Cubical Type Theory allows us to do so without losing canonicity or decidability of conversion. Sized types, on the other hand, explicitly index datatypes with size bounds on the height or depth of their elements. The sizes however can get in the way of the reasoning principles we expect. Our approach is to introduce new quantifiers for ”irrelevant” size quantification. We present a type theory with parametric quantifiers where irrelevance arises as a “free theorem”. We also develop a conversion checking algorithm for a more specific theory where the new quantifiers are restricted to sizes. Finally, our third contribution is about the operational semantics of type theory. For the extensions above we would like to devise a practical conversion checking algorithm suitable for integration into a proof assistant. We formal- ized the correctness of such an algorithm for a small but challenging core calculus, proving that conversion is decidable. We expect this development to form a good basis to verify more complex theories. The ideas discussed in this thesis are already influencing the development of Agda, a proof assistant based on type theory.