# Documentation

Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

# Locally discrete bicategories #

A category C can be promoted to a strict bicategory LocallyDiscrete C. The objects and the 1-morphisms in LocallyDiscrete C are the same as the objects and the morphisms, respectively, in C, and the 2-morphisms in LocallyDiscrete 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 LocallyDiscrete C is defined as the discrete category associated with the type X ⟶ Y.

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

Instances For
theorem CategoryTheory.LocallyDiscrete.eq_of_hom {C : Type u} {f : X Y} {g : X Y} (η : f g) :
f = g

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

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.

A locally discrete bicategory is strict.

@[simp]
theorem CategoryTheory.Functor.toOplaxFunctor_mapComp {I : Type u₁} [] {B : Type u₂} (F : ) :
∀ {a b c : } (f : a b) (g : b c), = CategoryTheory.eqToHom (_ : F.map () = CategoryTheory.CategoryStruct.comp (F.map f.as) (F.map g.as))
@[simp]
theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrefunctor_obj {I : Type u₁} [] {B : Type u₂} (F : ) :
∀ (a : I), (().toPrelaxFunctor).obj a = F.obj a
@[simp]
theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_map₂ {I : Type u₁} [] {B : Type u₂} (F : ) :
∀ {a b : } {f g : a b} (η : f g), CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor η = CategoryTheory.eqToHom (_ : { obj := F.obj, map := fun {X Y} f => F.map f.as }.map f = { obj := F.obj, map := fun {X Y} f => F.map f.as }.map g)
@[simp]
theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrefunctor_map {I : Type u₁} [] {B : Type u₂} (F : ) :
∀ {X Y : } (f : X Y), (().toPrelaxFunctor).map f = F.map f.as
@[simp]
theorem CategoryTheory.Functor.toOplaxFunctor_mapId {I : Type u₁} [] {B : Type u₂} (F : ) :
def CategoryTheory.Functor.toOplaxFunctor {I : Type u₁} [] {B : Type u₂} (F : ) :

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 LocallyDiscrete I to B.

Instances For