Berthelot's comparison theorem connects the algebraic de Rham cohomology of a $\mathbb{Z}\_p$-scheme and the crystalline cohomology of its special fiber. Is there a statement on the level of homotopy types which implies Berthelot comparison? 


One would have to define crystalline and de Rham homotopy types first, and I am not completely sure how to do that.



Non-abelian Berthelot comparison?
Yes. A Google search will immediately give you lots of articles in varying generality (see e.g. work of Shiho), but one article I'm particularly fond of is Kim and Hain's *"A de Rham-Witt approach to crystalline rational homotopy theory"* in Compositio 2001. See Theorem 2 for the comparison of crystalline and de Rham homotopy types.


