Consider the type "option A".
data option (A : Set) : Set where NONE : option A SOME : A → option A
It supports a recursion operator
option-rec : (C : Set) → C → (A → C) → option A → C
right? Given any result type C, a value of that type to use for NONE, and a function that takes any A and converts it to that result type to use for SOME, and a value of the option type, I can give you a C.
Furthermore, consider defining the natural numbers like so:
data Nat : Set where inj : option Nat → Nat
Zero is represented by inj NONE, and successor by inj o SOME.
This datatype immediately supports a recursion operator
nat-rec : (C : Set) → (option Nat → C) → Nat → C
but I also really want to know that it supports the "real" recursion operator for natural numbers:
nat-rec2 : (C : Set) → C → (C → C) → Nat → C
Is there a way I can implement nat-rec2 from option-rec and nat-rec? Is there a stronger principle I can prove of option-rec that will make it possible?