Kerodon

I can confused with the proof of proposition 3.4.1.9. By proposition 3.4.1.2, this should be obvious. Am I missing something?

Yep, that's simpler. Thanks!

In Proposition 3.4.1.14, it should say $X_{01}$ instead of $Y$ in the line before the second diagram.

Yep. Thanks!

Is it ok if you could elaborate on Example 3.4.1.14? Why $\mathrm{ev}_{0}$ is a Kan fibration? Why $P$ is contractible? And I cannot see clearly why the second square is a homotopy pullback if $\Omega X$ is contractible. I can understand that by Example 3.4.1.3 it is homotopy pullback if-f $\Omega X$ is weakly homotopy equivalent to the pullback of the square. This pullback is exactly the same of the first square before writing $\iota$ as $\iota'$, so I am confused a little bit.

I would like to ask about the general philosophy behind your definition of homotopy pullback. In the pdf note of W. G. Dwyer and J. Spalinski, we define a homotopy pullback in any model category $C$. If $X_{0}\to X ← X_{1}$ is a diagram, then the homotopy pullback of it is the pullback of a fibrant replacement of this diagram. It coincides with the pullback of this diagram if $X$ is fibrant and the two maps are fibrations. So, in the Kan-Quillen model structure of simplicial sets, the pullback is already a homotopy pullback if $X$ is a Kan complex and the two maps are Kan fibrations (if we assume now that X_{0},X,X_{1}) are simplicial sets. If we have only one of the maps to be a Kan fibration, then the pullback is already a homotopy pullback if all simplicial sets are Kan complexes, see Cisinksi's book proposition 2.3.27. But your definition is only for one of the maps to be a Kan fibration without having Kan complexes. If we have only $X$ Kan complex then it is also the homotopy fiber product.

Could you explain your approach and how it is related to the standard approach of model categories?

The standard model structure on simplicial sets is right proper. This gives extra flexibility for computing homotopy pullbacks.