Question about universes and typeclasses

Stream: lean4

[Andy Soffer]

I'm trying to prove that function composition preserves injectivity, and I was able to produce the following

def Injective {α: Sort u₁} {β: Sort u₂} (f: α → β): Prop :=
  ∀x y: α, f x = f y → x = y

theorem inj {α: Sort u₁} {β: Sort u₂} {γ: Sort u₃}:
  ∀ f: β → γ, ∀ g: α → β, Injective f ∧ Injective g → Injective (f∘g) := by {
  -- omitted for brevity
}

This works just fine, but what I really want is a typeclass CompositionPreserves and then an instance of CompositionPreserves Injective to provide a bit more structure. (I'm open to the idea that I don't actually want this, but it seems nice to be able to talk generically about properties preserved by composition). So what I've tried is

class CompositionPreserves (property: {α: Sort u₁} → {β: Sort u₂} → (α → β) → Prop) where
  proof {α: Sort u₁} {β: Sort u₂} {γ: Sort u₃} (f: β → γ) (g: α → β):
    property f ∧ property g → property (f∘g)

This doesn't seem to type-check and I'm unclear as to what's going wrong. It says that f has type β → γ but should have type β → ?m.128, which I would expect to unify. Indeed, these symbols actually have mismatched sorts, where β → γ: Sort (imax u₂ u₃) but should match β → ?m.128 : Sort u₂.

I'm unclear as to why the imax is coming in to play and why the universe constraints can't be resolved. Any pointers would be greatly appreciated.

[Henrik Böving]

Your declaration of property says that it expects alpha to have sort u1 and beta to have sort u2 but clearly in the case of f that is not the case, its first argument has sort u2 and the result has sort u3

[Henrik Böving]

In order to write this down in the most general way that you are aiming here Lean would have to support universe level parameters at that position which, afaik, it doesn't. You can aim for a lesser level of generality by saying that all should be in the same universe and that would typecheck.

[Andy Soffer]

This is super helpful, thank you. I expected the universe variables to be shadowed, but I don't think that's what was going on. Renaming them does resolve that particular issue, and forcing all the types into the same universe does typecheck properly!

[Henrik Böving]

universe variables are only declared per declaration. So if you have a class all universe variables that you mention in its body will be paramters of the class itself, not individual parts of the body