How to define recursive types in rocq?

Just use the Inductive type definition. For example:

Inductive nat : Type :=
	| O
	| S (n : nat).