mathlib3 documentation


The nerve of a category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the definition of the nerve of a category C, which is a simplicial set nerve C (see [GJ09], Example I.1.4).

References #

The nerve of a category, as a functor Cat ⥤ sSet