Eta-conversion for the unit type is a simple feature with well-known formal metatheory, but in practical implementations it’s more often shunned than supported. The problem is that it requires type-aware conversion, and implementors prefer the comfort of the purely syntax-directed world. To date, Agda is the only big system that attempts to support it, but its support is not particularly efficient or complete. I describe improved designs in the following, which I hope to be much faster than the existing Agda version, while guaranteeing unique solutions of unification problems.