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)`

.

For `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 `n`

and `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 `conat`

as `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 `0`

or `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.