 of (dependent) functions on these by recursion and induction
These are implemented using several layers of recursive definitions and diagonals (i.e., fixed points). In HoTT,
recursion and induction are applications of (dependent) functions <code>rec_W,X</code> and  <code>ind_W, Xs</code> to the <code><code>definition data</code></code>.</p><p>It is useful to capture information regarding inductive types and the recursion and induction functions in scala types. Our implementation
is designed to do this.</p>