Pseudofunctors from locally discrete bicategories

This file provides various ways of constructing pseudofunctors from locally discrete bicategories.

Firstly, we define the constructors pseudofunctorOfIsLocallyDiscrete and oplaxFunctorOfIsLocallyDiscrete for defining pseudofunctors and oplax functors from a locally discrete bicategories. In this situation, we do not need to care about the field map₂, because all the 2-morphisms in B are identities.

We also define a specialized constructor LocallyDiscrete.mkPseudofunctor when the source bicategory is of the form B := LocallyDiscrete B₀ for a category B₀.

We also prove that a functor F : I ⥤ B with B a strict bicategory can be promoted to a pseudofunctor (or oplax functor) (Functor.toPseudofunctor) with domain LocallyDiscrete I.

def CategoryTheory.pseudofunctorOfIsLocallyDiscrete {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) : Pseudofunctor B C

Constructor for pseudofunctors from a locally discrete bicategory. In that case, we do not need to provide the map₂ field of pseudofunctors.

Equations

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

@[simp]

theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapId {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (b : B) : (pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId b = mapId b

@[simp]

theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : (pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map a✝ = map a✝

@[simp]

theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (a✝ : B) : (pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj a✝ = obj a✝

@[simp]

theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapComp {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp f g = mapComp f g

def CategoryTheory.oplaxFunctorOfIsLocallyDiscrete {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ⟶ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ⟶ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (mapComp f (CategoryStruct.comp g h)) (Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h) (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g) (map h)) (Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f) (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀) (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)) (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁)) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) : OplaxFunctor B C

Constructor for oplax functors from a locally discrete bicategory. In that case, we do not need to provide the map₂ field of oplax functors.

Equations

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

@[simp]

theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ⟶ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ⟶ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (mapComp f (CategoryStruct.comp g h)) (Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h) (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g) (map h)) (Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f) (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀) (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)) (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁)) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : (oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map a✝ = map a✝

@[simp]

theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapId {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ⟶ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ⟶ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (mapComp f (CategoryStruct.comp g h)) (Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h) (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g) (map h)) (Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f) (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀) (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)) (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁)) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (b : B) : (oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId b = mapId b

@[simp]

theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapComp {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ⟶ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ⟶ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (mapComp f (CategoryStruct.comp g h)) (Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h) (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g) (map h)) (Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f) (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀) (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)) (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁)) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp f g = mapComp f g

@[simp]

theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj {B : Type u_1} {C : Type u_2} [Bicategory B] [Bicategory.IsLocallyDiscrete B] [Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryStruct.id b) ⟶ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ⟶ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (mapComp f (CategoryStruct.comp g h)) (Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h) (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g) (map h)) (Bicategory.associator (map f) (map g) (map h)).hom) := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f) (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀) (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)) (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁)) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (a✝ : B) : (oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj a✝ = obj a✝

def CategoryTheory.Functor.toPseudoFunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) : Pseudofunctor (LocallyDiscrete C) (LocallyDiscrete D)

A functor between two categories C and D can be lifted to a pseudofunctor between the corresponding locally discrete bicategories.

