A textbook on informal homotopy type theory -- Vladimir's fork, retained because there is a pull request based on it.
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is 2 commits ahead, 340 commits behind HoTT:master.
Permalink
Failed to load latest commit information.
coq_introduction Updated Reading_HoTT_in_Coq for Coq 8.4pl3 Dec 30, 2013
cover/torus Fix file permissions Jun 27, 2013
etc/ci Retry wget resolution when downloading fails Apr 16, 2014
other index-helper: exclude \indexdefs containing backslashes May 24, 2013
.gitattributes Try to prevent line ending problems Apr 13, 2013
.gitignore Add *.out.pdf to .gitignore Apr 17, 2014
.travis.yml Package 'mh' no longer exists, so get 'mathtools' for travis instead Sep 21, 2014
CONTRIBUTING.md re-fix some grammar Sep 21, 2014
CONVENTIONS.txt Specified which characters are ok in labels Mar 7, 2013
GIT_CHEATSHEET.txt Changed instructions that tell people to use `git add --all`, Apr 27, 2013
Makefile Add dvimode, remove pagecolor package Apr 16, 2014
README.md Changed version.txt to version.tex (twice) Dec 25, 2014
back.tex omit header on blank versos, fix HoTT#269 Jun 17, 2013
basics.tex Update basics.tex Feb 17, 2015
blurb.tex justify back cover Jun 19, 2013
bmpsize-hack.tex Add dvimode, remove pagecolor package Apr 16, 2014
categories.tex added erratum for hom-typo in categories Oct 29, 2014
cleveref.sty Update cleveref from 0.17.9 to 0.19 Mar 28, 2014
cover-a4.tex Add dvimode, remove pagecolor package Apr 16, 2014
cover-hires-back-bw.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-back.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-bw.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-front-bw.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-front.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires.png Blue Steve with dark gray torus Jun 4, 2013
cover-letter.tex Add dvimode, remove pagecolor package Apr 16, 2014
cover-lores-back-bw.png Reduce size of low resolution images Jun 19, 2013
cover-lores-back.png Reduce size of low resolution images Jun 19, 2013
cover-lores-front-bw.png Reduce size of low resolution images Jun 19, 2013
cover-lores-front.png Reduce size of low resolution images Jun 19, 2013
cover-lores.png Reduce size of low resolution images Jun 19, 2013
cover-lulu-hardcover.png Remove alpha channel from Lulu cover images Jun 18, 2014
cover-lulu-hardcover.tex Remove transparency from lulu.com covers Jun 4, 2014
cover-lulu-paperback.png Remove alpha channel from Lulu cover images Jun 18, 2014
cover-lulu-paperback.tex Remove transparency from lulu.com covers Jun 4, 2014
equivalences.tex Update equivalences.tex Feb 17, 2015
errata.tex Mark Errata (auto) Jan 2, 2015
exercise_solutions.tex another fix for exercise_solutions.tex, I haven't checked whether it … Oct 14, 2014
filter-errata rename filtered-errata files to not clash with those posted on the we… Aug 5, 2013
formal.tex Last rule of Section A.2.2, lines 591 and 592 Dec 19, 2014
front.tex Made the visible URL's fixed-width Dec 31, 2014
frontpage.tex white letters on gray-blue Jun 4, 2013
geometry.sty Added geometry.sty and ifxetex.sty. Mar 8, 2013
halpha.bst replace natbib by halpha, close HoTT#220 May 21, 2013
hits.tex P in the flattening lemma is defined *recursively*, not inductively Jan 5, 2015
hlevels.tex Fix a couple of issues with Lemma 7.5.12 Oct 21, 2014
homotopy.tex Replace `\autoref` with `\cref` throughout. Apr 16, 2014
hott-a4.tex A4 version Jun 20, 2013
hott-ebook.tex changed "resultion" to "resolution" on line 3 Dec 17, 2014
hott-letter.tex Bastard title, fix ebook format. Jun 17, 2013
hott-online.tex Bastard title, fix ebook format. Jun 17, 2013
hott-ustrade.tex Bastard title, fix ebook format. Jun 17, 2013
ifxetex.sty Added geometry.sty and ifxetex.sty. Mar 8, 2013
induction.tex Fixed several tiny (non-mathematical) typos Dec 24, 2014
introduction.tex A better version of one of the paragraphs in the introduction written Feb 28, 2015
logic.tex Fixed several tiny (non-mathematical) typos Dec 24, 2014
macros.tex introduced macro for uniq Oct 14, 2014
main.labelnumbers.first-edition A script to automatically check whether label numbers have changed Jul 3, 2013
main.tex Add dvimode, remove pagecolor package Apr 16, 2014
mark-errata Make the errata marker work after merges Nov 27, 2013
mathpartir.sty Misspellings run Jun 21, 2013
opt-a4.tex fix ebook-overfulls Nov 22, 2013
opt-bastard.tex Bastard title, fix ebook format. Jun 17, 2013
opt-black-white.tex Tweaks to allow latex (and not only pdflatex) to compile the book Apr 14, 2014
opt-color.tex Tweaks to allow latex (and not only pdflatex) to compile the book Apr 14, 2014
opt-cover.tex New and shiny cover Jun 4, 2013
opt-ebook.tex fix ebook-overfulls Nov 22, 2013
opt-letter.tex fix ebook-overfulls Nov 22, 2013
opt-no-bastard.tex Bastard title, fix ebook format. Jun 17, 2013
opt-no-cover.tex New and shiny cover Jun 4, 2013
opt-ustrade.tex fix ebook-overfulls Nov 22, 2013
preface.tex "univalent foundations" is not capitalized Jun 10, 2013
preliminaries.tex Merge pull request HoTT#728 from mikeshulman/punctured-disc Jan 5, 2015
reals.tex corrections as per PR comments in issue HoTT#751 Dec 25, 2014
references.bib restored original bracketing, as per discussion the pull request Dec 25, 2014
setmath.tex fix an ambiguous sentence Sep 22, 2014
symbols.tex also removed uniqueness for dependent pair types from symbol list Oct 14, 2014
torus-hires-bw.png Half-title page, variable quality of images. Jun 5, 2013
torus-lores-bw.png Reduce size of low resolution images Jun 19, 2013

