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

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.


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
Created on April 19, 2018 at 21:16:58 by Univalent foundations special year 2012