Terminal semantics for codata types in intensional Martin-Löf type theory

View the Project on GitHub benediktahrens/coinductives

Terminal semantics for codata types in intensional Martin-Löf type theory

Benedikt Ahrens and Régis Spadotti

Download the article here:

Download the Coq source from here:

View the online documentation generated by coqdoc here:

Abstract: We study the notions of relative comonad and comodule over a relative comonad. We use these notions to give categorical semantics for the coinductive type families of streams and of infinite triangular matrices and their respective cosubstitution operations in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.