Is there a class for "composition of funlikes"?

Stream: Is there code for X?

[Wrenna Robson]

So we have DFunLike/FunLike. Many FunLike classes have a comp operation which has the property that the function coercion of the composition of two members is the composition of the individual coercions. Is there a class for this?

[Wrenna Robson]

It occurs to me that there's a lot of general theorems that essentially arise from this.

[Edward van de Meent]

i don't think that exists as of yet...
Basically something like this?

class FunLikeCompClass (F₁ : Sort*) {α β : outParam (Sort*)} [FunLike F₁ α β] (F₂ : Sort*) {γ : outParam (Sort*)} [FunLike F₂ β γ] (F₃ : outParam Sort*) [FunLike F₃ α γ] where
  comp (f₂ : F₂) (f₁ : F₁) : F₃
  coe_comp_eq_coe_comp_coe (f₂ : F₂) (f₁ : F₁) : ⇑(comp f₂ f₁) = ⇑(f₂) ∘ ⇑f₁

[Jireh Loreaux]

We don't have it for a reason, which is basically that Lean can't generally infer the types. There's an issue that talks about a different design which might allow for this. It's Yury's #2000-something

[Jireh Loreaux]

(not actually 2000, it's 2xxx)

[Wrenna Robson]

I was just thinking that - relatedly - I was building lifts for various types, and thinking how much it felt like a general method would be useful.

[Wrenna Robson]

On this: I created #26071 just to experiment with it a little, and it seems to work with a little massaging. I realised really one could use a similar thing to generalise "having an identity" and generalising Equiv.symm for EquivLike, which would be quite nice.

[Wrenna Robson]

Would appreciate thoughts and demonstrations of where this doesn't work. I didn't find @Yury G. Kudryashov's PR yet!

[Yury G. Kudryashov]

My approach was to replace DFunLike with a common structure

structure BundledHom (X Y : Type*) (Pred : (X -> Y) -> Prop) where
  toFun : X -> Y
  isValid : Pred toFun

then using classes like

class BundledHom.Composable {X Y Z : Type*} (PredYZ : (Y -> Z) -> Prop) (PredXY : (X -> Y) -> Prop) (PredXZ : outParam ((X -> Z) -> Prop)) where
  isValid_comp {g f} : PredYZ g -> PredXY f -> PredXZ (g \o f)

I had a PR with a similar refactor for SetLikes (partial progress) but it wasn't merged for a few reasons:

• this would rule out, e.g., Finsupp and Finset from using this infrastructure;
• for bundled homs, I don't see how to make it work with equivalences;
• for many instances that came to my mind (e.g., a common order/lattice structure on BundledSets) people came up with examples where it doesn't make sense.