Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory
Benedikt Ahrens, Régis Spadotti · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015
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.