I'm new to type theory, and recently read introductory materials where dependent type are discussed. One of my friend asked me, "Those dependent types are having recursors & 'inductors'(dependent eliminators), but how about those types that is co-inductive/co-recursive?"

Some related example is much appreciated.