Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
I do use $\Delta$-generated spaces, it is written in the post and therefore all categories are locally presentable. Noone never saw Jeff Smith's argument and some mathematicians I know doubt that he has such an argument. And indeed not all objects are cofibrant, So Olschok's theory cannot be applied. It is a different configuration.
It's a old question (almost 2-y old). As a comment, I would say that to the best of my knowledge, there is no formalization of Bourbaki with a proof assistant (but I may be wrong). Concerning this kind of topological argument, the proof assistant Mizar (mizar.org) should have it in its library.
"Because for many important categories, the most natural presentation gives non-disjoint homsets." (like for the category of sets). No it is wrong at least for me :-). A set map consists of a triple $(X,Y,f)$ where $f$ is a subset of $X\times Y$ such that $(x,y)\in f$ and $(x,y')\in f$ implies $y=y'$.
@MahdiMajidi-Zolbanin I wrote my comment before reading the answer. It is the paragraph "Why might you want the disjointness condition?" about well-defined domain and codomain functions.
At least for small categories (I don't want to run into size issues), there is a well-defined set map called "source of a morphism". So $\mathrm{Id}_X=\mathrm{Id}_Y$ implies $X=Y$ and of course $X=Y$ implies $\mathrm{Id}_X=\mathrm{Id}_Y$...
After reading this answer, I believe now that VP could be inconsistent with ZFC (before reading it, I was convinced, I mean I believed, that VP was consistent with ZFC). In 8 years, did something new happen in a direction of a proof of either consistency or inconsistency ?
I am not physicist. I'd would like to point out anyway that maybe gravity does not exist at the Plank scale just because gravity is an emergent property of spacetime, not a fundamental force. That would imply that quantum mechanics and general relativity cannot be unified because there would be nothing to unify. Some physicists reading my comments will be certainly able to explain better than I can this new (emergent !) point of view in theoretical physics.
The answer is already in your question. The last sentence means geometrically that you're considering a cubical set with the two families of connections and you replace each cube by the simplex which is "orthogonal" to the direction $(0,...,0)\to (1,...,1)$ which is close to $(0,...,0)$.
What is the $n$-directed simplex ? Simplicial sets have something directed in their definition (unlike symmetric simplicial sets). So is it just the $n$-simplex ?
