Correspondence of left and right homotopies produces a homotopy of maps $A\times I \to X^I$ (Hovey, Lemma 6.1.5) My question pertains to a specific piece of the proof of Lemma 6.1.5 in Hovey's Model Categories
(page 160 in pdf, 150 by numbering).
I'll briefly recall the definitions and set up my question first, so that it's somewhat self contained.
Model Category: Let $\newcommand\C{\mathcal{C}}\C$ be a model category (in particular, the factorizations are functorial for Hovey).
Index notation: Upper indices indicate cosimplicial stuff, lower indices indicate simplicial stuff.
Framings:
Then $\C^\Delta$ and $\newcommand\op{{\mathrm{op}}}\C^{\Delta^\op}$ have Reedy model structures. If $A\in \C$ is an object, then we can define two cosimplicial objects,
$\ell^n A = [n]\otimes A=\coprod_{i=0}^n A$ (where the tensoring comes from $\Delta\newcommand\into\hookrightarrow \into \newcommand\Set{\mathbf{Set}}\Set$) and $r^nA = A$, the constant cosimplicial object at $A$. Moreover, the fold map gives a map $\ell^\bullet A\to r^\bullet A$. We can construct a functorial (in $A$) factorization of the fold map
$\ell^\bullet A \to A^\circ \to r^\bullet A$ such that the first map is a Reedy cofibration, the second map is a trivial Reedy fibration (in particular, a degreewise weak equivalence), and the factorization is $A\xrightarrow{1_A}A\xrightarrow{1_A}A$ in degree 0. Essentially $A^\circ$ is a cosimplicial resolution of $A$.
Dually, we can construct a simplicial resolution $X_\circ$ for any object $X$ as well. (Such factorizations are called framings, though I'll only be talking about these two.)
Background facts:
We can use the framings to define simplicial sets $\newcommand\Map{\operatorname{Map}}\Map_{\ell}(A,X)$ and $\Map_r(A,X)$ by $\Map_\ell(A,X)[n] = \C(A^\circ[n],X)$ and $\Map_r(A,X)[n]=\C(A,X_\circ[n])$.
The mapping simplicial sets are fibrant when $A$ is cofibrant and $X$ is fibrant, and
moreover, there are weak equivalences of simplicial sets
$$\Map_\ell(A,X) \xrightarrow{\sim} \newcommand\diag{\operatorname{diag}}\diag \C(A^\circ,X_\circ)\xleftarrow{\sim} \Map_r(A,X)
$$
induced by the degeneracy maps from/to degree 0 respectively. (Here $\diag$ is the diagonal of a bisimplicial set.)
These simplicial sets are pointed (by $0$) if $\C$ is.
The statement I want to prove:
Let $\C$ be a pointed model category, $A$ cofibrant, $X$ fibrant,
$h:A^\circ[1]\to X$, $k:A\to X_\circ[1]$ left and right homotopies respectively, such that $$hd^0=hd^1=d_0k=d_1k=0 : A\to X.$$
Suppose moreover, that we have $H:A^\circ[1]\to X_\circ[1]$ such that
$d_1H=h$, $d_0H=0$, $Hd^1=k$, $Hd^0=0$. (These might be backwards, I'm not sure whether the indices in Hovey correspond with the face maps or with vertex inclusions. For now I'll assume that they're the vertex inclusions, but we'll see that it won't matter in the end.)

We want to show that these data can be used to construct a simplicial homotopy (stationary on the boundary) from $s_0h$ to $ks^0$ (regarded as 1-simplices in $\diag\C(A^\circ,X_\circ)$).

Geometry:
We are given a 1-simplex in $\Map_\ell(A,X)$, $h:0\to 0$, a 1-simplex in $\Map_r(A,X)$, $k:0\to 0$, and a
correspondence, $H$, realized as a (1,1)-bisimplex in $\C(A^\circ,X_\circ)$ which looks like this:
$$
\require{AMScd}
\begin{CD}
0 @>0>> 0
\\
@AkAA @AA0A
\\
0 @>h>> 0
\end{CD}
$$
We want to produce a $\Delta^1\times \Delta^1$ in $\diag \C(A^\circ,X_\circ)$ that has boundary the following:
$$
\begin{CD}
0 @>ks^0>> 0
\\
@A0AA @AA0A
\\
0 @>>hs_0> 0
\end{CD}
$$
Hovey's argument, and where I think it breaks down
A simplicial homotopy from $s_0h$ to $ks^0$ (viewed as maps $\Delta^1\to \diag \C(A^\circ,X_\circ)$)
is a $\Delta^1\times \Delta^1$ in $\diag \C(A^\circ, X_\circ)$ with boundary
$$
\begin{CD}
0 @>ks^0>> 0
\\
@A0AA @AA0A
\\
0 @>>s_0h> 0,
\end{CD}
$$
where the first factor is on the horizontal axis.
Such a $\Delta^1\times \Delta^1$ is equivalent to the data of two diagonal $2$-simplices $H_0, H_1 : A^\circ[2]\to X_\circ[2]$ such that
$$d_0^{\mathrm{diag}}H_0 = ks^0, \quad d_2^{\mathrm{diag}}H_0 = 0,$$ $$d_1^{\mathrm{diag}}H_0=d_1^{\mathrm{diag}}H_1,$$
$$d_0^{\mathrm{diag}}H_1=0\text{, and }d_2^{\mathrm{diag}}H_1=s_0h.$$
Hovey suggests we define $H_0=s_1Hs^0$, $H_1=s_0Hs^1$, and then verify that the required identities hold using the simplicial identities.
He does not, however, include the verification, so we're left to check this ourselves, where we get the following:
$$\newcommand\ddiag{d^{\mathrm{diag}}}\ddiag_0H_0 = d_0s_1Hs^0d^0= s_0d_0H=0$$
$$\ddiag_1H_0 = d_1s_1Hs^0d^1 = H$$
$$\ddiag_2H_0 = d_2s_1Hs^0d^2 = Hd^1s^0 = ks^0$$
$$\ddiag_0H_1 = d_0s_0Hs^1d^0 = Hd^0s^0 = 0$$
$$\ddiag_1H_1 = d_1s_0Hs^1d^1 = H$$
$$\ddiag_2H_1 = d_2s_0Hs^1d^2 = s_0d_1H = s_0h.$$
In other words, we sort of recover $H$ in a sense, because the boundary of the square is
$$
\begin{CD}
0 @>0>> 0
\\
@Aks^0AA @AA0A
\\
0 @>>s_0h> 0,
\end{CD}
$$
and the diagonal 1-simplex in the square is $H$ itself.
However, this is not the homotopy we want. Also, it's clear that it doesn't matter what indexing convention Hovey was using, since we would again just get some version of $H$.
These seem to be the only reasonable 2-simplices that we can cook up out of $H$ just applying the degeneracies, since the other two possibilities would be degenerate in the diagonal simplicial set, and will have faces $H$, $H$, $0$ in the appropriate orders.
Summary of Questions

*

*Have I made a mistake in my interpretation or calculation somewhere?

2a) Is the claim even true? If yes, does some variation of this argument work?
2b) If the claim is not true, for the purposes of Lemma 6.1.5, it would suffice to prove the weaker claim that $s_0h$ and $ks^0$ represent the same morphism $\Delta^1\to \diag\C(A^\circ,X_\circ)$ in the homotopy category (which is not the same as being homotopic, since $\diag\C(A^\circ,X_\circ)$ is not necessarily fibrant). Is this true/can the argument be made to prove this?


