Dependent types I › Universes, or types of types

Summary

Suppose we wanted to define a function like that swaps the two booleans. Using the rules of and , we would write: We can use the computation rules to see that the following equations hold judgementally: These equations uniquely determine the value of for any in the sense that if we have such that and then we may construct some Indeed, we define using a dependent if-statement: Note that we do not have ; based on our , this reflects that we know describes the same boolean as , but we don’t know that it is the same description of this boolean. Because of the uniqueness of the values of that we have seen, it is very common to define such a function implicitly by just stating the equations that it is meant to satisfy. For example, you might see a definition like the following: Part of interpreting (reading) such a definition is convincing yourself that there really is a unique function that satisfies these equations, where uniqueness is taken as above in the sense of the . If you can’t prove this to yourself when you see such a definition, then you must conclude that either you have not understood the definition or that the author of the definition has made a mistake. Many computerised proof assistants, including Agda and Lean, support implicit definitions like the one above directly. Lean attempts to “understand” such a definition by converting it into an explicit one in terms of the elimination rules, and if it cannot do that, it reports an error. Agda, on the other hand, has implicit definitions primitively and does not deal with explicit definitions at all; Agda includes complicated heuristics to check whether an implicit definition is meaningful (e.g. terminating), but these heuristics have repeatedly been shown to be unsound over the years, leading to many small tweaks to the algorithm. Although there are practical trade-offs when deciding between designing a system around explicit vs. implicit definitions, we will take the position that the explicit definitions ar...