The Funtion Complex - Product Adjunction of simplicial sets and diagram chasing I run into the following claim in the book Simplicial Homotopy Theory (in the proof of Proposition 5.2.). Given $i:K \rightarrow L$ inclusion of simplicial sets and $p:X\rightarrow Y$ fibration.

Someone explained to me that I can use the exponential law to get the identification, but I don't get his idea, for it involves careful interchanging lim/colim etc. Is there any written down proof for this fact? Moreover, I wish to know that if there is general way to understand the interplay between adjunction and commutative diagram so that I might guess from the first diagram what kind of equivalent diagram should I look for.
 A: Yes, there is a written proof of this very long and boring exercise: https://arxiv.org/abs/1902.06074
The general statement is dubbed "Theorem 2.6", and although the obvious application is to model structures, it has absolutely nothing to do with algebraic topology, just old plain category theory.
A: I'm just going to write down a proof here, since there seem to be very few written proofs of this, since most sources seem to leave it as an exercise. Fosco of course has linked a paper on the arXiv with a proof, but I think it's best that we have an answer on MSE as well.
Let $\newcommand\calC{\mathcal{C}}\calC$ be a category, let's suppose we have a closed symmetric monoidal structure on $\calC$, with $\otimes$ the tensor, and the internal hom denoted by $[-,-]$.
Now we make an observation. In any category, commuting squares between morphisms $f:A\to B$ and $g:C\to D$ are given by the following pullback:
$$
\require{AMScd}
\begin{CD}
\calC(A,C)\underset{\calC(A,D)}{\times} \calC(B,D) @>>>\calC(B,D) 
\\
@VVV @VVf^*V
\\
\calC(A,C) @>g_*>> \calC(A,D).
\end{CD}
$$
It's worth carefully thinking about what this is saying first, it's saying that a commuting square is a morphism $a:A\to C$ and a morphism $b:B\to D$ such that $bf = ga$.
Now we can apply the same idea to your situation. We have three maps, $i:A\to B$, $j:K\to L$, and $p:X\to Y$ ($i:A\to B$ here is taking the place of your horn inclusion, and I've renamed your $i$ to $j$).
I claim both sets of squares in your question can be identified with the set of triples of maps
$$
\begin{align*}
\{
(a,k,y) \in \calC(A\otimes L, X)\times &\calC(B\otimes K, X) \times \calC(B\otimes L, Y) \\
:\quad 
& pa = y(i\otimes 1_K), \\
& a(1_A\otimes j) = k(i\otimes 1_K),\\
& pk = y(1_A\otimes j)
\}.
\end{align*}
$$
Note that we can equivalently take the maps to be $a':A\to [L,X]$, $k':B\to [K,X]$, and $y':B\to [L,Y]$ by the adjunction isomorphisms, and the equalities become
$[1_L,p]a' = y'i$, $[j,1_X]a' = k'i$, and $[1_K,p]k' = [j,1_Y]y'$.
To see that both sets of squares are of this form, we could expand out the data of a square like the first one you have:
$$
\begin{CD}
A @>>> [L,X]
\\
@ViVV @VV\widehat{[j,p]}V
\\
B @>>> [K,X]\underset{[K,Y]}{\times}[L,Y].
\end{CD}
$$
The bottom map is a pair of maps $(k' : B\to [K,X],y':B\to [L,Y])$ such that
$[1_K,p]k'=[j,1_Y]y'$. The top map is of course $a' : A\to [L,X]$, and the requirement that the square commute gives the equalities
$[j,1_X]a' = k'i$ and $[1_L,p]a'=y'i$.
Conversely, triples of maps satisfying the equalities give such a square.
We can do exactly the same thing for the bottom square.
Notes
This generalizes to two variable adjunctions more generally.
Moreover it's worth noting that the collection of such squares in both cases is actually given by the cubical analogue of a pullback, the limit over $(0\to 1)^3$ minus its initial vertex (I'll call diagrams of this shape punctured cubes.).  Then the adjunction isomorphisms give isomorphisms between the punctured cubes, which induces isomorphisms on the limits, which are the sets of commuting squares. Finally, a morphism in the arrow category say $i'\to i$, $j'\to j$, or $p\to p'$ induces translations of the punctured cubes which make the commuting diagrams contravariantly functorial in $i$ and $j$ and covariantly functorial in $p$.
Moreover, since the adjunction isomorphisms are natural, this means that we'll end up with a 2-variable adjunction on the arrow category.
