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. I did not write down proofs in full detail, but I sketched them for identity types, sigma types, and coproducts and I think this also should be true for pushouts. Now, when I say that we have identity types I mean a strong version of Id:
Γ |– a : A
Γ, y:A, u:Id(a,y) |– C(y,u) type
Γ |– d : C(a,a,r(a)) type
Γ |— b : A
Γ |— p : Id(a,b)
——————————————
Γ |— J(a, (y,u)C, d, b, p) : C(b,p)
We can prove all the usual constructions for identity types using this version of J including transport and extensionality for sigma types. To define the "Frobenius version" of this J, we construct a term t : (b,p) = (a,r(a)) using extensionality for sigma. Then we transport c along t from Δ(b,p) to Δ(a,r(a)), and substitute this in d. At this point, we have a term d' of type C(a,r(a),t_*(c)). Then we use the fact that the type of triples \Sigma (q : \Sigma (b : A) Id(a,b)) Id((b,p),q) is contractible (this type is of the form \Sigma (x : A) Id(a,x) and we can prove that such types are contractible using the strong version of J). Thus, we have a path from ((a,r(a),t) to ((b,p),r((b,p))) and transporting d' along this path gives us a term of type C(b,p,c).
Similar argument shows that the "Frobenius version" of sigma eliminator is definable. We just prove that p = (\pi_1(p),\pi_2(p)) and then transport terms back and forth along this path. The proof for coproducts is slightly more difficult, but the idea is similar.
I constructed Frobenius versions of various eliminators in my recent preprint
https://arxiv.org/abs/1806.08038 (I call Frobenius eliminators "local" and the usual ones "global"). I used there a non-standard version of HoTT, but as I mentioned before I believe that it should be possible to construct them in the ordinary HoTT (with sigma and Id types only).
I also want to mention that Frobenius eliminators are definable only when our constructions are stable under substitution. If we do not assume that the type former, the constructors, and the non-Frobenius eliminator of some construction are stable under substitution, then we can interpret them in any category in which the corresponding categorical constructions are not necessarily stable under pullbacks, but this is not true for Frobenius eliminators.