mathlib documentation


Locally discrete bicategories #

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.

def category_theory.locally_discrete (C : Type u) :
Type u

A type synonym for promoting any type to a category, with the only morphisms being equalities.

Instances for category_theory.locally_discrete

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.

@[protected, instance]

A locally discrete bicategory is strict.


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.