 where we have omitted the common context \(\Gamma\), since the types of these constants are closed. Note that the recursion operator \(R\) has a first argument \(C {:} \N \rightarrow \Set\) unlike in the original formulation.