The hom functor, sending (X, Y) to the type X ⟶ Y.
functor.hom is the hom-pairing, sending (X,Y) to X → Y, contravariant in X and covariant in Y.
@[simp]
theorem
category_theory.functor.hom_obj
(C : Type u)
[category_theory.category C]
(X : Cᵒᵖ × C) :
(category_theory.functor.hom C).obj X = (opposite.unop X.fst ⟶ X.snd)
@[simp]
theorem
category_theory.functor.hom_pairing_map
(C : Type u)
[category_theory.category C]
{X Y : Cᵒᵖ × C}
(f : X ⟶ Y) :
(category_theory.functor.hom C).map f = λ (h : (category_theory.functor.hom C).obj X), f.fst.unop ≫ h ≫ f.snd