Weak omega-categories from intensional type theory (Q2786141)

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 \textit{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.NEWLINENEWLINEDeveloping 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.NEWLINENEWLINEIt has been suggested earlier (the idea can be traced back to [\textit{M. Hofmann} and \textit{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 \textit{M. A. Batanin} [Adv. Math. 136, No. 1, 39--103 (1998; Zbl 0912.18006)]. A proof of similar results was proposed independently by \textit{B. van den Berg} and \textit{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.NEWLINENEWLINEBesides 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. [\textit{V. Voevodsky}, Lect. Notes Comput. Sci. 7086, 70 (2011; Zbl 1250.03121)]).