Abstract
The logic of higher categories (or ∞-categories) is a variation of type theory, which is homotopic in nature and in which the notion of category is the primitive concept - the one that is never defined! An adequate generalization of Voevodsky's axiom of univalence makes this theory a highly expressive language, sufficiently so that it can produce its own semantic interpretations. This provides a mathematical foundation system at the heart of which the concepts of category theory and homotopy theory are implemented. A logic of logics. A semantic interpretation of this logic is produced in classical mathematics by the theory of ∞-categories as developed by Joyal and Lurie. A formulation in dependent type theory, via Riehl-Shulman theory, is the subject of a current project by Buchholtz and Weinberger. This logic makes it possible to formulate constructively many theories considered as advanced (e.g. spread cohomology of derived or non-derivative schemes, derived categories of quasi-coherent bundles) in a way close to practice. It's also a new way of apprehending logic itself, so that the distance between syntax and semantics is apparently very significantly reduced: logics are terms of a type, i.e. objects of an ∞-category.
