Question regarding terminology regarding injectivity of objects:
(1) An object D is called injective over an arrow j:X->Y if the
"restriction map"
hom(Y,D) -> hom(X,D)
g |-> g o j
is a surjection. This is fairly standard terminology (where does it come
from, by the way).
(2) I am working with the situation where the restriction map is a
*split* surjection.
I thought of the terminology "D is split injective over j", but perhaps
this is awkward. Is there a standard terminology for this notion. Or,
failing that, a terminology that at least one person has already used in
the literature or in the folklore. Or, failing that too, a good
suggestion by any of you?
(Before anybody says that there is no difference assuming choice, I remark that I am interested in the "infty-category of types (in a universe)" in HoTT/UF, where the homs are infty-groupoids and so the section has to be a morphism, not just a theoretical function.)
Thanks,
Martin