# Definitional equalities for universal properties?

If we view user-defined types as having the universal properties of sums, products, intial algebras, terminal coalgebras, etc. as a category theoretic perspective would suggest, we might want definitional equalities like the following (when well-typed):

``````f ≡ λ x, match f x with
| (a, b) => (a, b)
end

f ≡ λ s, match s with
| inl a => f (inl a)
| inr b => f (inr b)
end

f ≡ λ n, match n with
| 0 => f 0
| S n' => f (S n')
end

f ≡ λ x, match f x with
| co0 => co0
| coS c => coS c
end
``````

etc.

Would it potentially be acceptable to add these equalities when a type is defined, presumably behind some flag? I’m guessing we’d want them in the same order as eta equivalence, i.e. expansion?

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.

1 Like

Deciding equality with eta for sums in a simply typed setting is showed (not the earliest proof) in “Deciding equivalence with sums and the empty type” ,
Gabriel Scherer, POPL 2017.
But now that I’m re-reading Conor’s argument for the undecidability of conversion with eta for empty types, I’m wondering whether we could adapt part of it to the case of binary sums (in a dependent setting ofc).