## Stream: general

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

#### 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

#### Kenny Lau (Nov 23 2018 at 02:47):

well this surely implies decidable_eq to start with

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

#### Kenny Lau (Nov 23 2018 at 02:53):

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

#### Kenny Lau (Nov 23 2018 at 02:54):

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

#### Mario Carneiro (Nov 23 2018 at 04:46):

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

#### 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