mathlib documentation


Locally discrete bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A category C can be promoted to a strict bicategory locally_discrete C. The objects and the 1-morphisms in locally_discrete C are the same as the objects and the morphisms, respectively, in C, and the 2-morphisms in locally_discrete C are the equalities between 1-morphisms. In other words, the category consisting of the 1-morphisms between each pair of objects X and Y in locally_discrete C is defined as the discrete category associated with the type X ⟶ Y.

Extract the equation from a 2-morphism in a locally discrete 2-category.

@[protected, instance]

The locally discrete bicategory on a category is a bicategory in which the objects and the 1-morphisms are the same as those in the underlying category, and the 2-morphisms are the equalities between 1-morphisms.


If B is a strict bicategory and I is a (1-)category, any functor (of 1-categories) I ⥤ B can be promoted to an oplax functor from locally_discrete I to B.