# What is the name of a coinductive type defined with a total order relation?

In type theory, is there a name for a coinductive type simply defined with a successor operator and an equivalence relation?

And what would be the name of such a type if it were defined with a total order relation as well?

Also, as far as the successor operator is concerned, is there a recommend single-symbol notation for it that would provide a more concise alternative to the usual $$succ(\alpha)$$? For example, something like $$\alpha^\triangleright$$.