## Stream: General

### Topic: Generalising to subset

#### Lukas Stevens (Aug 13 2020 at 08:33):

Consider the locale `comp_fun_commute`: it fixes `f` and assumes `f x o f y = f y o f x`.What I want to have is `comp_fun_commute_on` that fixes `f` and `A` and assumes `x ∈ A ⟹ y ∈ A ⟹ f y ∘ f x = f x ∘ f y`. Is there a trick to generalise the first locale to the second one, without changing all the theorems and proofs?

#### Manuel Eberl (Aug 13 2020 at 09:04):

Yeah that's what types-to-sets does

#### Manuel Eberl (Aug 13 2020 at 09:04):

probably not worth it in this case though

#### Manuel Eberl (Aug 13 2020 at 09:05):

you might be able to do some trickery like artificially defining a new f relativised to A that returns some dummy value for everything not in A, perhaps, and thus fulfils the equality on the entire type

#### Lukas Stevens (Aug 13 2020 at 10:06):

Is `Types_To_Sets` something you could use in the distribution?

#### Manuel Eberl (Aug 13 2020 at 11:28):

I think the jury is still out on that.

#### Manuel Eberl (Aug 13 2020 at 11:29):

But I think there probably wouldn't be too much opposition to it

#### Manuel Eberl (Aug 13 2020 at 11:29):

regardless, I doubt it's worth it for your example

#### Manuel Eberl (Aug 13 2020 at 11:30):

the proofs are probably pretty simple

#### Manuel Eberl (Aug 13 2020 at 11:30):

and you'd probably have to restate the theorems in their relativised form anyway if you wanted to lift them over with types-to-sets, so that still involves significant boilerplate

#### Lukas Stevens (Aug 13 2020 at 11:54):

The most annoying thing in my example is that you have to duplicate most theorems since you need to generalise the carrier `A` to `A'` and assume `A' ⊆ A` every time the theorem is proved by induction.

#### Lukas Stevens (Aug 13 2020 at 11:57):

Use types to sets is really a lot more elegant in this case (provided I can get the setup to work :laughter_tears:).

#### Manuel Eberl (Aug 13 2020 at 12:02):

I don't think you want to open that can of worms

#### Kevin Kappelmann (Aug 13 2020 at 12:06):

I remember a person saying that it is a bit worrying that there is (barely) anyone left knowing how to use types to sets - do not discourage the volunteer :laughter_tears:

#### Manuel Eberl (Aug 13 2020 at 12:07):

I said we should have people who know how to use it, I didn't say we /should/ actually use it. :P

#### Lukas Stevens (Aug 13 2020 at 12:08):

I think you can't have both at the same time :D

#### Manuel Eberl (Aug 13 2020 at 12:09):

Well, feel free to play around with it. But I'm pretty sure it is not worth the effort for your use case, even if there were not the additional obstacle of you having to learn how to use it first.

#### Manuel Eberl (Aug 13 2020 at 12:09):

I'm curious what Mikhail Chekhov is up to with types-to-sets…

Last updated: Dec 07 2023 at 08:19 UTC