Home

Welcome to the wiki for the HoTT/HoTT library!

Important and helpful information for anyone using or contributing to the library can be found in the STYLE file in the repository.

A reference manual autogenerated by coqdoc. (index) (table of contents)

An interactive reference manual autogenerated by Alectryon; hovering over a line of code will display the feedback given by Coq at that point in the code. (index) (table of contents)

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. (index) (table of contents)

Coq can also be run in your browser with JsCoq/JsHoTT.

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 Alectryon.

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.

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.

HoTT in the Coq bench marking tool.