Abstract:The formalization of mathematical language traditionally relies on undefined terms - such as Set, Type, universes - whose properties are specified by axioms and inference rules. In this talk, I present an alternative approach in which mathematical language is entirely built from definitions. At its core are n-category constructors - an internal alternative to typing judgments - denoted as $(X : Cat_n)$ for a variable $X$, which are inductively assigned a truth value - a meaning. Defining an n-category here consists of constructing an element (a proof) of the corresponding truth value. To give meaning to these constructors, $(n-1)$-categories and $(n-1)$-functors are inductively organised as an $n$-category, resulting in a graded structure of nested $n$-categories $({Cat}_{n-1} : Cat_n)$. By treating each mathematical object as an element of another object, this framework offers a natural and expressive language for higher category theory, set theory, and logic, all with vast generalisation potential. I will discuss key consequences of this approach, including its implications for fundamental notions such as sameness, size, and ∞-categories, as well as its connexions to homotopy type theory.