Commit 2024-07-17 18:39 fa249230

View on Github →

chore(CategoryTheory/Bicategory): split the bicategorical composition (#14815) Similar to #11149.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Bicategory/Adjunction.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CategoryTheory/BicategoricalComp.lean

added def CategoryTheory.bicategoricalComp

added theorem CategoryTheory.bicategoricalComp_refl

added def CategoryTheory.bicategoricalIso

added def CategoryTheory.bicategoricalIsoComp

Modified Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

deleted def Mathlib.Tactic.BicategoryCoherence.bicategoricalComp

deleted theorem Mathlib.Tactic.BicategoryCoherence.bicategoricalComp_refl

deleted def Mathlib.Tactic.BicategoryCoherence.bicategoricalIso

deleted def Mathlib.Tactic.BicategoryCoherence.bicategoricalIsoComp

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

Modified scripts/noshake.json