Type Theory with Single Substitutions
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909844479410176 |
|---|---|
| author | Kaposi, Ambrus Xie, Szumi |
| author_facet | Kaposi, Ambrus Xie, Szumi |
| contents | Type theory can be described as a generalised algebraic theory. This automatically gives a notion of model and the existence of the syntax as the initial model, which is a quotient inductive-inductive type. Algebraic definitions of type theory include Ehrhard's definition of model, categories with families (CwFs), contextual categories, Awodey's natural models, C-systems, B-systems. With the exception of B-systems, these notions are based on a parallel substitution calculus where substitutions form a category. In this paper we define a single substitution calculus (SSC) for type theory and show that the SSC syntax and the CwF syntax are isomorphic for a theory with dependent function space and a hierarchy of universes. SSC only includes single substitutions and single weakenings, and eight equations relating these: four equations describe how to substitute variables, and there are four equations on types which are needed to typecheck the other equations. SSC provides a simple, minimalistic alternative to parallel substitution calculi or B-systems for defining type theory. SSC relates to CwF as extensional combinatory calculus relates to lambda calculus: there are more models of the former, but the syntaxes are equivalent. If we have some additional type formers, we show that an SSC model gives rise to a CwF. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_12303 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Type Theory with Single Substitutions Kaposi, Ambrus Xie, Szumi Logic in Computer Science F.4.1 Type theory can be described as a generalised algebraic theory. This automatically gives a notion of model and the existence of the syntax as the initial model, which is a quotient inductive-inductive type. Algebraic definitions of type theory include Ehrhard's definition of model, categories with families (CwFs), contextual categories, Awodey's natural models, C-systems, B-systems. With the exception of B-systems, these notions are based on a parallel substitution calculus where substitutions form a category. In this paper we define a single substitution calculus (SSC) for type theory and show that the SSC syntax and the CwF syntax are isomorphic for a theory with dependent function space and a hierarchy of universes. SSC only includes single substitutions and single weakenings, and eight equations relating these: four equations describe how to substitute variables, and there are four equations on types which are needed to typecheck the other equations. SSC provides a simple, minimalistic alternative to parallel substitution calculi or B-systems for defining type theory. SSC relates to CwF as extensional combinatory calculus relates to lambda calculus: there are more models of the former, but the syntaxes are equivalent. If we have some additional type formers, we show that an SSC model gives rise to a CwF. |
| title | Type Theory with Single Substitutions |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2510.12303 |