Struggling with implicit type level arguments

Stream: new members

[Tomáš Jakl]

I'm trying to define custom Subobject akin to what's in Mathlib.CategoryTheory.Subobject.Basic but parameterised by a MorphismProperty and I'm constantly hitting issues with implicit arguments of type levels.

In particular, if I start with the following:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Subobject.Basic

namespace CategoryTheory

universe u_1 u_2
variable {C : Type u_1} [Category.{u_2, u_1} C] {Δ : MorphismProperty C}

def StgOver (X : C) :=
  ObjectProperty.FullSubcategory (fun f : Over X => Δ f.hom)
  -- replacing original line in Mathlib.CategoryTheory.Subobject.Basic:
  --   ObjectProperty.FullSubcategory (fun f : Over X => Mono f.hom)

and then I would like to define the variant of Subobject for which I need the Category instance. However, both of these fail if I just use the same formulas as for the original definition of Subobject.

instance (X : C) : Category (StgOver X) :=
  ObjectProperty.FullSubcategory.category _
-- error: don't know how to synthesize implicit argument 'Δ' ...

def StgSub (X : C) := ThinSkeleton (StgOver X)
-- error: failed to synthesize Category.{?u.982, max u_2 u_1} (StgOver X)

What is really strange is that I get errors without even invokingThinSkeleton. Namely, already this fails

def JustRename (X : C) := (StgOver X)
-- error: don't know how to synthesize implicit argument 'Δ' ...

It's probably something trivial but I'm a bit lost with this. Any pointers highly appreciated!

[Vlad]

StgOver X (Δ := Δ)

[Tomáš Jakl]

Wow, magic! Thanks so much!

[Kyle Miller]

Given that X doesn't determine Δ, maybe Δ should be an explicit argument to StgOver as well?

[Tomáš Jakl]

If I have to always write (Δ := Δ) then I'd consider it. I'll see how things go as I encode more maths. It would be nice to guide it somehow...

[Kyle Miller]

Maybe the Δ in the type of StgOver will be enough, but you'll likely need to use (Δ := Δ) frequently.

At least as an explicit argument you can write StgOver _ X, so it's not that onerous.

Anyway, no need to worry about it now, since you'll find out soon enough which is more convenient!

[Tomáš Jakl]

Good advice, I'll keep it in mind. Thanks!

[Tomáš Jakl]

Actually, just tried to do as you say and it still fails to synthesize the argument for _...

[Kyle Miller]

Right, in that case you need to write StgOver Δ X

[Kyle Miller]

The point is that you can write _ when it can figure it out from the expected type, but _ has the same failures as if it were an implicit argument.

[Tomáš Jakl]

Writing this in every application would still be too annoying (it's one of the main operations I plan to use). I guess that the solution to this is to define a custom class which would extend Category with extra data for Δ.