Zulip Chat Archive

Stream: general

Topic: constructivising using `trunc (subtype (is_well_order _))`


view this post on Zulip Kenny Lau (Nov 23 2018 at 02:46):

How many things can we constructivise with a trunc (subtype (is_well_order _)) hypothesis? I'm sure we can make a truncated basis this way... Maybe if it can constructivise a lot of stuff, I would imagine making it as wide-used as decidable_eq

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:47):

well this surely implies decidable_eq to start with

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:48):

(on second thought maybe we need a decidable prop to do so, but we can fix this by requiring our function to have codomain bool instead?)

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:53):

and how about making trunc (equiv _ _) an instance

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:54):

congratulations then, you got yourself into an instance loop with a fintype having decidable equality

view this post on Zulip Mario Carneiro (Nov 23 2018 at 04:46):

I think is_well_order is not as useful constructively as it is in classical maths

view this post on Zulip Mario Carneiro (Nov 23 2018 at 04:46):

in particular is_well_order.min is not constructive


Last updated: May 11 2021 at 13:22 UTC