2026-08-14T12:07:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5489 2024-03-06T10:36:12Z ddc:004 open_access

Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory Ahrens, Benedikt Spadotti, Régis relative comonad Martin-Löf type theory coinductive type computer theorem proving 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Ahrens and Régis Spadotti 2015 Is Part Of LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2014.1 urn:nbn:de:0030-drops-54891 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.1 eng https://creativecommons.org/licenses/by/3.0/legalcode