Two set-based implementations of quotients in type theory

Niccolò Veltri

Institute of Cybernetics at TUT

Thursday, 20 November 2014, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: We present and compare two different implementations of quotient types in Intensional Type Theory. We first introduce quotients as particular inductive types following the extension of Calculus of Constructions with quotient types from Martin Hofmann's 2005 PhD thesis. Then we give an impredicative encoding of quotients. This implementation is reminiscent of Church numerals and more generally of encodings of inductive types in Calculus of Constructions.

Tarmo Uustalu
Last update 18 November 2014