Documentation

Mathlib.CategoryTheory.Functor.Hom

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    @[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) :