表示索引容器最大不动点之间的连续函数
Representing Continuous Functions between Greatest Fixed Points of Indexed Containers
AI总结：
本文提出用转换器表示余归纳类型间的可计算函数，推广了Hancock的工作，并在Agda中形式化，无需相等性但需归纳-递归定义。
摘要：
我们描述了一种在类型论中将余归纳类型之间的可计算函数表示为特定转换器的方法。这推广了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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
