[TYPES] Reg Axioms of pure type systems

[Param Jyothi Reddy]

Hi all,
I have a doubt regarding the pure type systems.  Let it be (S, A, R) 

In A we have sorting relation on the sorts (s_1:s_2 kind of data). Are
there any conditions on these? (Not like functional or injective but
more inherent for arbitrary PTS).

Like for example is circularity allowed (s_1:s_2 and s_2:s_1)?

Regards,
Param