[Merged by Bors] - feat: trivial morphisms in StructuredArrow

[TwoFX]

---

[joelriou]

Suggested change

	left := eqToHom (by ext)
	left := 𝟙 _

(There are other definitions in this file where eqToHom can be replaced by the identity.)
Otherwise, I am wondering whether we could get rid of (even non simp) lemmas which introduce eqToHom in the RHS. Do you think we really need them? (They could be removed in a separate PR.)

[TwoFX]

Thanks for pointing out the unnecessary eqToHom.

Regarding your question, I'm making essential use of these lemmas #10245 (I even make them into local simp lemmas there). I think it's definitely valid to ask in which way these constructions are functorial, and stating the answer happens to require eqToHom. StructuredArrow is just one case where DTT means that eqToHom is unavoidable, given that it is usually fine to consider equality of morphisms, but not when they are objects in StructuredArrow, so I think that it makes sense to provide these tools to those people who are unfortunate enough to need them. What do you think?

[joelriou]

Actually, it is possible not to use eqToHom at all in #10245 (see the very draft commit 0d51b85 in the branch comma_presheaf_jriou). I have just tried to make the file compile without eqToHom. Most of proofs which are changed follow a similar pattern, so that it may be possible to get better automation. Then, I am not completely sure that keeping eqToHoms here is necessary the best design.

[TwoFX]

I really appreciate you taking the time to investigate this in detail. I am very happy to see that it is possible to get rid of eqToHom entirely. I had unsucessfully tried a similar approach to yours in an earlier (and much messier) version of the proof, so it's great to see that it's possible.

However, I'm not convinced that a construction of the form Quiver.Hom.op (CostructuredArrow.homMk (by exact 𝟙 _)) is a clear improvement over eqToHom _.

I see several disadvantages with the homMk (by exact 𝟙 _) approach:

• It's classic defeq abuse to forcefully supply 𝟙 _ in a place that is not syntactically (only definitionally) equal to X ⟶ X. This is exactly the kind of thing that (in my experience) will require things like simp, dsimp, simp and erw down the line, with simp not applying lemmas (even simple ones like Category.comp_id) because some object in an implicit argument isn't quite right, etc.
• Given that the functors we're dealing with in this proof are completely general presheaves (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v, it's quite difficult to actually make use of the nice definitional property (homMk (by exact 𝟙 _)).left = 𝟙 _ that this approach gets you. Indeed, you still need to group all the instances of F.map (CostructuredArrow.homMk (by exact 𝟙 _)).op together and then combine them, just like in the eqToHom approach.

The main advantage that I believe the eqToHom approach has is that I'd much rather deal with a problem I can see (eqToHom) than one I cannot see (some implicit argument being syntactically incorrect, forcing me to use some arcane combination of dsimp, simp only and erw). eqToHom is "honest" in the way that if I put eqToHom _ in some place, then its source and target will syntactically match what's expected there, and the simplifier automatically collecting and eliminating eqToHoms in the goal has worked really well for me in this proof.

Sorry for the long-winded message, but I have fought with various incarnations of this proof for a long time (in fact, apparently the first time I committed something related to this proof was in December 2022, so more than a year ago), and if I were to start over again, I would definitely want to go with the eqToHom version again.

[joelriou]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style