Weak omega-categories from intensional type theory. (English) Zbl 1250.03127
The aim of the paper is to show that for any type in Martin-Löf intuitionistic type theory, the terms of this type and its higher identity types form a weak \(\omega\)-category in the sense of T. Leinster [Theory Appl. Categ. 10, 1–70 (2002; Zbl 0987.18007)]. In the globular approach to higher categories, the objects of a higher category are \(0\)-cells, the arrows between objects are \(1\)-cells, there are \(2\)-cells considered as arrows between arrows \(\mathrm{etc}\)., all these data subject to appropriate composition operations and laws that depend on the kind of category under consideration (strict or weak, \(n\)- or \(\omega\)-). As the author outlines, the paradigm for semantics of type theory is roughly that types (or contexts) are thought of as objects \([|A|]\), terms \(x:A\vdash \tau(x):B\) as arrows \([|\tau|]: [|A|]\rightarrow [|B|]\), terms of identity type \(\rho: \mathrm{Id}_B(\tau, \tau')\) as \(2\)-cells etc.
Developing this idea, the author uses a syntactical approach, { i.e.}, investigation of the structures formed by the syntax of type theory, based on the methods of structural proof theory.
It has been suggested earlier (the idea can be traced back to [M. Hofmann and T. Streicher, Oxf. Logic Guides 36, 83–111 (1998; Zbl 0930.03089)]) that the terms of any type considered together with its higher identity types should carry the structure of a weak \(\omega\)-category or an \(\omega\)-groupoid. The paper provides a proof of this hypothesis. It uses the definition of weak \(\omega\)-category by Leinster [loc. cit.] that follows the approach of M. A. Batanin [Adv. Math. 136, No. 1, 39–103 (1998; Zbl 0912.18006)]. A proof of similar results was proposed independently by B. van den Berg and R. Garner [Proc. Lond. Math. Soc. (3) 102, No. 2, 370–394 (2011; Zbl 1229.18007)]. Their proof is based rather on the use of category-theoretical methods. A detailed comparison of the two proofs is given at the end of the present paper.
Besides the proof of a hypothesis concerning weak \(\omega\)-structure that is of interest in itself, the paper is interesting in the context of recent developments concerning the so-called univalent foundations program (cf. [V. Voevodsky, Lect. Notes Comput. Sci. 7086, 70 (2011; Zbl 1250.03121)]).
Developing this idea, the author uses a syntactical approach, { i.e.}, investigation of the structures formed by the syntax of type theory, based on the methods of structural proof theory.
It has been suggested earlier (the idea can be traced back to [M. Hofmann and T. Streicher, Oxf. Logic Guides 36, 83–111 (1998; Zbl 0930.03089)]) that the terms of any type considered together with its higher identity types should carry the structure of a weak \(\omega\)-category or an \(\omega\)-groupoid. The paper provides a proof of this hypothesis. It uses the definition of weak \(\omega\)-category by Leinster [loc. cit.] that follows the approach of M. A. Batanin [Adv. Math. 136, No. 1, 39–103 (1998; Zbl 0912.18006)]. A proof of similar results was proposed independently by B. van den Berg and R. Garner [Proc. Lond. Math. Soc. (3) 102, No. 2, 370–394 (2011; Zbl 1229.18007)]. Their proof is based rather on the use of category-theoretical methods. A detailed comparison of the two proofs is given at the end of the present paper.
Besides the proof of a hypothesis concerning weak \(\omega\)-structure that is of interest in itself, the paper is interesting in the context of recent developments concerning the so-called univalent foundations program (cf. [V. Voevodsky, Lect. Notes Comput. Sci. 7086, 70 (2011; Zbl 1250.03121)]).
Reviewer: Serguei V. Solov’ev (Toulouse)
MSC:
| 03G30 | Categorical logic, topoi |
| 03F50 | Metamathematics of constructive systems |
| 18D50 | Operads (MSC2010) |
