Theorems · Definition · category theory

CategoryTheory.Functor.pi

{I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₂} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
          ((i : I) → CategoryTheory.Functor (C i) (D i)) → CategoryTheory.Functor ((i : I) → C i) ((i : I) → D i)

Assemble an I-indexed family of functors into a functor between the pi types.

Defined in

Mathlib.CategoryTheory.Pi.Basic

Cited by

29 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category