{"id":"arxiv/2601.06567","url":"https://arxiv.org/abs/2601.06567","tags":["math.CT","math.AT","math.LO"],"score":0,"title":"Path Types in Algebraic Type Theory","domain":"math.CT","source":"arxiv","authors":["Steve Awodey","Joseph Hua"],"reviews":0,"subject":"math.CT","summary":"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 of \\emph{extensional} identity types in the original presentation of natural models paralleled that of the other type formers $Σ$ and $Π$, but the treatment of the \\emph{intensional} case there was less uniform. It was later reformulated to an account based on polynomials; here a further improvement in the style of the other type formers is achieved by employing an interval, in order to give a single pullback…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-01-10","reactions":{}}