Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 19 min ago
PreprintCC BY 4.0arXiv

Type classifiers

  • Martin E. Bidlingmaier
Open at sourcePDFDOICite

Abstract

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.

Related

  1. Ensemble-based support vector machine classifiers as an efficient tool for quality assessment of beef fillets from electronic nose data
    Fady Mohareb, Olga Papadopoulou, Efstathios Panagou +2
    Analytical MethodsPeer-reviewedCC BYFull text60 citedGeneral biologyStatisticsHAL
  2. Local Discrimination of Binary Classifiers via Localized AUC Functional
    Wenye Ren, Anna Győrffy-Kerekes, Tancredi Dorsi +1
    arXivPreprintarXiv licenceFull textStatisticsarXiv
  3. Efficient Support Recovery of Mixtures of Sparse Linear Classifiers with Fewer Measurements
    Xiaxin Li, Arya Mazumdar
    arXivPreprintCC BY 4.0Full textGeneral mathematicsarXiv
  4. The Blind Spot Paradox: When Adaptive Classifiers Defeat Drift Detectors
    Raphaël Minato, Fabrice Popineau, Arpad Rimmel +1
    arXivPreprintarXiv licenceFull textStatisticsarXiv
  5. Propagate, Then Sharpen: Post-Hoc Refinement of Frozen Node Classifiers
    Preben Johnsen Bentdal, Nello Blaser, Xue-Cheng Tai
    arXivPreprintCC BY 4.0Full textStatisticsarXiv

Cite

BibTeXRIS
BibTeX
@misc{bidlingmaier2026type,
  title = {{Type classifiers}},
  author = {Martin E. Bidlingmaier},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.41941},
  eprint = {2610.41941},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.41941},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Type classifiers
AU  - Martin E. Bidlingmaier
PY  - 2026
DA  - 2026/10/30
PB  - arXiv
DO  - 10.48550/arxiv.2610.41941
UR  - https://arxiv.org/abs/2610.41941
AB  - 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.
ER  -