has_zero (fin n)

Stream: new members

[Yakov Pechersky]

Why do we only allow 0 for fin (n + 1)? I understand that 0 = 1 at fin (n + 1), but it seems a lot of things about fin _ would be more simply stated (for what I'm working on) if has_zero (fin 0) was an instance.

[Yakov Pechersky]

In general, is there no has_zero (subsingleton a)?

[Adam Topaz]

fin 0 is empty

[Mario Carneiro]

and subsingleton a, while not really an algebraic type in the first place, is also possibly empty

[Yakov Pechersky]

So we always identify 0 (or 1) with an actual value, not just a stand-in, then?

[Mario Carneiro]

has_zero A implies that the designated element 0 : A has type A, therefore A is not empty

[Yury G. Kudryashov]

has_zero A is defined here: src#has_zero

[Yury G. Kudryashov]

As you can see, the constructor takes zero : α.