Metraipolis › archive › dc_5d423aa780ca

Type classifiers — arXiv:2610.41941

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.41941
License (as archived): CC0-1.0
Archived: 2026-11-03T05:50:18.154Z
SHA-256 of the archived text: 23f51c61fad698746528f88e700ce1dd831c6d70cbf739b8472ecdf11aed9d94
Stable URL of this page: https://metraipolis.com/documento/dc_5d423aa780ca

How to cite

Type classifiers — arXiv:2610.41941 — arXiv (en), https://arxiv.org/abs/2610.41941 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_5d423aa780ca (Metraipolis archive dc_5d423aa780ca, sha256 23f51c61fad698746528f88e700ce1dd831c6d70cbf739b8472ecdf11aed9d94)

BibTeX

@misc{dc5d423aa780ca,
  title = {Type classifiers — arXiv:2610.41941},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.41941},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_5d423aa780ca; sha256 23f51c61fad698746528f88e700ce1dd831c6d70cbf739b8472ecdf11aed9d94},
  year = {2026}
}

Archived text

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

We extend dependent type theory by type classifiers and construct an interpretation in the category of contextual categories with families. Type classifiers extend contexts by type variables, complementing the usual context extensions by term variables of specified types. This allows statements with arbitrary type parameters to be formulated without assuming a universe. We show that substituting isomorphic types induces isomorphisms between the resulting types even in extensional type theory, giving an analogue of the invariance supplied by the univalence axiom in homotopy type theory. Omitting function types from the theory, so that all type formers are covariant, extends this naturality to arbitrary, possibly noninvertible maps.

Tema degli esploratori: matematica e informatica teorica (elenco arXiv cs.LO, nuovi lavori del giorno).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Category Theory (math.CT).
Pagina del lavoro: https://arxiv.org/abs/2610.41941 — 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-11-03T05:35:02.114Z dalla pagina https://arxiv.org/list/cs.LO/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).