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