So here is the proof of the 5.2.3.1:
I have two question about this proof.
A.in the last paragraph it says:
It suffices to prove that there exists an extension of $\bar{k_0}$ to a map $\bar{k}:X\rightarrow M$
But $X=(K\times \Delta^1)\coprod_{K\times \Delta^1\times B\times \{0\}}(K\times \Delta^1\times B\times \Delta^1)$ is different from $(K\times \Delta^1)\diamond B=(K\times \Delta^1)\coprod_{K\times \Delta^1\times B\times \{0\}}(K\times \Delta^1\times B\times \Delta^1)\coprod_{K\times \Delta^1\times B\times \{1\}}B$:
A morphism from $X$ can be represented by a morphism from $K\times \Delta^1\times B\times \Delta^1$ whose restriction to $K\times \Delta^1\times B\times \{0\}$ is induced by some morphism from $K\times \Delta^1$ via the projection $K\times \Delta^1\times B\times \{0\}\rightarrow K\times \Delta^1$.
A similar statement holds for $(K\times \Delta^1)\diamond B$, and I see nothing ensures that a morphism from $X$, represented by $f:K\times \Delta^1\times B\times \Delta^1\rightarrow ?$, when restricted to $K\times \Delta^1\times B\times \{1\}$, is induced by some morphism from $B$ via the projection $K\times \Delta^1\times B\times \{1\}\rightarrow B$.
So my first question is, why this proof is correct...?
B. The second question arises when I try to figure out another way to prove this lemma. A general idea to solve lifting problem like this is to use lemma like 2.1.2.3, 2.1.2.4:
So I have been wondering is there any similar mechanism for marked anodyne morphisms?
Specifically, in the morphism $H:((K\times \Delta^1)\ast A)\coprod_{(K\times\{0\})\ast A} ((K\times \{0\})\ast B)\rightarrow ((K\times \Delta^1)\ast B)$, we can mark the edges $\{k\}\times \Delta^1$ in the $(K\times \Delta^1)$, precisely those who are sent to $q$-coCartesian edges. And by fibrant replacement, without loss of generality we can suppose that $M\rightarrow \Delta^1$ is a coCartesian fibration. Now the morphism $H$ is the push-out join of the marked anodyne $K\times \{0\}\rightarrow K\times \Delta^1$ and the cofibration $A\subseteq B$.
Here comes my second question:
B1. Is there a way to suitably define the marked edges of the join(or alternate join whatever) of two simplicial sets?
B2. If the answer of B1 is yes, Is the push-out join(or alternate join whatever) of a marked anodyne morphism and a cofibration still a marked anodyne morphism?
Meanwhile I think the following proposition might be a hint of the availability of those claims:
