表示索引容器最大固定点之间的连续函数
摘要：一种在类型理论中将可计算函数表示为特定转导器的方法。这将P. Hancock关于流之间函数的早期工作推广到了更丰富的类别的共归类型。这些转导器可以在依赖类型理论中定义，而无需任何等式的概念，但需要归纳递归的定义。这些构造的大部分属性只依赖于轻微的等式概念（内禀等式），因此可以在依赖类型的语言Agda中形式化。
作者：Pierre Hyvernat
论文ID：1902.10971
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22