The hom functor, sending (X, Y) to the type X ⟶ Y.

@[simp]

theorem CategoryTheory.Functor.hom_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : Cᵒᵖ × C} (f : X ⟶ Y) (h : X.fst.unop ⟶ X.snd), (Cᵒᵖ × C).map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.hom C).toPrefunctor X Y f h = CategoryTheory.CategoryStruct.comp f.fst.unop (CategoryTheory.CategoryStruct.comp h f.snd)

@[simp]

theorem CategoryTheory.Functor.hom_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (p : Cᵒᵖ × C) : (CategoryTheory.Functor.hom C).obj p = (p.fst.unop ⟶ p.snd)

def CategoryTheory.Functor.hom (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (Cᵒᵖ × C) (Type v)

Functor.hom is the hom-pairing, sending (X, Y) to X ⟶ Y, contravariant in X and covariant in Y.

Equations

• One or more equations did not get rendered due to their size.