Subtypes of fun_like types

Stream: general

[Frédéric Dupuis]

On branch#dupuisf/gelfand_space_def, I found myself putting a fun_like instance on subtypes, like so:

instance subtype.fun_like (F : Sort*) (α : out_param Sort*) (β : out_param $ α → Sort*)
  [fun_like F α β] (p : F → Prop) : fun_like (subtype p) α β :=
{ coe := fun_like.coe ∘ coe_subtype.coe,
  coe_injective' := function.injective.comp fun_like.coe_injective' subtype.coe_injective }

along with the same thing for the various hom classes I needed there, such as:

instance subtype.zero_hom_class (F : Type*) (M N : out_param $ Type*) [has_zero M] [has_zero N]
  [zero_hom_class F M N] (p : F → Prop) : zero_hom_class (subtype p) M N :=
{ map_zero := λ f, zero_hom_class.map_zero _,
  ..subtype.fun_like F M (λ _, N) p }

It seems to work fine, though it did break a handful of proofs involving coe_fn_coe_base'. Is this a good idea, or am I doing something foolish here?

[Anne Baanen]

The fun_like instance is probably a good idea! My criteria:

• is there a has_coe_to_fun instance already (yes, I think it's called something like docs#coe_fn_trans) or would such an instance help produce natural notation?
• do we compare elements of this type for equality? (yes, since we have coe_fn_coe_base')

[Anne Baanen]

The only drawback I can imagine for the zero_hom_class is that we don't want to get expensive checks on the exact value of p, otherwise simp would become too slow. In this case we are completely generic in p so it is totally fine.