Home

Welcome to the wiki for the HoTT/HoTT library!

Information for anyone using the library.

A reference manual autogenerated by coqdoc.

An interactive reference manual autogenerated by proviola; hovering over a line of code will display the feedback given by Coq at that point in the code.

An index for the HoTT library based on the HoTT book (in order of appearance in the book), autogenerated by coqdoc.

An interactive index for the HoTT library based on the HoTT book, autogenerated by proviola.

A table of contents for the HoTT library which includes timing information for the lines in each file, autogenerated by a script adapted from Microsoft Research's SSReflect library.

Solutions to some exercises from the HoTT book, autogenerated by proviola.

Information for contributing to the library.

Hyperlinked dependency graph of the core library, created using GraphViz, borrowing a script from MathClasses (click to enlarge):

Hyperlinked dependency graph of the entire library (click to enlarge):

Dependency graphs of theorems in files, created by the dpdgraph tool of Anne Pacalet and Yves Bertot.