powering in nLab
H((−),Maps(X,A))≃H((−)×X,A)→H((−)×f,A)H((−)×Y,A)≃H((−),Maps(X,A)). \mathbf{H} \big( (-) ,\, Maps(X,A) \big) \;\simeq\; \mathbf{H} \big( (-) \times X ,\, A \big) \xrightarrow{ \mathbf{H} \big( (-) \times f ,\, A \big) } \mathbf{H} \big( (-) \times Y ,\, A \big) \;\simeq\; \mathbf{H} \big( (-) ,\, Maps(X,A) \big) \,.
By definition, for any S∈Grpd ∞S \in Grpd_\infty and X∈HX \in \mathbf{H} the powering] is the (∞,1)-limit over the diagram constant on XX
K⋅X=lim → KX. K \cdot X \,=\, {\lim_{\to}}_K X \,.
Proof
For the first statement to be proven, consider the following sequence of natural equivalences:
H(X,Maps(LConst(S),A)) ≃H(X×LConst(S),A) (2) ≃H(LConst(S),Maps(X,A)) (2) ≃Grpd ∞(S,ΓMaps(X,A)) (1) ≃Grpd ∞(S,H(* H,Maps(X,A))) bythis Prop. ≃Grpd ∞(S,H(* H×X,A)) (2) ≃Grpd ∞(S,H(X,A)) \begin{array}{lll} \mathbf{H} \Big( X ,\, Maps \big( LConst(S) ,\, A \big) \Big) & \;\simeq\; \mathbf{H} \big( X \times LConst(S) ,\, A \big) & \text{(2)} \\ & \;\simeq\; \mathbf{H} \Big( LConst(S) ,\, Maps \big( X ,\, A \big) \Big) & \text{(2)} \\ & \;\simeq\; Grpd_\infty \Big( S ,\, \Gamma \, Maps \big( X ,\, A \big) \Big) & \text{ (1) } \\ & \;\simeq\; Grpd_\infty \bigg( S ,\, \mathbf{H} \Big( \ast_{\mathbf{H}} ,\, Maps \big( X ,\, A \big) \Big) \bigg) & \text{by}\;\text{<a href="https://ncatlab.org/nlab/show/terminal+geometric+morphism#DirectImageOfTerminalGeometricMoprhismIsHomOutOfTerminalObject">this Prop.</a>} \\ & \;\simeq\; Grpd_\infty \Big( S ,\, \mathbf{H} \big( \ast_{\mathbf{H}} \times X ,\, A \big) \Big) & \text{(2)} \\ & \;\simeq\; Grpd_\infty \Big( S ,\, \mathbf{H} \big( X ,\, A \big) \Big) \end{array}
For the second statement, recall that hom-functors preserve limits in that there are natural equivalences of the form
(5)H(lim⟶i,X i,lim⟵j,A j)≃lim⟵ilim⟵jH(X i,A j), \mathbf{H} \Big( \underset{\underset{i}{\longrightarrow}}{\lim} \,, X_i ,\, \underset{\underset{j}{\longleftarrow}}{\lim} \,, A_j \Big) \;\; \simeq \;\; \underset{\underset{i}{\longleftarrow}}{\lim} \, \underset{\underset{j}{\longleftarrow}}{\lim} \, \mathbf{H} \Big( X_i ,\, A_j \Big) \,,
and that ∞\infty-toposes have universal colimits, in particular that the product operation is a left adjoint (2) and hence preserves colimits:
(6)(−)×lim⟶S •≃lim⟶((−)×S •). (-) \,\times\, \underset{{\longrightarrow}}{\lim} \, S_\bullet \;\; \simeq \;\; \underset{{\longrightarrow}}{\lim} \, \big( (-) \,\times\, S_\bullet \big) \,.
With this, we get the following sequences of natural equivalences:
H((−),Maps(lim⟶LConst(S •),X)) ≃H((−)×lim⟶LConst(S •),X) (2) ≃H(lim⟶((−)×LConst(S •)),X) (6) ≃lim⟵H((−)×LConst(S •),X) (5) ≃lim⟵H((−),Maps(LConst(S •),X)) (2) ≃H((−),lim⟵Maps(LConst(S •),X)) (5) . \begin{array}{lll} & \mathbf{H} \bigg( (-) ,\, Maps \Big( \underset{\longrightarrow}{\lim} \, LConst(S_\bullet) ,\, X \Big) \bigg) \\ & \;\simeq\; \mathbf{H} \Big( (-) \times \underset{\longrightarrow}{\lim} \, LConst(S_\bullet) ,\, X \Big) & \text{ (2) } \\ & \;\simeq\; \mathbf{H} \Big( \underset{\longrightarrow}{\lim} \big( (-) \times LConst(S_\bullet) \big) ,\, X \Big) & \text{ (6) } \\ & \;\simeq\; \underset{\longleftarrow}{\lim} \, \mathbf{H} \big( (-) \times LConst(S_\bullet) ,\, X \big) & \text{ (5) } \\ & \;\simeq\; \underset{\longleftarrow}{\lim} \, \mathbf{H} \Big( (-) ,\, Maps \big( LConst(S_\bullet) ,\, X \big) \Big) & \text{ (2) } \\ & \;\simeq\; \mathbf{H} \Big( (-) ,\, \underset{\longleftarrow}{\lim} \, Maps \big( LConst(S_\bullet) ,\, X \big) \Big) & \text{ (5) } \,. \end{array}
This implies (4) by the ∞ \infty -Yoneda lemma over H\mathbf{H} (which is large but locally small, so that the lemma does apply).
Finally (3) is immediate from the fact that LConstLConst preserves the terminal object, by definition:
Maps(LConst(*),X)≃Maps(* H,X)≃X. Maps \big( LConst(\ast) ,\, X \big) \;\simeq\; Maps \big( \ast_{\mathbf{H}} ,\, X \big) \;\simeq\; X \,.