Def CategoryTheory.Bicategory.LeftExtension.whiskerOfIso

Modification history

2026-10-20 15:02

Mathlib/CategoryTheory/Bicategory/Extension.lean

feat(CategoryTheory): kan extensions from isos (#41484) …

Added CategoryTheory.Bicategory.LeftExtension.whiskerOfIso View on Github →