Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Nice, thanks! Do you feel like updating the page?
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.
1 to 8 of 8