There are also some facts about $\Delta$-generated spaces not in your references in Section 2 of my paper Homotopical interpretation of globular complex by multipointed d-space.

@FranzLemmermeyer Use a VPN.

One suggestion : the proof assistant Mizar works in a variant of ZFC. And its library of certified proofs is already very huge. You could investigate in this direction. Unlike many people, I don't think that coq is appropriate for formalizing math: because the axiom of choice and the law of excluded middle cannot live together in coq. The situation seems to be different with HoTT, as far as I understand the theory.

I don't understand the last part of your question. What is the translation of your question for the more general setting of a simplicial proper model category ?

@TomLeinster I understand now: with the hipster terminology, a presentable category is not necessarily presentable.

@DylanWilson Me too, I would like to know what could be a globally presentable category.

And also a right adjoint between locally presentable categories is always accessible.

What is a presentable category ? And what is a cocontinuous functor ? I don't understand (i). If you mean a colimit-preserving functor between locally presentable categories, indeed it has a right adjoint by the dual of the Special Adjoint Functor theorem (take the opposite categories and apply SAFT). And an accessible limit-preserving functor between locally presentable categories is always a right adjoint indeed. This is explained in the book you mention.

About Computer science: "It is known that quantum computers can solve NP complete problems in polynomial time." A wrong believe is rather that quantum computers can calculate more things than classic computers; which is false. quantum calculability is equivalent to classic calculability.

@ZhenLin The meaning of homotopy limit was a part of the question.

I did not use commas and periods in my display-mode formulae until an editor one day added periods and commas almost everywhere before publishing the paper. Now I use them... most of the time. :-).

@PeterLeFanuLumsdaine yes indeed.

Simpler: $\Delta[n]\subset \Delta[n+1]$ and then consider the colimit of the tower.