CategoryTheory.Bicategory.Functor !4#2301

Stream: mathlib4

[Kevin Buzzard]

@Adam Topaz and I have got a vested interest in getting some category theory ported, because we're giving a workshop on some of the basic aspects of Clausen/Scholze in Lean 4 in a few months. Adam challenged me to port Bicategory.Functor but so far it's been relatively straightforward. I'm unlikely to spend any time on this for the next 4 hours because I'll be at the IPAM talks, so I've pushed what I have.

[Kevin Buzzard]

I might do some live porting at lunchtime maybe

[Kevin Buzzard]

(working on this file again)