Post #2103990

Just picked up from "Logical Relations as Types" the practice of not saying the words "beta rule" and "eta rule" and instead saying "computation rule" and "uniqueness rule". I feel like I would have been much happier if people had used this terminology when I originally learned type theory, and I'm definitely going to use it next time I teach someone. While I'm on that subject... I like thinking about the four rules as answers to the four questions. How can I make an element of this type? How can I use an element of this type? What happens when I use an element of this type? Are there any other sneaky elements of this type? (No!)