Welcome!

You're looking at the (-2)Lab, a formalized reference for (-2)-category theory and a natural extension of the equally fantastic 1Lab and nLab projects. In a similar bid for maximal formalism, any definition or theorem will be accompanied by one or more listings of code for the Agda proof assistant which provide machine-checkable justification for the claims. The hope is that this will serve as a useful resource for working (-2)-category theorists, as well as a handy educational tool for beginners or interested persons from other fields.

The content on the (-2)Lab is organized into articles, each of which covers one particular concept in as much detail as possible. As concepts in mathematics tend to have complex interdependencies in both definition and proof, articles covering those concepts will prefer to hyperlink to each other rather than duplicating content. Each individual article is structured as a series of definitions, each followed by proofs of relevant theorems regarding those definitions. At the end of each article, a list of hyperlinks to articles on related concepts is provided. In this way, the (-2)Lab forms a sort of graph structure, where each article constitutes a vertex and each hyperlink constitutes an edge.

To enter the graph and begin your exploration of the (-2)Lab, check out the article on the foundational concept of (-2)-category theory: the (-2)-category.