Erased Postulates, Identity Types and Quotients

Nils Anders Danielsson

This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a progra…