I wish I understand

[thesz]

Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory.

Как же не хватает знаний!