Design and implement a form of co-inductive types

[Russoul]

Varients:

• Base co-inductive type that's enough to assemble others from (like Nat for inductive types)
• M-type
• Co-inductive data-type schema

Later generalise to quotient-indexed-co-inductive data-types