Idempotents in intensional type theory
We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents ca...
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Artigo |
| Langue: | Inglês |
| Publié: |
Logical Methods in Computer Science e.V.
2017-04-01
|
| Collection: | Logical Methods in Computer Science |
| Sujets: | |
| Accès en ligne: | https://lmcs.episciences.org/2027/pdf |
| Tags: |
Pas de tags, Soyez le premier à ajouter un tag!
|