Coinitial semantics for redecoration of triangular matrices
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Coinitial semantics for redecoration of triangular matrices.
Sus autores son Benedikt Ahrens y Régis Spadotti (del IRIT, Université Paul Sabatier).
Su resumen es
Infinite triangular matrices and, in particular, the redecoration operation on them, were studied by Matthes and Picard. In their work, redecoration is characterized as the cobind operation of what the authors call a “weak constructive comonad”.
In this work, we identify weak constructive comonads as an instance of the more general notion of relative comonad. Afterwards, building upon the work by Matthes and Picard, we give a category-theoretic characterisation of infinite triangular matrices—equiped with the canonical bisimulation relation and a compatible comonadic cobind operation—as the terminal object in some category.
El código de las correspondientes teorías en Coq se encuentra aquí.