# What is the well-established η law for naturals?

Notation. ≡ means a general equality. Well, $$η$$ laws are usually judgmental, but sometimes we provide $$η$$ laws as theorems.

To me $$η$$ rules are like vibes, because there can be many $$η$$ laws for the same type. I'm mainly interested in the coproduct type, where we have:

• commuting conversions split(M, x.f(A), x.f(B)) ≡ f(split(M, x.A, x.B))
• identity expansion (unsure about the name for this one) M ≡ split(M, x. inl x, x. inr x)

I was told the full $$η$$ law for coproduct looks like this: f(M) ≡ split(M, x.f(inl x), x.f(inr x)), this is also how it is written down on nLab.

However, for recursive types, it is less clear. Natural number is a recursive type, but only identity expansion for it is obvious: M ≡ split(M, zero, x. suc x) (I hope this clarifies the type of split on naturals), the full $$η$$ law does not seem easy to write down, especially what do I do in the last argument of split.

There's a CS SE answer that said identity expansion to be the $$η$$ law for naturals, but I wonder how to do the other versions.

• The ultimate eta law should be "given two expressions G, x : Nat |- M, N : A, if G |- M[x/0] = N[x/0] and G, x : Nat |- M[x/succ x] = N[x/succ x] then M, N are judgementally equal." But this is probably never mentioned and never given this name because it has zero hope of being implemented.
– Trebor
Commented Feb 23 at 16:48
• So @Trebor, you are just saying case splitting on x (but with no “judgmental equality induction hypothesis”) and then applying judgmental equality to each case? Commented Feb 23 at 18:34

I find it's best to think of $$\eta$$ laws for inductive types in terms of their categorical semantics as initial algebras. Recall that initiality for $$(\mathbb{N},0,\mathsf{succ})$$, regarded as an initial algebra of the functor $$X \mapsto 1 + X$$, means that for any other algebra $$(X,z,s)$$ of this functor there is a unique homomorphism $$\mathsf{rec}_{(X,z,s)} : \mathbb{N} \to X$$.
For $$\mathsf{rec}_{(X,z,s)}$$ to be a homomorphism, it must be the case that $$\mathsf{rec}_{(X,z,s)}(0) = z$$ and $$\mathsf{rec}_{(X,z,s)}(\mathsf{succ}(n)) = s(\mathsf{rec}_{(X,z,s)}(n))$$ for all $$n \in \mathbb{N}$$, which is just another way of stating the $$\beta$$-law for $$\mathbb{N}$$. The $$\eta$$-law for $$\mathbb{N}$$, in its most general form, is then just the requirement that any homomorphism from $$(\mathbb{N},0,\mathsf{succ})$$ to $$(X,z,s)$$ is unique, i.e. any $$f,g : \mathbb{N} \to X$$ such that $$f(0) = g(0) = z$$ and $$f(\mathsf{succ}(n)) = g(\mathsf{succ}(n)) = s(f(n))$$ for all $$n \in \mathbb{N}$$ must be such that $$f = g$$.
In practice, as Trebor mentioned above, it's basically hopeless to implement $$\eta$$-laws in this fully general form for non-trivial inductive types, so various restrictions of these to more tractable instances often get called "$$\eta$$-laws" as well.
• I think we should be a bit more precise than "basically hopeless to implement". This $\eta$-law cannot be a definitional equality in a proof assistant because it would make definitional equality undecidable. Commented Feb 27 at 4:45