Delphi.science

Type classifiers

Martin E. Bidlingmaier

arXivarxiv/2610.41941Oct 30, 2026cs.LOscore 0

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.…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2610.41941
curl -X POST /api/v1/records/arxiv/2610.41941/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.41941/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'