How to mechanically derive the recursor of a type from its constructors?
Section 5.6 of the HoTT book discusses the general schema for inductive types, including how to get the corresponding induction principle.

In short, yes there is a general way to derive the elimination principle from the signature (the description of the construcotrs), and it is of course algorithmic. Coq does it, for instance, when you define an Inductive foo and it generates the eliminator foo_rect.