Zulip Chat Archive

Stream: new members

Topic: has_zero (fin n)


Yakov Pechersky (Aug 11 2020 at 20:50):

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 (Aug 11 2020 at 20:50):

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

Adam Topaz (Aug 11 2020 at 20:52):

fin 0 is empty

Mario Carneiro (Aug 11 2020 at 20:53):

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

Yakov Pechersky (Aug 11 2020 at 20:54):

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

Mario Carneiro (Aug 11 2020 at 20:55):

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

Yury G. Kudryashov (Aug 12 2020 at 07:21):

has_zero A is defined here: src#has_zero

Yury G. Kudryashov (Aug 12 2020 at 07:21):

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


Last updated: Dec 20 2023 at 11:08 UTC