2

I need to express the countable property over a specific subset defined by a certain predicate P. My first idea was to explicitly state that there exists a function f which is bijective between my subset and, let's say, the natural numbers. Is there another more general way to express that property in the standard library ?

Thank you in advance

MrO
  • 1,291
  • 7
  • 14
  • An injective function from your subset to the natural numbers is enough, isn't it? – gallais Nov 22 '17 at 12:15
  • I also want to ensure that my subset is infinite, which is why I wanted the function to be bijective. I should have mentioned that, even though this does not change the question much. – MrO Nov 22 '17 at 15:18
  • What would an uncountable set look like in Agda? – Cactus Nov 23 '17 at 08:13
  • I don't see why Sets should necessarily be countable. Reals defined as Cuts in rational are not countable for instance. Although I don't know if that's been implemented in Agda. – MrO Dec 01 '17 at 15:48

1 Answers1

1

If you are using a set that is isomorphic to the natural numbers why don't you just use the natural numbers?

There is no way to distinguish isomorphic sets and in HoTT (or cubical agda) isomorphic sets are equal. Hence asking for a set that is isomorphic to Nat is the same as asking for a number that is equal to 3.

Thorsten Altenkirch
  • 519
  • 2
  • 3
  • What if your functions are very cumbersome to express over Nat? – Cactus Nov 27 '17 at 03:06
  • I don't use the natural numbers because I use differents subsets of a generic set which are supposed to be countable. Also, I don't see why two isomorphic sets should be equal. It depends on the equality one use, they never will be regarding the propositional equality, but the bijection is indeed supposed to reveal an underlying link which allows to use one instead of the other when required. – MrO Dec 01 '17 at 15:49
  • They are propositionally equal in Homotopy Type Theory, e.g. in cubical or cubical agda. – Thorsten Altenkirch Dec 06 '17 at 09:59
  • Could you please elaborate ? To my knowledge, propositionnal equality is generated by reflexivity and provides no way to prove such a thing. – MrO Jan 12 '18 at 16:56
  • In HoTT propositional (or typal) equality is extensional and in particular it identifies isomorphic types. If you generate equality by reflexivity you just reflect definitional equality for closed terms which is not usually what you want. – Thorsten Altenkirch Jan 13 '18 at 21:30