fixed bad wiki link from prev edit
Peter LeFanu Lumsdaine
]]>Added clarification about Lumsdaine–Shulman usage, to forestall confusion
Peter LeFanu Lumsdaine
]]>Added more examples and a properties section, and also some discussion of Lawson’s proof that the invertibility hypothesis is redundant.
]]>I’m not sure what I think about this proof. It seems to go like this:
Part of me feels as though the use of simplicial and cubical sets ought to be -reducible out of this proof to obtain a proof that actually works directly with an otherwise-excellent model category. But another part of me finds it a pleasing application of the “classifier principle” that if you can find a universal object with some structure (e.g. classifying space, classifying topos, syntactic category of a type theory), then working directly with that universal object can be an easier way to prove that something holds in all such structures.
]]>Nice, thanks! Do you feel like updating the page?
]]>Added an explanation of how the DK result implies that sSet is excellent.
]]>Add missing axiom that weak equivalences are stable under filtered colimits
]]>