README.md

This is a textbook that we are writing on informal homotopy type theory. It is part of the Univalent foundations of mathematics project that took place at the Institute for Advanced Study in 2012/13.

License

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License.

Prerequisites and compilation

To compile the book you need a fairly new version of LaTeX. Texlive 2012 is confirmed to work. You might need to install some packages, see main.tex for packages that are used by the book.

BasicTeX, which is a minimalistic version of MacTeX is confirmed to work once the following packages have been installed: tlmgr, install, braket, comment, courier, enumitem, helvetic, mathpazo, nextpage, ntheorem, palatino, rsfs, stmaryrd, symbol, titlesec, wallpaper, wasy, wasysym, xstring, zapfding.

You also need the make utility. The book is a fairly complex piece of LaTeX code. Also, the file version.tex is generated on the fly, so you will need the make utility with which you can compile the main files, as follows:

  • make hott-online.pdf -- the book appropriate for online reading, with colors and green links
  • make hott-ebook.pdf -- the book with small margins, suitable for ebook readers
  • make hott-letter.pdf hott-cover.pdf -- the book in black & white, letter paper format, for printing at home, as well as a color cover (just two pages)
  • make hott-a4.pdf hott-a4.pdf -- the book in black & white, A4 paper format, for printing at home, as well as a color cover (just two pages)
  • make hott-ustrade.pdf cover-lulu-hardcover.pdf cover-lulu-paperback.pdf -- the book in US Trade format, without cover, used for the bound copy available at http://lulu.com/
  • make exercise_solutions.pdf -- compile (some) solutions to exercises

If you do not have make (for example, because you are on MacOS and you did not install the XCode command-line utilities), you can still fake it as follows. Create the file version.tex and put in it (where "Joe Hacker" should be replaced with your name):

\newcommand{\OPTversion}{Joe-Hacker-version}

Then use whatever tools you normally do to compile LaTeX. The main LaTeX files are called hott-XXX.tex. But you really should have make, you know.

Once make is run so that version.tex gets generated, you need not run make again. You can just perform the usual LaTeX cycle from your favorite editor.