The goal of this talk is to present a formulation and proof of Châtelet’s Theorem over an arbitrary commutative ring in the setting of synthetic algebraic geometry, using the results already proved about projective space, in particular the fact that any automorphism of the projective space is given by a homography. We make essential use of basic results about HoTT and modalities. Indeed, in this context, étale sheafification can be described as a modality. The formulation of Châtelet’s result then becomes that given an inhabited étale sheaf X, the proposition ‘X is a projective space’ is itself an étale sheaf.