Theorems · Definition · category theory

CategoryTheory.LocallyDiscrete.mkPseudofunctor

{B₀ : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} B₀] →
      [inst_1 : 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)) →
                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 ⋯)
                    CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_1 →
                  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 ⋯)
                      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_3 →
                    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 ⋯)
                        CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_5 →
                      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.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Cited by

4 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Bicategory