I have been trying to make my way through the homotopy type theory book, slowly but surely, and I just finished reading this introductory series of 3 articles on hott on ScienceForAll.


At some point, he describes identity proofs and higher inductive types, he shows how you could construct the integers starting with a base element 0 and two constructors, up (u) and down (d), such that


for any "integer" A. Now he says that one way of reducing the complexity of the type and flattening it is to use higher order inductive types and have two identity constructors:

id_ud (n) : n = u(d(n)),

id_du (n) : n = d(u(n))

Now, my question is simply: Why can't we just make up this type by playing around with computation rules? Couldn't we just posit an induction principle that would say something like:

ind_Z (C,0) := C(0),

ind_Z (C, u(d(n))) := ind_Z (C, n),

ind_Z (C, d(u(n))) := ind_Z (C, n)

I'm aware that we'd get stuck at something like uudd(0), but then I'm sure we could have more rules to swap the ups and downs around or something.

Then, having those equalities at the definitional level, u(d(n))=n : Z (3-bar equality symbol), we would get the equality type from above u(d(n))=n (as a type). Is the problem that it's too strong?

Thank you very much

  • $\begingroup$ I don't understand what you're proposing; can you write it out in more detail? $\endgroup$ – Mike Shulman Aug 6 '14 at 19:24
  • $\begingroup$ Sorry if this is unclear, it's all very new to me. I guess I'm just confused as to why identity proof constructors would be necessary. The reason why he added the constructor for the type u(d(n))=n, was so that he could say that going up and then down was the same as not moving. But aren't computation rules there exactly for this kind of question? Why didn't he just define instead a computation rule udn=n : Z? If he later wanted to use the type udn=n, he would have had it with "ref", since the computation says that they're "the same". Maybe there is a reason why having a term udn=n is bad? $\endgroup$ – Gabriel Aug 6 '14 at 22:02
  • $\begingroup$ Ah, I think I see. I will try to answer. $\endgroup$ – Mike Shulman Aug 7 '14 at 3:06
  • $\begingroup$ Thanks. In the meantime, I reread a couple of pages on equality and identity proofs, etc. on ncatlab, and it made it somewhat clearer for me. Although, it's still confusing to me why in some cases we'd want to encode our more fundamental relations like udn=n as propositional equalities and in other cases as definitional ones, but I guess continuing reading about the subject will eventually blow away the fog. $\endgroup$ – Gabriel Aug 7 '14 at 5:48
  • $\begingroup$ My reading of the question seems to be a bit different from Mike's. I think Gabriel wants to avoid postulating identity constructors and replace them by "indistinguishability rules", i.e. what would result from substitution but without assuming that the terms are "equal" (it's unclear to me whether Gabriel means for "equal" to be propositional or definitional). I'm not sure but my hunch is that these rules could be powerful enough to recover the identity rules in the propositional sense but not in the definitional sense. $\endgroup$ – François G. Dorais Aug 7 '14 at 23:15

If I understand the question correctly, one answer is that the rules of type theory are not (supposed to be) arbitrarily chosen independently of each other like the axioms of set theory are. They come in "packages", one for each "type-forming operation", and each package has the same general shape: it consists of a Formation rule, some Introduction rules, some Elimination rules, and some Computation rules.

A Formation rule tells you how to introduce a type, e.g. "if $A$ and $B$ are types, so is $A\times B$". An Introduction rule tells you how to introduce terms in that type, e.g. "if $a:A$ and $b:B$, then $(a,b):A\times B$". An Elimination rule tells you how to use terms in that type to construct terms in other types, e.g. "if $f:A\to B\to C$, then $rec(f):A\times B\to C$". And a Computation rule tells you what happens when you apply an Elimination rule to an Introduction rule, e.g. "$rec(f)((a,b)) \equiv f(a)(b)$".

These four groups of rules that pertain to any type former can't be chosen arbitrarily either; they have to be "harmonious". There's no formal definition of what this means, but the idea is that the Introduction and Elimination rules should determine each other, and the Computation rules should tell you exactly how to apply any Elimination rule to any Introduction rule and no more.

A bit more specifically, there are two kinds of type formers: positive ones and negative ones. For a positive type, you choose the Introduction rules, and then the Elimination rules are essentially determined by saying "in order to define a function out of our new type, it suffices to specify its value on all the inputs coming from some Introduction rule". For a negative type, you choose the Elimination rules, and then the Introduction rules are essentially determined by saying "in order to construct an element of our new type, it suffices to specify how all the Elimination rules would behave on that element". In both cases, the Computation rules then say that these "specifications" do in fact hold (as definitional equalities).

So, you can't just arbitrarily postulate Computation rules. I mean, you can, but you won't end up with a well-behaved theory. Thus, we have to regard the equalities postulated by higher inductive types as Introduction rules, with correspondingly determined Elimination and Computation rules. (We could try to make them Elimination rules instead, yielding a notion of "Higher Coinductive Type", but there's no consensus yet on what such a thing should look like.)

Why do we require this sort of harmony between the rules? From a computational point of view, it's so that we can actually compute with the Computation rules. If you didn't have that sort of harmony, then you might end up with "stuck" terms with an Elimination form applied to an Introduction form but no applicable Computation rule, or conversely if there were too many Computation rules then you might have some terms that try to "compute" to many different things.

From a category-theoretic point of view, it's because we're specifying objects by universal properties: a positive type former has a "left" universal property like a colimit, while a negative type former has a "right" universal property like a limit. I wrote a blog post about this here.


A different answer is that one of the purposes of higher inductive types is to define homotopy types containing nontrivial paths. The judgmental equalities coming from computation rules cannot give rise to nontrivial paths, because there is no way for two things to be "judgmentally equal in more than one way". By contrast, two things can be propositionally equal in more than one way (because an equality type can contain more than one term), so we can regard those as paths.

Higher inductive types also make sense in "extensional type theory" where there is no (or little) distinction between propositional and judgmental equality, and in this case it is true that every path-constructor of a HIT gives rise to a judgmental equality as well as a propositional one. In this case, they are less interesting, since all types are 0-truncated, but they still have a good deal of uses. However, at a basic level the path-constructors are still Introduction rules for the reasons described in my other answer, with the resulting judgmental equalities coming from the "reflection rule" of extensional type theory.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.