# mathlibdocumentation

category_theory.bicategory.locally_discrete

# 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.

Equations
Instances for category_theory.locally_discrete
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem category_theory.locally_discrete.eq_of_hom {C : Type u} {X Y : category_theory.locally_discrete C} {f g : X Y} (η : f g) :
f = g

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.

Equations
@[protected, instance]

A locally discrete bicategory is strict.

@[simp]
theorem category_theory.functor.to_oplax_functor_map_id {I : Type u₁} {B : Type u₂} (F : I B)  :
@[simp]
theorem category_theory.functor.to_oplax_functor_obj {I : Type u₁} {B : Type u₂} (F : I B) (ᾰ : I) :
= F.obj
@[simp]
theorem category_theory.functor.to_oplax_functor_map₂ {I : Type u₁} {B : Type u₂} (F : I B) (i j : category_theory.locally_discrete I) (f g : i j) (η : f g) :
def category_theory.functor.to_oplax_functor {I : Type u₁} {B : Type u₂} (F : I B) :

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.

Equations
@[simp]
theorem category_theory.functor.to_oplax_functor_map_comp {I : Type u₁} {B : Type u₂} (F : I B) (i j k : category_theory.locally_discrete I) (f : i j) (g : j k) :
@[simp]
theorem category_theory.functor.to_oplax_functor_map {I : Type u₁} {B : Type u₂} (F : I B) (X Y : category_theory.locally_discrete I) (f : X Y) :
= F.map f.as