Commit 2024-08-22 13:53 b35703fe
View on Github →feat(Category/Cat): add API lemmas (#16064)
This PR adds more API lemmas about the bicategory of categories Cat. These are added as simp is not able to use the corresponding NatTrans lemmas when working with 2-morphisms in the bicategory Cat.
Due to this some proofs in CategoryTheory/Grothendieck can be golfed.