nLab nPOV




Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Category theory

Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations

Wikipedia enforces its entries to adopt an NPOV – a neutral point of view. This is appropriate for an encyclopedia.

However, the nLab is not Wikipedia, nor is it an encyclopedia, although it does aspire to provide a useful reference in many areas (among its other purposes). In particular, the nnLab has a particular point of view, which we may call the nnPOV, the higher algebraic, homotopical, or n- categorical point of view.

To some extent the nnPOV is just the observation that higher algebra, homotopy theory, type theory, category theory and higher category theory, have a plethora of useful applications.



Around the nLab it is believed that higher algebra, homotopy theory, type theory, category theory and higher category theory provide a point of view on Mathematics, Physics and Philosophy which is a valuable unifying point of view for the understanding of the concepts involved.

So at the nnLab, we don’t care so much about being neutral. Although we don’t want to offend people unnecessarily, we are also not ashamed about writing from this particular point of view. There are certainly other valid points of view on mathematics, but describing them and being neutral towards them is not the purpose of the nnLab. Rather, the nnLab starts from the premise that higher algebra, homotopy theory, type theory, category theory and higher category theory are a true and useful point of view, and one of its aims is to expose this point of view generally and in a multitude of examples, and thereby accumulate evidence for it.

If you feel skeptical about the nn-point of view, you may want to ignore the nnLab. Or you may want to take its content as a contribution to a discussion on what is behind the claim that higher algebra, homotopy theory, type theory, and/or category theory is the right language to describe the world, or at least the world of mathematical ideas.

Category theory

As recalled in parts on the page on category theory, category theorists have early on, beginning in the 1960s, proclaimed the advantages of category theory over other points of view. It has been observed that this claim, or at least the way it has been put forward, has contributed to a certain alienation of category theory in parts of the mathematical community. That may be true and is understandable. But since a claim is not false just because it is put forward with possibly unpleasant boldness, all evidence for the claim deserves to be collected and exposed. We hope the nnLab to play a role in this effort.

In particular, there have been dramatic developments since the 1960s. Back then promoting category theory may have been as visionary as the invention of complex numbers was in the 16th century. But just as the early rejections of the complex numbers appear strangely out of place from today’s perspective, where their ubiquity proves their reality to the point that it is hard to imagine how life must have been before their conception, so developments of category theory and its applications in the last years have in many areas brought it to the point that rejecting its prevalence amounts (we believe) to rejecting the obvious and ubiquitous. But also mathematics as a whole has drastically grown since then, and while category theory has become an entirely obvious ingredient in areas such as homotopy theory, homological algebra, algebraic geometry and even fields like topological quantum field theory, its similar role to be played in many other areas has often not found wide recognition yet. But this is gradually changing.

Higher algebra/Homotopy theory/Type theory

From the perspective of higher algebra, homotopy theory, and type theory, the fundamental objects of mathematics are homotopy types or \infty -groupoids, and the nn-truncated versions of them, the n n -groupoids, due to their differing treatment of equality/equivalence of such objects. This perspective is somewhat different from the perspective of category theory, as category theory takes nn-categories to be more fundamental than nn-groupoids, while these branches of mathematics view nn-categories merely as nn-groupoids with additional higher structure on top of the core nn-groupoid. In particular, nn-categories are merely specific kinds of directed ( n , r ) (n,r) -graphs.

On the other hand, from this perspective, if one were to take the directed structure to be more fundamental as one does in category theory, then the fundamental structures would end up being nn-posets rather than nn-categories; in particular, taking preorder to be more fundamental than equivalence relations/equality.

The role of the nnPOV

Category theory

Practitioners of category theory have often attempted to express the striking power of category theory (or general conceptual methods), sometimes through aphorism, sometimes through metaphor. Early on, Peter Freyd wrote

Perhaps the purpose of categorical algebra is to show that which is trivial is trivially trivial.

This can be taken to mean that one thing category theory does is help make the softer bits seem utterly natural and obvious, so as to quickly get to the heart of the matter, isolating the hard nuggets, which one may then attack with abandon. This is an invaluable service category theory performs for mathematics; therefore, category theory is plain good pragmatics.

However, it is also possible to take it a step beyond the pragmatic attitude, and see category theory (and now higher category theory) as exemplifying a style for doing even hard mathematics, as in the style for which Grothendieck is renowned. Paraphrasing from Colin McLarty’s excellent essay, let us regard the aforementioned pragmatic attitude as leading up to the hammer-and-chisel principle: if you think of a theorem to be proved as a nut to be opened, so as to reach “the nourishing flesh protected by the shell” (Grothendieck), then one thing to do is “put the cutting edge of the chisel against the shell and strike hard. If needed, begin again at many different points until the shell cracks – and you are satisfied.” Grothendieck points to Serre as a master of this technique. He then says:

I can illustrate the second approach with the same image of a nut to be opened. The first analogy which came to my mind is of immersing the nut in some softening liquid, and why not simply water? From time to time you rub so the liquid penetrates better, and otherwise you let time pass. The shell becomes more flexible through weeks and months – when the time is ripe, hand pressure is enough, the shell opens like a perfectly ripened avocado!

A different image came to me a few weeks ago. The unknown thing to be known appeared to me as some stretch of earth or hard marl, resisting penetration… the sea advances insensibly in silence, nothing seems to happen, nothing moves, the water is so far off you hardly hear it… yet it finally surrounds the resistant substance. (Translated from the French by McLarty)

This arresting metaphor of “la mer qui monte” (“the rising sea”), which over time changes the very form of the resistant substance, is very much in the style of Grothendieck himself. McLarty quotes Deligne as saying that a typical Grothendieck proof consists of a long series of trivial steps where “nothing seems to happen, and yet at the end a highly non-trivial theorem is there.”


For an (incomplete) list of examples of topics for which the nnPOV has proven to be a useful perspective, see

category: meta

Last revised on May 16, 2022 at 17:10:44. See the history of this page for a list of all contributions to it.