Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and left on me an impression of something like a text by Conan Doyle abruptly interrupted at the most thrilling moment.
Could somebody update me on it? What happened afterwards? Most intriguing question that remains unanswered there is whether one can construct a more or less complete duality between inductive and coinductive types. The phenomenon of limit-colimit coincidence somehow suggests that in at least some circumstances that stem from endofunctors in the category-theoretic semantics, the types that correspond to initial algebras and final coalgebras of these endofunctors should be equivalent in some sense. There is a controversy in that discussion whether to expect that.
As an aside, let me remark that there does not even seem to exist any tags related to coinduction here.
I -> T
, which is the way paths are presented. So similar theories almost automatically make proper coinductive equality proofs just as natural as inductive equality proofs. $\endgroup$