Commit 2026-10-01 17:39 53cd6f8a
View on Github →refactor(CategoryTheory): use quadrifunctors for the localized pentagon (#43009)
Refactors the localized monoidal pentagon and triangle proofs to compare natural transformations using localization extensionality. This removes the manual choice and transport of preimage objects and the associated auxiliary lemmas, and uses MonoidalCategory.ofBifunctor to construct the localized monoidal category.