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

Stream: general

[Kenny Lau]

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

[Kenny Lau]

well this surely implies decidable_eq to start with

[Kenny Lau]

(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?)

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

in particular is_well_order.min is not constructive