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

Benedikt Ahrens and Régis Spadotti

Download the article here:

• most recent version (pdf)
• paper on the arXiv (updated less frequently than above version)

Download the Coq source from here:

• Coq source code (zip)

View the online documentation generated by coqdoc here:

• Table of contents
• Index

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.