agda - Agda 中的可数子集

Question

我需要在某个谓词 P 定义的特定子集上表达可数属性。我的第一个想法是明确声明存在一个函数 f，它在我的子集和自然数之间是双射的。在标准库中是否有另一种更通用的方式来表达该属性？

先感谢您

Answer 1

如果您使用的是与自然数同构的集合，为什么不直接使用自然数呢？

没有办法区分同构集，并且在 HoTT（或立方体 agda）中，同构集是相等的。因此，求一个与 Nat 同构的集合与求一个等于 3 的数是一样的。