Univalent Models of a Non-Associative Composition

My master’s thesis1 at the University of Cambridge, supervised by Jon Sterling. Click here to download for print or on-screen viewing.

Abstract

Mixing call-by-name and call-by-value evaluation orders in a single programming language gives rise to a composition which is non-associative. To model such semantics, one may use Munch-Maccagnoni’s duploids, category-like structures that relax the associativity of composition. We study and formalize duploids in homotopy type theory/univalent foundations. Our work includes a definition of what it means for a duploid to be univalent: that 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 fails to be 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.

Bibtex

@mastersthesis{Szilvasy26,
  author={Beatrice Szilvasy},
  title={Univalent Models of a Non-Associative Composition},
  school={University of Cambridge},
  year={2026},
  month={June},
  url={https://eutro.dev/share/umac.pdf}
}

Footnotes:

1

Or rather, the report for my “Part III Project”.