Benedikt Ahrens and RΓ©gis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index

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

This table of contents give pointers in the Coq formalisation following the sectioning of the paper

Preliminaries

Codata types in intensional Martin-Löf type theory

Relative Comonads and their morphisms

Comodules over relative comonads

Terminality for streams and infinite triangular matrices

Benedikt Ahrens and RΓ©gis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index