5 ms·
Don't you need to quotient after you've got Cauchy sequences? For example, (0,0,0,0,....) is a representative of the same real number (as Cauchy sequence) same
by mafribe 11y ago
Don't you need to quotient after you've got Cauchy sequences? For example, (0,0,0,0,....) is a representative of the same real number (as Cauchy sequence) same as (1,0,0,0,0,0,....), but both are different as streams.
- tel 11y agoYeah, depends on how you're encoding it. Quotient types are to my knowledge still tricky to implement, but you can try to make a setoid and structure this type with some kind of equality. Of course, now we run directly into totality and semi-decidability.