Canonicity of the Mahlo Universe

Abstract

The thesis presents a proof of canonicity of the external Mahlo universe using the gluing technique. The used metatheory is an extensional type theory extended with indexed induction-recursion to express the reducibility predicate for the external Mahlo universe. This is motivated by the fact that the Mahlo universe can express certain inductive-recursive definitions and so understanding the metatheory for the external Mahlo universe should help with metatheory for induction-recursion.