Equations

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

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor_map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {X✝ Y✝ : LocallyDiscrete C} (x✝ : X✝ ⟶ Y✝) : F.toPseudoFunctor.map x✝ = (F.map x✝.as).toLoc

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor_mapId {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (x✝ : LocallyDiscrete C) : F.toPseudoFunctor.mapId x✝ = eqToIso ⋯

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor_mapComp {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {a✝ b✝ c✝ : LocallyDiscrete C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toPseudoFunctor.mapComp f g = eqToIso ⋯

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor_obj {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (x✝ : LocallyDiscrete C) : F.toPseudoFunctor.obj x✝ = { as := F.obj x✝.as }

@[reducible, inline]

abbrev CategoryTheory.Functor.toOplaxFunctor {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) : OplaxFunctor (LocallyDiscrete C) (LocallyDiscrete D)

A functor between two categories C and D can be lifted to an oplax functor between the corresponding locally discrete bicategories.

This is just an abbreviation of Functor.toPseudoFunctor.toOplax.

Equations

• F.toOplaxFunctor = F.toPseudoFunctor.toOplax

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_obj {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (x✝ : LocallyDiscrete C) : F.toOplaxFunctor.obj x✝ = { as := F.obj x✝.as }

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_mapComp {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {a✝ b✝ c✝ : LocallyDiscrete C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toOplaxFunctor.mapComp f g = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_mapId {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) (a : LocallyDiscrete C) : F.toOplaxFunctor.mapId a = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor_map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) {X✝ Y✝ : LocallyDiscrete C} (x✝ : X✝ ⟶ Y✝) : F.toOplaxFunctor.map x✝ = (F.map x✝.as).toLoc

def CategoryTheory.Functor.toPseudoFunctor' {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) : Pseudofunctor (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 a pseudofunctor from LocallyDiscrete I to B.

Equations

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

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor'_obj {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) (x✝ : LocallyDiscrete I) : F.toPseudoFunctor'.obj x✝ = F.obj x✝.as

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor'_mapComp {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) {a✝ b✝ c✝ : LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toPseudoFunctor'.mapComp f g = eqToIso ⋯

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor'_mapId {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) (x✝ : LocallyDiscrete I) : F.toPseudoFunctor'.mapId x✝ = eqToIso ⋯

@[simp]

theorem CategoryTheory.Functor.toPseudoFunctor'_map {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) {X✝ Y✝ : LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) : F.toPseudoFunctor'.map x✝ = F.map x✝.as

@[reducible, inline]

abbrev CategoryTheory.Functor.toOplaxFunctor' {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) : OplaxFunctor (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

• F.toOplaxFunctor' = F.toPseudoFunctor'.toOplax

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor'_map {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) {X✝ Y✝ : LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) : F.toOplaxFunctor'.map x✝ = F.map x✝.as

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor'_mapComp {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) {a✝ b✝ c✝ : LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toOplaxFunctor'.mapComp f g = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor'_obj {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) (x✝ : LocallyDiscrete I) : F.toOplaxFunctor'.obj x✝ = F.obj x✝.as

@[simp]

theorem CategoryTheory.Functor.toOplaxFunctor'_mapId {I : Type u_1} {B : Type u_2} [Category.{u_3, u_1} I] [Bicategory B] [Bicategory.Strict B] (F : Functor I B) (a : LocallyDiscrete I) : F.toOplaxFunctor'.mapId a = eqToHom ⋯

def CategoryTheory.LocallyDiscrete.mkPseudofunctor {B₀ : Type u_1} {C : Type u_2} [Category.{u_3, u_1} B₀] [Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) : Pseudofunctor (LocallyDiscrete B₀) C

Constructor for pseudofunctors from a locally discrete bicategory. In that case, we do not need to provide the map₂ field of pseudofunctors.

Equations

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

@[simp]

theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapId {B₀ : Type u_1} {C : Type u_2} [Category.{u_3, u_1} B₀] [Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (x✝ : LocallyDiscrete B₀) : (mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId x✝ = mapId x✝.as

@[simp]

theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj {B₀ : Type u_1} {C : Type u_2} [Category.{u_3, u_1} B₀] [Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (b : LocallyDiscrete B₀) : (mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj b = obj b.as

@[simp]

theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapComp {B₀ : Type u_1} {C : Type u_2} [Category.{u_3, u_1} B₀] [Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) {a✝ b✝ c✝ : LocallyDiscrete B₀} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp x✝ x✝¹ = mapComp x✝.as x✝¹.as

@[simp]

theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_map {B₀ : Type u_1} {C : Type u_2} [Category.{u_3, u_1} B₀] [Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryStruct.id b) ≅ CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryStruct.comp (mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryStruct.comp (Bicategory.associator (map f) (map g) (map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryStruct.comp g h)).inv))) = eqToHom ⋯ := by aesop_cat) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp (CategoryStruct.id b₀) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (mapId b₀).hom (map f)) (Bicategory.leftUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryStruct.comp (mapComp f (CategoryStruct.id b₁)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (map f) (mapId b₁).hom) (Bicategory.rightUnitor (map f)).hom) = eqToHom ⋯ := by aesop_cat) {X✝ Y✝ : LocallyDiscrete B₀} (f : X✝ ⟶ Y✝) : (mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map f = map f.as