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.
Yes there is a trick: for every universe $\mathcal{U}$, postulate the existence of a successor universe $\mathcal{U}^+$ : this is used for example in "Homotopy Limit Functors on Model Categories and Homotopical Categories" by Dwyer, Hirschhorn, Kan, Smith.
This is an additional comment to my post. What is remarkable is not that there is a homotopy theory of types: after all, there are a lot of homotopy theories of many kinds of objects. What is remarkable is that the homotopy theory of logical types behaves exactly like "standard" homotopy types. And also, there are other coincidences in mathematics which are indeed not very fortunate. Some adjectives like "regular" or "normal" are semantically overloaded.
Yes of course ; Should I post here or open a new thread ? I will give the definitions, and my attempts to find zig-zag of adjunctions, and why that does not work (so far).
I believed that "On combinatorial model categories" by J. Rosicky was the answer (math.muni.cz/~rosicky/papers/comb2.pdf), and page 8 (top of the page), one can read that $cof(S)$ is not always accessible, $S$ being a set ! On the contrary, $inj(S)$ is always accessible (Proposition 3.3 of the same paper) as a small injectivity class...
I cannot edit my comment so I rephrase my question. Take a "very good" cofibrant replacement $f.g$ of $X$ ($f$ cofibration and $g$ trivial fibration). Why does it come from a factorization by a functor $T$ constructed using the small object argument ?
