{"id":"arxiv/2611.00068","url":"https://arxiv.org/abs/2611.00068","tags":["cs.LO","cs.PL","math.CT"],"score":0,"title":"Univalent Non-Associative Categorical Structures","domain":"cs.LO","source":"arxiv","authors":["Beatrice Szilvasy"],"reviews":0,"subject":"cs.LO","summary":"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.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-10-15","reactions":{}}