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

def CategoryTheory.Functor.hom (C : Type u) [Category.{v, u} C] : 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.

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.hom_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Cᵒᵖ × C} (f : X✝ ⟶ Y✝) (h : Opposite.unop X✝.1 ⟶ X✝.2) : (hom C).map f h = CategoryStruct.comp f.1.unop (CategoryStruct.comp h f.2)