Hi Peter,
I've been thinking about such eliminators lately too. It seems that they are derivable from ordinary eliminator for most type-theoretic constructions as long as we have identity types and sigma types.
Thankyou — very nice observation, and (at least to me) quite surprising!
I mean a strong version of Id:
Side note: this is I think more widely known as the Paulin-Mohring or one-sided eliminator for Id-types; the HoTT book calls it based path-induction.
Ah, yes — there was a mistake in the argument I had in mind. In that case, do we really know for sure that the Frobenius versions are really strictly stronger?
–p.