Implicit parameters in `pullback.fst` and `pullback.snd`

Stream: mathlib4

[Calle Sönne]

pullback.fst and pullback.snd only have implicit parameters. For example pullback.snd is defined as follows:

/-- The second projection of the pullback of `f` and `g`. -/
abbrev pullback.snd {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] : pullback f g ⟶ Y :=
  limit.π (cospan f g) WalkingCospan.right

When working with multiple pullbacks (and more complicated diagrams) the fact that all variables here are implicit can make it really hard to read. Here is a concrete example:

theorem pullbackAssoc_hom_snd_snd [HasPullback ((pullback.snd : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd ≫ pullback.snd = pullback.snd := by

It is not immediately clear exactly which pullbacks these projections are referring to, unless you write down the diagrams yourself (and all three are referring to projections of different pullbacks!). Here in the hypotheses, one also needs to specify the type of pullback.snd and pullback.fst, since the arguments are all implicit.

I have found this quite inconvenient, but are there good reasons for why these arguments should be implicit? Would it be a bad idea to try to make them explicit?

[Kevin Buzzard]

My instinct is to make them explicit, I remember @Mario Carneiro once telling me that the rules for what's explicit in defs are different to the rules for what's explicit in theorems. The other possibility is ASCII art diagrams in the docstring making it clear what's going on

[Markus Himmel]

I think this is a historical accident. It goes all the way back to mathlib#1339 (from the early-ish days of mathlib3) and my guess would be that it hasn't really been challenged since then. It's interesting that prod.fst and friends have the same problem, while equalizer.ι and friends do not. I don't see a pattern that would explain this. In Lean 4 you can provide the relevant morphisms by using the syntax pullback.snd (f := ...) (g := ...). I would say that PR making the parameters explicit would be welcome. Hopefully you can just add _ _ to all existing uses and nothing breaks.

[Dagur Asgeirsson]

I’d be in favor of making them explicit

[Calle Sönne]

Okay cool! I will try to make these explicit then :)

[Kim Morrison]

Yes, I agree, it was an experiment we can now declare to have failed.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I just came across this. Has there been any progress on explicitification?

[Calle Sönne]

Yes! pullback.fst/snd and pushout.inr/inl have explicit arguments now :)

[Calle Sönne]

Although most of the replacing was automatic, so I'm sure there are still places where it is written like (pullback.fst _ _ : pullback f g ⟶ _)