3 papers
math.CT2026
Internal Algebraic Type Theory
Joseph Hua
This thesis brings us closer to applying computer-assisted, internal, type-theoretic reasoning to a category, with examples in the category of cubical sets, the category of groupoi…
math.CT2026
Polynomial functors in Ï-clans for the semantics of type theory
Joseph Hua, Yiming Xu
The category of contexts underlying a model of Martin-Löf type theory with Unit-, -, and -types need not be locally Cartesian closed, but is necessarily a -clan. We ex…
math.CT2026
Path Types in Algebraic Type Theory
Steve Awodey, Joseph Hua
A new approach to the semantics of identity types in intensional Martin-Löf type theory is proposed, assuming only a category with finite limits and an interval. The specification…