Type Formulation Question

Stream: new members

[Petur Vetle]

I'm reading the early chapters of the Homotopy Type Theory: Univalent Foundations of Mathematics textbook and a few other resources to get a better grasp of type theory. According to the textbook, when defining a new type one must specify its formulation, introduction, elimination, and computation rules.

Going through the basic types (e.g. products/co-products), the elimination and computation rules seem to be determined by its formulation and introduction rules. In general, is this true?

The only one basic type that seems to break the pattern that I see is the elimination rule for the Equality/Identification type.

[Kevin Buzzard]

This is not correct. When defining a new type, the system specifies all those rules for you, you don't have a say in the matter.

[Kevin Buzzard]

It's probably also worth mentioning, given that you are posting in a Lean chatroom, that when the univalent foundations book talks about a type, they mean a higher type; these don't exist in Lean, we only have "lower types", i.e. a type in Lean is what the univalent people would call a set. A higher type has a very rich structure involving identities, and identities between identities etc etc; Lean's types only have equalities like you would expect in normal set theory, i.e. any two proofs of a = b are by definition equal, if a and b are terms of a type in Lean. This is not at all true in a univalent system.