Datatype of Rationals

[Saizan]

I didn't define any operation, but it's a start if someone wants.

[mortberg]

Nice! We could also define this as a set quotient and prove that the two representations are equivalent. I don't have any suggestions for improvements, but let's leave it open for a bit if someone else wants to comments.

@riaqn You might want to look at this.

[Alizter]

The quotient version is defined as Z x N / ~. Where (a, b) ~ (c, d) iff a(d + 1) = c(b + 1).

[Saizan]

@Alizter do you think that would work better? it seems a bit of an artificial representation trick that would need more messing around with the signs of these interegers, though we won't really know until we implement things.

[Alizter]

@Saizan that is the definition of the rationals in the HoTT book, just showing they are equivalent is enough. I like your definition of rationals better however.

[Saizan]

See issue #116