Skip to main content
Wikispaces Classroom is now free, social, and easier than ever.
Try it today.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
The HoTT Book is now done!
Get it here.
The book is available at the
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
(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:
Link to cheatsheet:
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. (-:
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
Volunteer to write or co-write a chapter or a section.
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.
Add small things like exercises.
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
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.
Each chapter is listed along with its coordinating author(s), who will be writing some of its sections but not necessarily all.
Introduction to type theory - open
Summary of type theory (from HoTT perspective, from Propositions-as-Types)
Basics of HoTT - Mike Shulman
Basic properties of equality
Summary of some basic HoTT definitions
Dependent types, sums, products
Paths and path induction
Transport and map on paths
Introduction to equivalences - open
Interaction of paths with type constructors
Equivalences - Mike Shulman
Equivalences and homotopies
Bijections and isomorphisms
Identity systems on a type universe
Induction in general - Kristina Sojakova
Booleans and natural numbers
Disjoint unions and dependent sums
H-levels - Benedikt Ahrens, Chris Kapulkin
Definition and first properties
Preservation under constructors
Propositions and sets
The h-level of the type of types with h-level n
Higher-inductive types - Guillaume Brunerie, Peter Lumsdaine
The flattening lemma
The interval (+ implies FE)
Reduction of HITs to 1-HITS
Homotopy theory - Guillaume Brunerie
Reflective subuniverses of Type
Connectedness of suspensions
Univalence - Peter Aczel
The notion of a univalent universe
Two more equivalence relations between types
Function extensionality in a univalent universe
First proof of the theorem
Appendix: another proof of the theorem
Other formulations (EQ-induction)
Consequences of univalence
Programming in HoTT (?)
Category theory - Mike Shulman
lots of subsections
Set-level mathematics - Andrej Bauer
the category of sets
real numbers and analysis
help on how to format text
Turn off "Getting Started"