Theorem CategoryTheory.FreeBicategory.preinclusion_obj

Modification history

2024-04-25 15:18

Mathlib/CategoryTheory/Bicategory/Coherence.lean

feat(CategoryTheory/Bicategory/LocallyDiscrete): Make LocallyDiscrete a structure (#12383) …

Modified CategoryTheory.FreeBicategory.preinclusion_obj View on Github →

2023-05-28 08:49

Mathlib/CategoryTheory/Bicategory/Coherence.lean

feat: port/CategoryTheory.Bicategory.Coherence (#4062)

Added CategoryTheory.FreeBicategory.preinclusion_obj View on Github →