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

    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.

    theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_map₂ {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
    ∀ {a b : CategoryTheory.LocallyDiscrete I} {f g : a b} (η : f g), CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.Functor.toOplaxFunctor F).toPrelaxFunctor η = CategoryTheory.eqToHom (_ : { obj := F.obj, map := fun {X Y} f => }.map f = { obj := F.obj, map := fun {X Y} f => }.map g)

    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