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.