Author: P Format: MarkdownItexdisplayed coinductive types in dependent type theory
<a href="https://ncatlab.org/nlab/revision/displayed+coinductive+type/1">v1</a>, <a href="https://ncatlab.org/nlab/show/displayed+coinductive+type">current</a>
displayed coinductive types in dependent type theory