3 papers
cs.LO2026
Polynomial Universes in Homotopy Type Theory
C. B. Aberlé, David I. Spivak
Awodey, later with Newstead, showed how polynomial functors with extra structure (termed ``natural models'') hold within them the categorical semantics for dependent type theory. T…
cs.LO2025
Substructural Parametricity
C. B. Aberlé, Chris Martens, Frank Pfenning
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary lo…
cs.LO2024
Parametricity via Cohesion
C. B. Aberlé
Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In re…