Is there a table somewhere of the commonly used types along with the formation rules, constructors, eliminators, computation rules, recursors and inductions ?

Whenever I'm going an exercise I have to keep flicking back and forth to find the appropriate definition.

  • $\begingroup$ Have you looked at Section A.2 of the homotopy type theory book? For instance the rules for dependent functions and dependent pairs are listed in Sections A.2.4 and A.2.5. $\endgroup$ – Ingo Blechschmidt Nov 29 '16 at 10:05
  • $\begingroup$ It's almost what I want. I think the best solution is for me to write my own. $\endgroup$ – Q the Platypus Nov 29 '16 at 22:52
  • 1
    $\begingroup$ If you do so, then consider linking to it here, so others can benefit from your work as well. :-) Note that the TeX source of the homotopy type theory book is available online, so you might be able to save some typesetting work. $\endgroup$ – Ingo Blechschmidt Nov 30 '16 at 9:48

Check out this attempt:


So far, I added chapter 2 content.


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.