For some categories $C$ and $D$, there's a functor from $C$ to $D$, and we claim (and prove! -- by citing an old paper of Mochizuki) that this functor is fully faithful. Joshi defines a category $C'$ with a non-fully-faithful forgetful functor $C'\to C$ by endowing objects of $C$ with some extra data, and then notes that $C'\to C\to D$ is not fully faithful. Joshi makes the linguistic trick of calling the extra data he puts on objects of $C$ an "arithmetic holomorphic structure", but this is just linguistics...

I'm not sure exactly what you're asking, but for any condensed anima $X$, one can define an $\infty$-topos of relatively discrete condensed anima over $X$ (this is some kind of etale topos of $X$). Then this pro-anima is the shape of this $\infty$-topos. It's also the shape of the slice (condensed anima over $X$).

The word Hecke operator is overloaded: Traditionally, it refers to correspondences coming from bi-$K$-orbits in $G(\mathbb Q_p)$. The name then got used more generally for correspondences coming from bi-$K$-orbits in $G(F)$ for any "local" field $F$, and here we use it for $B_{\mathrm{dR}}^+$. I.e., we really talk about a geometric Hecke operator acting on $\mathrm{Bun}_G$. So this Hecke operator is about modifications of $G$-bundles on the Fargues-Fontaine curve. But the LT space can be written as a space of modifications $\mathcal O^n\to \mathcal O(1/n)$ on the FF curve.

@JamesHanson If you build projective resolutions in condensed abelian groups, this will happen, so it's definitely convenient. Whether the proofs really require you to choose a full projective resolution may be a different matter. And I'm sure much of the theory works in much weaker fragments.

Sure! I claim that if $R$ is a normal integral domain with fraction field $K$, then finite etale $X\times \mathrm{Spec}(R)$-schemes embed fully faithfully into finite etale $X\times \mathrm{Spec}(K)$-schemes. (In particular, connectedness is preserved.) For the claim, you can use h-descent in $X$ to reduce to the case that $X$ is normal and affine, in which case the inverse functor is given by taking the normalization in the finite etale scheme over the generic fibre.

That works. Fun fact that should be more widely known: Instead of asking $\hat{R}$ to be noetherian, it's enough to ask $R/\pi$ to be noetherian (the two are equivalent, see stacks.math.columbia.edu/tag/05GH).