3
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Trebor
    Commented Feb 23 at 16:48
  • $\begingroup$ 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? $\endgroup$
    – Jason Rute
    Commented Feb 23 at 18:34

1 Answer 1

5
$\begingroup$

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.

$\endgroup$
1
  • 3
    $\begingroup$ 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. $\endgroup$
    – Max New
    Commented Feb 27 at 4:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.