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.

def CategoryTheory.LocallyDiscrete (C : Type u) : Type u

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

Equations

• CategoryTheory.LocallyDiscrete C = C

instance CategoryTheory.LocallyDiscrete.instInhabitedLocallyDiscrete {C : Type u} [Inhabited C] : Inhabited (CategoryTheory.LocallyDiscrete C)

Equations

• CategoryTheory.LocallyDiscrete.instInhabitedLocallyDiscrete = { default := default }

instance CategoryTheory.LocallyDiscrete.instCategoryStructLocallyDiscrete {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] : CategoryTheory.CategoryStruct.{v, u} (CategoryTheory.LocallyDiscrete C)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.LocallyDiscrete.homSmallCategory {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : CategoryTheory.LocallyDiscrete C) (Y : CategoryTheory.LocallyDiscrete C) : CategoryTheory.SmallCategory (X ⟶ Y)

Equations

• CategoryTheory.LocallyDiscrete.homSmallCategory X Y = let X' := X; let Y' := Y; CategoryTheory.discreteCategory (X' ⟶ Y')

instance CategoryTheory.LocallyDiscrete.subsingleton2Hom {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : CategoryTheory.LocallyDiscrete C} {Y : CategoryTheory.LocallyDiscrete C} (f : X ⟶ Y) (g : X ⟶ Y) : Subsingleton (f ⟶ g)

Equations

• (_ : Subsingleton (f ⟶ g)) = (_ : let X' := X; let Y' := Y; let f' := f; let g' := g; Subsingleton (f' ⟶ g'))

theorem CategoryTheory.LocallyDiscrete.eq_of_hom {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : CategoryTheory.LocallyDiscrete C} {Y : CategoryTheory.LocallyDiscrete C} {f : X ⟶ Y} {g : X ⟶ Y} (η : f ⟶ g) : f = g

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

instance CategoryTheory.locallyDiscreteBicategory (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Bicategory (CategoryTheory.LocallyDiscrete C)

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

• One or more equations did not get rendered due to their size.

instance CategoryTheory.locallyDiscreteBicategory.strict (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C)

A locally discrete bicategory is strict.

Equations

• (_ : CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C)) = (_ : CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C))

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_mapComp {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 c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.Functor.toOplaxFunctor F).mapComp f g = CategoryTheory.eqToHom (_ : F.toPrefunctor.map (CategoryTheory.CategoryStruct.comp f.as g.as) = CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f.as) (F.toPrefunctor.map g.as))

@[simp]

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.Functor.toOplaxFunctor F).toPrelaxFunctor.map₂ η = CategoryTheory.eqToHom (_ : { obj := F.obj, map := fun {X Y : CategoryTheory.LocallyDiscrete I} (f : X ⟶ Y) => F.toPrefunctor.map f.as }.map f = { obj := F.obj, map := fun {X Y : CategoryTheory.LocallyDiscrete I} (f : X ⟶ Y) => F.toPrefunctor.map f.as }.map g)

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_mapId {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (i : CategoryTheory.LocallyDiscrete I) : (CategoryTheory.Functor.toOplaxFunctor F).mapId i = CategoryTheory.eqToHom (_ : F.toPrefunctor.map (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj i))

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrefunctor_map {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : ∀ {X Y : CategoryTheory.LocallyDiscrete I} (f : X ⟶ Y), (↑(CategoryTheory.Functor.toOplaxFunctor F).toPrelaxFunctor).map f = F.toPrefunctor.map f.as

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrefunctor_obj {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : ∀ (a : I), (↑(CategoryTheory.Functor.toOplaxFunctor F).toPrelaxFunctor).obj a = F.toPrefunctor.obj a

def CategoryTheory.Functor.toOplaxFunctor {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete 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 LocallyDiscrete I to B.

Equations

• One or more equations did not get rendered due to their size.