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?

Yeah that's what types-to-sets does

probably not worth it in this case though

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

Is `Types_To_Sets`

something you could use in the distribution?

Asking because it introduces additional axioms

I think the jury is still out on that.

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

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

the proofs are probably pretty simple

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

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.

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

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

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:

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

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

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.

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

Last updated: Dec 07 2023 at 08:19 UTC