def Category.Hom {OA : Sort u_1} {A : OA → OA → Sort u_2} [𝓐 : Category A] : Category.Op A ⨂ A ⥤ Category.Fun

Represents the hom functor as an explicit bifunctor.

Equations

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