The usual notion of trivial covering morphism is in a sense intrinsic to the adjunction $\Pi_0\dashv H$ between connected components and discrete spaces: a continuous map $f$ is a trivial covering morphism if and only if its naturality square is a pullback square. The naturality square being a pullback encodes being an identity on each connected component.
Is there an adjunction that gives an intrinsic notion of formal étaleness? I know that infinitesimal cohesion might have something to do with this, but I find it very hard to fill in the blanks in the ideas sketched by Lawvere. On the nlab there are fascinating entries on differential cohesion which unfortunately I cannot digest. I struggle with the $\infty$-groupoids and the latter.
So, rephrasing, what is the "down to earth" adjunction that yields formally étale morphisms? Is there any place to read about it at the 1 or 2-categorical level? What is this adjunction for commutative ring spectra?