OAI.Thomason.nerveDetection_allDimensions

The theorem states that the Thomason weak equivalences on strict ω-categories are exactly the morphisms detected by the Street nerve, in every dimension. Here a morphism of simplicial sets is a simplicial weak equivalence when its geometric realization (the image under the functor from simplicial sets to topological spaces) is a weak homotopy equivalence. The Thomason weak equivalences of ω-categories are defined as the morphisms sent to simplicial weak equivalences by thomasonRight, which is the Street nerve functor from ω-categories to simplicial sets followed by two applications of the Ex functor. The first conclusion is that this class equals the class of ω-functors whose Street nerve alone is a simplicial weak equivalence, so the two applications of Ex can be dropped. The second conclusion is the same statement for each natural number n for the full subcategory of n-truncated ω-categories: the finite-dimensional Thomason weak equivalences, defined through the corresponding finite thomasonRightFinite n (the Street nerve on n-categories followed by Ex twice), coincide with the morphisms of n-categories whose Street nerve is a simplicial weak equivalence. The statement is proved by sorry in the source.