Documentation

Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

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.

source
@[simp]
theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
∀ (a : B), (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj a = obj a
source
@[simp]
theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapId {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (b : B) :
(CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId b = mapId b
source
@[simp]
theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
∀ {X Y : B} (a : X ⟶ Y), (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map a = map a
source
@[simp]
theorem CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapComp {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp f g = mapComp f g
source
def CategoryTheory.pseudofunctorOfIsLocallyDiscrete {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
CategoryTheory.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.
Instances For
    source
    @[simp]
    theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapComp {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom)) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
    ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp f g = mapComp f g
    source
    @[simp]
    theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom)) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
    ∀ (a : B), (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj a = obj a
    source
    @[simp]
    theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_map {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom)) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
    ∀ {X Y : B} (a : X ⟶ Y), (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map a = map a
    source
    @[simp]
    theorem CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapId {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom)) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (b : B) :
    (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId b = mapId b
    source
    def CategoryTheory.oplaxFunctorOfIsLocallyDiscrete {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] [CategoryTheory.Bicategory C] (obj : B → C) (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) = CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h)) (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom)) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁)) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
    CategoryTheory.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.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_map {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      ∀ {X Y : CategoryTheory.LocallyDiscrete I} (x : X ⟶ Y), F.toPseudoFunctor.map x = F.map x.as
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_obj {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      ∀ (x : CategoryTheory.LocallyDiscrete I), F.toPseudoFunctor.obj x = F.obj x.as
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_mapId {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      ∀ (x : CategoryTheory.LocallyDiscrete I), F.toPseudoFunctor.mapId x = CategoryTheory.eqToIso ⋯
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_mapComp {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      ∀ {a b c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c), F.toPseudoFunctor.mapComp f g = CategoryTheory.eqToIso ⋯
      source
      def CategoryTheory.Functor.toPseudoFunctor {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      CategoryTheory.Pseudofunctor (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 a pseudofunctor from LocallyDiscrete I to B.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_map {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
        ∀ {X Y : CategoryTheory.LocallyDiscrete I} (x : X ⟶ Y), F.toOplaxFunctor.map x = F.map x.as
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_mapId {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
        ∀ (x : CategoryTheory.LocallyDiscrete I), F.toOplaxFunctor.mapId x = CategoryTheory.eqToHom ⋯
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_mapComp {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
        ∀ {a b c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c), F.toOplaxFunctor.mapComp f g = CategoryTheory.eqToHom ⋯
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_obj {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
        ∀ (x : CategoryTheory.LocallyDiscrete I), F.toOplaxFunctor.obj x = F.obj x.as
        source
        def CategoryTheory.Functor.toOplaxFunctor {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} I] [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.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapComp {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
          ∀ {a b c : CategoryTheory.LocallyDiscrete B₀} (x : a ⟶ b) (x_1 : b ⟶ c), (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp x x_1 = mapComp x.as x_1.as
          source
          @[simp]
          theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (b : CategoryTheory.LocallyDiscrete B₀) :
          (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj b = obj b.as
          source
          @[simp]
          theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_map {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
          ∀ {X Y : CategoryTheory.LocallyDiscrete B₀} (f : X ⟶ Y), (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map f = map f.as
          source
          @[simp]
          theorem CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapId {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
          ∀ (x : CategoryTheory.LocallyDiscrete B₀), (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId x = mapId x.as
          source
          def CategoryTheory.LocallyDiscrete.mkPseudofunctor {B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : autoParam (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_left_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) (map₂_right_unitor : autoParam (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯) _auto✝) :
          CategoryTheory.Pseudofunctor (CategoryTheory.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.
          Instances For