I can give some thoughts. Summary: Coq already has a version of this for products, I don’t believe sums pose any fundamental problems, but with generalizations, in particular terminal coalgebras or the initial object you often lose decidable type-checking.
The primitive projections feature allows products with definitional eta (so your first equation).
I think I remember reading a paper about a (non-dependent) type theory with this eta rule for sums (your second equation), maybe using binary decision diagrams as normal forms? But I can’t find it right now.
If you redefine
nat as the (isomorphic)
1 + nat, your third equation reduces to the second (well, if you have definitional eta for
1, which Coq also doesn’t, because it’s internal conversion checking is untyped and getting strict eta for
1 in this setting appears impossible).
You may have meant a more recursive version where any
fix rec n := match n with O => a | S n => h (rec n) end = f whenever
f O = a and
f (S n) = h (f n).
conat, your proposed equation implies
n = match n with co0 => co0 | coS c => coS c end, but then I believe decidable type checking is impossible by reduction to the halting problem.
Take a Turing machine, and define
n by coinduction on the state to be
coS (next state) when the machine steps, and
infinity when the machine halts. Then ask if
n = infinity. If the machine ever halts, then
n = infinity after expanding both by the number of steps taken. If the machine never halts, then
infinity will never be the same (I think, my reasoning here is fuzzy), since
n will always be a cofixpoint over the state and
infinity a cofixpoint over unit. I don’t think the other consequences of your fourth equation span the gap, but I could be wrong.
However, if you define
1 + conat, then definitional eta for sum implies your fourth equation, modulo the same caveat as with nat.
For a more solid example of where strict eta for coinductive types can go wrong, see section 1 of “Grins from my Ripley Cupboard” by Conor McBride.
There is an obvous generalization from sums to the initial type
void, which is that
f = \x -> match x with end when
f : 0 -> A. This also prevents decidable type checking, with the argument spelled out in section 3 of the above linked note by Conor McBride.