Univalent Non-Associative Categorical Structures
Source: arxiv.org/abs/2611.00068
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2611.00068
curl -X POST /api/v1/records/arxiv/2611.00068/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2611.00068/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'