Path Types in Algebraic Type Theory
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911366163464192 |
|---|---|
| author | Awodey, Steve Hua, Joseph |
| author_facet | Awodey, Steve Hua, Joseph |
| contents | 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 specification of a model with \emph{path types}. The interval is also used to specify a (Hurewicz) fibration structure on the universe of the model. It is shown that the combination of these two conditions suffices to model the intensional identity rules, assuming only finite limits. The addition of an interval also relates the current treatment to that of cubical type theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_06567 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Path Types in Algebraic Type Theory Awodey, Steve Hua, Joseph Category Theory Algebraic Topology Logic 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 specification of a model with \emph{path types}. The interval is also used to specify a (Hurewicz) fibration structure on the universe of the model. It is shown that the combination of these two conditions suffices to model the intensional identity rules, assuming only finite limits. The addition of an interval also relates the current treatment to that of cubical type theory. |
| title | Path Types in Algebraic Type Theory |
| topic | Category Theory Algebraic Topology Logic |
| url | https://arxiv.org/abs/2601.06567 |