Def Mathlib.Tactic.BicategoryCoherence.bicategoricalIso

Modification history

2024-07-17 18:39

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

chore(CategoryTheory/Bicategory): split the bicategorical composition (#14815) …

Deleted Mathlib.Tactic.BicategoryCoherence.bicategoricalIso View on Github →

2023-06-07 03:09

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

feat: port CategoryTheory.Bicategory.CoherenceTactic (#4610)

Added Mathlib.Tactic.BicategoryCoherence.bicategoricalIso View on Github →