*If neither claim in 2a or 2b holds, it should still be true that Lemma 6.1.5 is true. It seems that Hovey's goal is to reprove Quillen's results on the representability of elements of $[\Sigma A, X]$ in terms of homotopy classes of left/right homotopies in the language of framings. Is there another source that uses framings to prove these results? Hovey only cites Quillen for this chapter.

 A: As noted in question 2b, it would suffice for the purposes of Lemma 6.1.5 to prove that if we have a correspondence $H:A^\circ[1]\to X_\circ[1]$ between $h:A^\circ[1]\to X$ and $k:A\to X^\circ[1]$, then $s_0h$ and $ks^0$ represent the same homotopy class of maps
in $$[\Delta^1,\newcommand\diag{\operatorname{diag}}\diag\newcommand\C{\mathcal{C}}\C(A^\circ,X_\circ)].$$
I think we can adapt Hovey's proof to at least prove this.
We can produce simplicial homotopies $s_0h$ to $H$ and $ks^0$ to $H$ using the simplices $H_0$, and $H_1$ from the question, as well as $\newcommand\ddiag{d^{\mathrm{diag}}}\newcommand\sdiag{s^{\mathrm{diag}}}\sdiag_1H$.
This is because $\ddiag_1\sdiag_1H=\ddiag_2\sdiag_1H=H$, and $\ddiag_0\sdiag_1H=\sdiag_0\ddiag_0H=0$.
Thus $H_1$ and $\sdiag_1H$ fit together to give a $\Delta^1\times \Delta^1$ with boundary
$$
\require{AMScd}
\begin{CD}
0 @>H>> 0 \\
@A0 AA @AA0A \\
0 @>>s_0h> 0,
\end{CD}
$$
and diagonal $H$, with $H_1$ in the lower right half of the square and $\sdiag_1H$ in the upper left half.
Doing the same thing with $H_0$ gives a simplicial homotopy from $ks^0$ to $H$.
Finally, simplicial homotopies are left homotopies, so $s_0h$ and $ks^0$ represent the same homotopy class of maps.
(Actually, this should all be in pointed simplicial sets, since we're really trying to prove facts about $\pi_1\newcommand\Map{\operatorname{Map}}\Map_\ell(A,X)$ and its isomorphism to $\pi_1\Map_r(A,X)$, however, this should all descend to pointed maps properly, because we've guaranteed that the homotopies are $0$ on the boundary of the interval, so these actually give pointed homotopies $S^1\wedge \Delta^1_+\to \diag\C(A^\circ,X_\circ)$ which are again left homotopies.)
