Theorems · Definition · category theory

CategoryTheory.Grothendieck.functorFrom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {E : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} E] →
          (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) →
            (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) →
              (∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) →
                (∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
                    hom (CategoryTheory.CategoryStruct.comp f g) =
                      CategoryTheory.CategoryStruct.comp (hom f)
                        (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g))
                          (CategoryTheory.eqToHom ⋯))) →
                  CategoryTheory.Functor (CategoryTheory.Grothendieck F) E

Construct a functor from Grothendieck F to another category E by providing a family of functors on the fibers of Grothendieck F, a family of natural transformations on morphisms in the base of Grothendieck F and coherence data for this family of natural transformations.

Defined in

Mathlib.CategoryTheory.Grothendieck

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category