Commit 2025-04-25 04:02 50ab41a8

feat(Bicategory/Oplax): Fix simp lemmas and renaming (#18252) This PR renames OplaxNatTrans to OplaxTrans and puts it in the Oplax namespace (as there should also be oplax natural transformations between lax functors, so this is more fitting). It also removes @[simp] from OplaxTrans.id and OplaxTrans.vcomp, and instead adds @[simp!] to the CategoryStruct instance. This is needed as for example, right now, in order to prove that (η ≫ θ).app a = η.app a ≫ θ.app a simp needs to first convert this to (OplaxTrans.vcomp η θ).app a which is not ideal (in particular it converts (η ≫ θ) to OplaxTrans.vcomp η θ). This is part of some of the restructuring that I want to do before constructing the bicategory of pseudofunctors.