UF IAS 2012 Archive The book

---

The HoTT Book is now done!

Get it here.

---

Github repository

The book is available at the HoTT/book repository on Github. If you are one of the contributors, you should have push access (which means that you can make changes) to the repository, which means you should be on Team book (link possibly only for admins). If you are not, talk to the technical dictator. You will need to create a github account (it’s free).

Slides on using Git: StepByStepGit.pdf Link to cheatsheet: GIT_CHEATSHEET.txt

If you would rather not learn to use git and github, you may download the main LaTeX files and work on your particular file in isolation, then email your completed file to the technical dictator (or anyone else who is agreeable) to be pushed to the repository. Please don’t do this overly frequently. (-:

Organizational issues

• Mike Shulman is the technical dictator.
• Peter Aczel is the logical dictator.
• Goal to finish first draft by December 7th
• Tuesday meetings 1:30 for discussion of status, progress, and problems

How to contribute

1. Volunteer to write or co-write a chapter or a section.
2. Be a reviewer of drafts. If you are interested in reviewing a particular chapter or section, contact its author. Completed drafts should also be announced on the mailing list so that anyone who is interested can review them.
3. Add small things like exercises.

Issues

• We will use LaTeX macros for contentious notations, to avoid endless discussions of notation for now. The macros are defined in the file “macros.tex”.
• There should be a separate section at the end of each chapter containing exercises. Authors are encouraged to include exercises.
• References to the research literature, perhaps with notes, should be concentrated at the end of each section, Elephant-style.
• We should avoid using too much type-theoretic notation and terminology. Perhaps the word “induction” is preferable to “elimination”.
• The standard of rigor is that everything should be formalizable, but we do not focus on any specific issues of formalization.
• It would be nice if there were a parallel Coq development, and most of our chapters do already exist in some form in the HoTT repository or elsewhere. But this is perhaps for version 2 of the book; the focus now is on the informal version.

Preliminary contents

Each chapter is listed along with its coordinating author(s), who will be writing some of its sections but not necessarily all.

1. Introduction to type theory - open
   1. Summary of type theory (from HoTT perspective, from Propositions-as-Types)
2. Basics of HoTT - Mike Shulman
   1. Basic properties of equality
   2. Summary of some basic HoTT definitions
   3. Dependent types, sums, products
   4. Paths and path induction
   5. Transport and map on paths
   6. Introduction to equivalences - open
   7. Function extensionality
   8. Interaction of paths with type constructors
3. Equivalences - Mike Shulman
   1. Equivalences and homotopies
   2. Bijections and isomorphisms
   3. Adjoint isomorphisms
   4. Identity systems on a type universe
4. Induction in general - Kristina Sojakova
   1. Booleans and natural numbers
   2. Disjoint unions and dependent sums
   3. W-types
   4. Identity types
5. H-levels - Benedikt Ahrens, Chris Kapulkin
   1. Definition and first properties
   2. Preservation under constructors
   3. Propositions and sets
   4. The h-level of the type of types with h-level n
6. Higher-inductive types - Guillaume Brunerie, Peter Lumsdaine
   1. The interval
   2. The flattening lemma
   3. Spheres
   4. Truncations
   5. The interval (+ implies FE)
   6. Suspensions
   7. Quotients
   8. Reduction of HITs to 1-HITS
   9. (general theory)
7. Homotopy theory - Guillaume Brunerie
   1. Homotopy pushouts
   2. Homotopy pullbacks
   3. Reflective subuniverses of Type
   4. Truncations
   5. Connectedness of suspensions
   6. Homotopy groups
8. Univalence - Peter Aczel
   1. Introduction
   2. The notion of a univalent universe
   3. Two more equivalence relations between types
   4. Function extensionality in a univalent universe
   5. First proof of the theorem
   6. Appendix: another proof of the theorem
   7. Other formulations (EQ-induction)
   8. Consequences of univalence
9. Programming in HoTT (?)
10. Category theory - Mike Shulman
    1. lots of subsections
11. Set-level mathematics - Andrej Bauer
    1. the category of sets
    2. algebra
    3. real numbers and analysis
    4. topology