Metraipolis › archive › dc_2ea319bbaef9

Erased Postulates, Identity Types and Quotients — arXiv:2609.08578

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.08578
License (as archived): CC0-1.0
Archived: 2026-10-16T15:40:03.179Z
SHA-256 of the archived text: 872f82daf025032bdf7e11e684220a00ffd403cc209080d4ded611d17a4ab2bd
Stable URL of this page: https://metraipolis.com/documento/dc_2ea319bbaef9

How to cite

Erased Postulates, Identity Types and Quotients — arXiv:2609.08578 — arXiv (en), https://arxiv.org/abs/2609.08578 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_2ea319bbaef9 (Metraipolis archive dc_2ea319bbaef9, sha256 872f82daf025032bdf7e11e684220a00ffd403cc209080d4ded611d17a4ab2bd)

BibTeX

@misc{dc2ea319bbaef9,
  title = {Erased Postulates, Identity Types and Quotients — arXiv:2609.08578},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.08578},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_2ea319bbaef9; sha256 872f82daf025032bdf7e11e684220a00ffd403cc209080d4ded611d17a4ab2bd},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.08578. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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 program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-09-09 in cs.LO).
Categorie arXiv: Programming Languages (cs.PL) ; Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2609.08578 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-16T15:30:57.145Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-09-09?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).