Commit 2024-05-23 03:28 57cb4371

feat(Algebra/Category/*): simp lemmas for unbundled comp and categorical identities (#13109) These are useful in "mixed contexts" where we have categorical morphisms combined in "non-categorical" ways.