Commit 2024-04-25 15:18 bdc67338

View on Github →

feat(CategoryTheory/Bicategory/LocallyDiscrete): Make LocallyDiscrete a structure (#12383) Made LocallyDiscrete a structure, similar to Discrete, and added some basic API. Coherence.lean was also adjusted because of these changes. This should make it easier to move between a given type C and LocallyDiscrete C.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Coherence.lean

modified theorem CategoryTheory.FreeBicategory.preinclusion_obj

Modified Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

added def CategoryTheory.Functor.toPseudoFunctor

added theorem CategoryTheory.LocallyDiscrete.comp_as

added theorem CategoryTheory.LocallyDiscrete.id_as

added def CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv

added theorem CategoryTheory.LocallyDiscrete.mk_as

added structure CategoryTheory.LocallyDiscrete

deleted def CategoryTheory.LocallyDiscrete

added theorem Quiver.Hom.comp_toLoc

added theorem Quiver.Hom.id_toLoc

added def Quiver.Hom.toLoc