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$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.