In the theory, the rule looks like this:
A : \Type0 p : isSet A
----------------------------------
F(A,p) : \Set0
and we also add an equivalence between A and F(A,p). In the actual implementation, you can do this using \use \level construction. If you can prove that some \data or \record satisfies isSet (or, more generally, that it is an n-type), then you can put this proof in \use \level function corresponding to this definition and it will be put in the corresponding universe. So, you can define \data F(A,p) with one constructor with one parameter of type A and put it in \Set0.