Счетные подмножества в Агде

Question

Мне нужно выразить счетное свойство для определенного подмножества, определенного определенным предикатом P. Моя первая идея состояла в том, чтобы явно заявить, что существует функция f, которая является биективной между моим подмножеством и, скажем, натуральными числами. Есть ли другой более общий способ выразить это свойство в стандартной библиотеке?

заранее спасибо

Answer 1

Если вы используете набор, изоморфный натуральным числам, почему бы вам просто не использовать натуральные числа?

Нет никакого способа различить изоморфные множества, и в HoTT (или кубической агде) изоморфные множества равны. Следовательно, запросить множество, изоморфное Nat, - это то же самое, что запросить число, равное 3.