API for avoiding defeq abuse with Cat 2-morphisms

Stream: Is there code for X?

[Edward van de Meent]

other than by abusing defeq, how does one lift natural transformations (and isos) between functors to 2-(iso)morphisms in Cat? I couldn't find any API for this...
context: I wrote a definition of Bicategory.pseudoCoyoneda : Bᵒᵖ ⥤ᵖ B ⥤ᵖ Cat, and only afterwards discovered that docs#CategoryTheory.Functor.toCatHom is a thing. After changing my code to using it, a lot of code broke, because suddenly simping no longer reduces things like F.toCatHom.obj X -> G.toCatHom.obj X (where F and G are stand-ins for specific functors i'm defining)

[Calle Sönne]

This is not answering to your question, but in #30927 I define the yoneda pseudofunctor (and I am happy to collaborate on this to be clear, I have not yet managed to prove it is a biequivalence, and I also have not added coyoneda).

Also I am not sure either if there is any API for this as far as I know.

[Edward van de Meent]

I had no idea someone else was working getting this to mathlib, this is great to learn :tada:
Since this API not there, should i see if i can make a PR with some basics?

[Calle Sönne]

Yes that definitely sounds like a good idea!

[Edward van de Meent]

(experimental) PR at #31807

[Edward van de Meent]

turns out, Grothendieck abuses the heq out of this defeq.

[Edward van de Meent]

update: i've managed to make all of mathlib compile with the change that the 1- and 2-morphisms in Cat are 1-field structures (called Cat.Hom and Cat.Hom₂ respectively) in #31807 . I'm decently satisfied with the simp set i made for converting back and forth between the Cat-morphisms and Functors or NatTrans'. (i made the 1-field structure change because it is the easiest way to see where the defeq is being abused, and it forces me to build API around avoiding the defeq. it can be reversed if people want.)

[Edward van de Meent]

or, well, it compiled before i merged current mathlib. :work_in_progress:

[Edward van de Meent]

it builds :tada: