Theorems · Definition · category theory

CategoryTheory.presheafHom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        CategoryTheory.Functor Cᵒᵖ A →
          CategoryTheory.Functor Cᵒᵖ A → CategoryTheory.Functor Cᵒᵖ (Type (max (max u v) v'))

Given two presheaves F and G on a category C with values in a category A, this presheafHom F G is the presheaf of types which sends an object X : C to the type of morphisms between the "restrictions" of F and G to the category Over X.

Defined in

Mathlib.CategoryTheory.Sites.SheafHom

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category