Hom Functors

A hom functor for a category \(C\) is a functor \(C^{op} \times C \to Set\). In our case, we use CoqType in place of Set. The functor must send \((c, c') \in ob(C^{op} \times C)\) to the set of morphisms \(c \to c'\) in \(C\), and send a pair of morphisms \((f^{op} : c \to d, g : c' \to d')\) to the function \(Hom_C(c, c') \to Hom_C(d, d')\) which sends \((q : c \to c') \to g \circ q \circ f\).