Skip to content
DraconiticResearch
Search Sources API
182,549 studies31 sourcesUpdated 52 min ago
PreprintCC BY 4.0arXiv

Univalent Non-Associative Categorical Structures

  • Beatrice Szilvasy
Open at sourcePDFDOICite

Abstract

We study category-like structures in which composition is not associative, especially Munch-Maccagnoni's duploids, in univalent foundations. Included is a definition of what a univalent duploid is: one where isomorphisms of a suitable kind render the objects indistinguishable to the type theory. We show that the existing construction of a duploid from an adjunction is not univalent as a "single-sorted" duploid, and provide a novel construction which is. This work is formalized in the UniMath library for the Rocq proof assistant.

Related

  1. A Non-Dichotomy for CSPs of Stable ω-Categorical Structures
    Manuel Bodirsky, David Bradley-Williams, Ehud Hrushovski +1
    arXivPreprintarXiv licenceFull textLogic & foundationsarXiv
  2. Freely Generated Categorical Structures and Automatic Differentiation, PhD Thesis (Introduction and Conclusion)
    Fernando Lucatelli Nunes
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv
  3. Different approach to certain problems in univalent function theory
    Milutin Obradović, Nikola Tuneski
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsarXiv
  4. Radii of Concavity for Subclasses of Univalent Functions Associated with the Exponential Mapping
    Pradip Das, Nabadwip Sarkar
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsarXiv
  5. Models for dagger (∞,1)-categories III: Univalent flagged dagger (∞,1)-categories and unitarily complete dagger Segal anima
    Keima Akasaka
    arXivPreprintarXiv licenceFull textAlgebra & number theoryGeometry & topologyarXiv

Cite

BibTeXRIS
BibTeX
@misc{szilvasy2026univalent,
  title = {{Univalent Non-Associative Categorical Structures}},
  author = {Beatrice Szilvasy},
  howpublished = {arXiv},
  year = {2026},
  month = nov,
  doi = {10.48550/arxiv.2611.00068},
  eprint = {2611.00068},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2611.00068},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Univalent Non-Associative Categorical Structures
AU  - Beatrice Szilvasy
PY  - 2026
DA  - 2026/11/01
PB  - arXiv
DO  - 10.48550/arxiv.2611.00068
UR  - https://arxiv.org/abs/2611.00068
AB  - We study category-like structures in which composition is not associative, especially Munch-Maccagnoni's duploids, in univalent foundations. Included is a definition of what a univalent duploid is: one where isomorphisms of a suitable kind render the objects indistinguishable to the type theory. We show that the existing construction of a duploid from an adjunction is not univalent as a "single-sorted" duploid, and provide a novel construction which is. This work is formalized in the UniMath library for the Rocq proof assistant.
ER  -