一句话：将余归纳类型间的可计算函数表示为类型论中的特殊 transducer，推广流函数工作并在 Agda 中形式化。
本文研究如何在依赖类型论中表示余归纳类型（最大不动点）之间的可计算/连续函数。作者将这类函数刻画为一种特殊的 transducer，从而把 P. Hancock 关于流之间函数的工作推广到由索引容器生成的更广泛的余归纳类型。该构造无需一般等式概念，但依赖于归纳-递归定义；其大部分性质仅依赖内涵相等这种较弱的等式概念，因而可在 Agda 中形式化。关键结果是给出一般化的表示方法，并说明这些构造与性质可在依赖类型语言中机械化验证。
We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.
@article{paperbot1293,
title = {Representing Continuous Functions between Greatest Fixed Points of Indexed Containers},
author = {Pierre Hyvernat},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:13)2021}
}