Providing implicit arguments to a function field

Stream: general

[Lime Sublime]

Suppose I have code like

universe l
structure Thing : Type (l + 1) :=
    (Obj : Type l)
    (Arr : Obj → Obj → Type l)
    (id : ∀ {a} , Arr a a)

variables (A  B : Thing) (f : A.Obj -> B.Obj)

def foo : ∀ a, B.Arr (f a) (f a)
  := λ a, let bid := B.id in @bid (f a)

I would like to avoid the let binding, but Lean complains at both @B.id and B.@id. Is there anything I can do?

[Yakov Pechersky]

def foo : ∀ a, B.Arr (f a) (f a)
  := λ a, Thing.id _

[Lime Sublime]

EDIT: This was wrong, sorry (I get a "too many arguments" error message when trying that)

[Reid Barton]

I don't understand why B.id doesn't work, something weird about implicit argument insertion and dot notation? sounds vaguely familiar...

[Yakov Pechersky]

Does this not work for you @Lime Sublime ?

universe l
structure Thing : Type (l + 1) :=
    (Obj : Type l)
    (Arr : Obj → Obj → Type l)
    (id : ∀ {a} , Arr a a)

variables (A  B : Thing) (f : A.Obj -> B.Obj)

def foo : ∀ a, B.Arr (f a) (f a)
  := λ a, Thing.id _

#check foo A B f

[Lime Sublime]

That code works for me! Unfortunately, the solution produces an error in a larger section of code. Trying to build a repro now

[Reid Barton]

If you need to give an explicit argument for some reason then another option is @Thing.id B (f a)

[Lime Sublime]

In fact it does work, @Yakov Pechersky ! Thanks! How did you generate the fix?

[Yakov Pechersky]

I took Reid's suggestion from earlier for the notation to just use the structure's field instead of relying on projection notation

[Floris van Doorn]

Yeah, you cannot combine the @ with the projection notation (dot notation), so in that case you have to just write the full name of the projection.