Terminal semantics for codata types in intensional Martin-L\"of type theory
Logic in Computer Science
2014-04-23 v2 Category Theory
Abstract
In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type families of streams and of infinite triangular matrices, respectively, in intensional Martin-L\"of type theory. Our results are mechanized in the proof assistant Coq.
Keywords
Cite
@article{arxiv.1401.1053,
title = {Terminal semantics for codata types in intensional Martin-L\"of type theory},
author = {Benedikt Ahrens and Régis Spadotti},
journal= {arXiv preprint arXiv:1401.1053},
year = {2014}
}
Comments
14 pages, ancillary files contain formalized proof in the proof assistant Coq; v2: 20 pages, title and abstract changed, give a terminal semantics for streams as well as for matrices, Coq proof files updated accordingly