FunLike instance

Stream: Is there code for X?

[Wrenna Robson]

Is there a better way to do this and/or are there any pitfalls in this instance?

instance [FunLike F α β] : FunLike (γ → F) γ (fun _ => (a : α) → β a) where
  coe f y := f y
  coe_injective' f f' hff' := by
    simp_rw [Function.funext_iff] at hff' ⊢
    simp_rw [FunLike.ext_iff]
    exact hff'

[Yaël Dillies]

This looks pretty bad as an instance. Why do you want this?

[Wrenna Robson]

Wanted to coerce α → Equiv.Perm β to α → β → β.

[Wrenna Robson]

It works, by the by, without an obvious hitch, but it didn't look that nice...

[Wrenna Robson]

If there is some better way to do this, I am all ears.

[Yaël Dillies]

Why don't you coerce every Equiv.Perm β to β → β one by one?

[Jireh Loreaux]

For f : α → Equiv.Perm β, you could write fun a ↦ ⇑(f a), which I don't think is terrible.

[Wrenna Robson]

Yes, that's what I had essentially.

[Jireh Loreaux]

But that instance I think is really bad.

[Wrenna Robson]

If you think that's better than such an instance, then I'll go with that.

[Eric Wieser]

A CoeFun instance might be less bad, because that would at least unfold

[Kyle Miller]

There'd never be an occasion for a CoeFun instance to apply, right? γ → F is already a function

[Kyle Miller]

Jireh Loreaux said:

For f : α → Equiv.Perm β, you could write fun a ↦ ⇑(f a), which I don't think is terrible.

I probably would write that, or maybe even fun a b ↦ f a b.

Maybe there's also post-composing with docs#Equiv.toFun (assuming that the CoeFun for Equiv.Perm is just applying Equiv.toFun directly.)

[Yaël Dillies]

It's syntactically not (but defeqally yes). It is docs#FunLike.coe instead.

[Kyle Miller]

Ok, then FunLike.coe ∘ f. If (↑) ∘ f works that's probably cleanest.

[Wrenna Robson]

In some ways I suppose if Equiv.Perm automatically coerced to Function.End that might also work, though I'm not sure Bool -> Equiv.Perm would automatically coerce even so.

[Wrenna Robson]

Hmm, we don't seem to have this either.

instance Function.End.instFunLikeEnd {α : Type u} : FunLike (Function.End α) α (fun _ => α) where
  coe := id
  coe_injective' := injective_id

[Eric Wieser]

I think we don't have that because we're exploiting the defeq

[Wrenna Robson]

Aye. I just ran into somewhere where not having it was inconvenient - specifically Function.End doesn't have ext lemmas and to define them it was useful to have that instance.