Trebor on Nostr: nprofile1q…ndand Now that I think of it, eta for unit types seems really bad for ...

nprofile1qyt8wumn8ghj7un9d3shjtnyd968gmewwp6kytcqyp2aucj8nm0d5n2ls2z3dy2z5udpsplzpjq60kur0q9qfax33370cyndand (nprofile…dand) Now that I think of it, eta for unit types seems really bad for rewriting systems. Do we define a family of reductions, one for each type? Otherwise an untyped reduction can only turn the constructor of Unit into a (fresh) variable, because no other direction makes sense. But then confluence is dead. (I'm assuming eta because this thread is specifically about eta.)