Home

Welcome to the Wiki for the HoTT/Coq-HoTT library!

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

Documentation

Reference manual

We have various bits of browsable documentation for the HoTT library:

• A reference manual autogenerated by coqdoc.

  • Coqdoc - Table of Contents
  • Coqdoc - Index - Warning: This page is very large.

• 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. You can also step through the proofs as if interacting with Coq.

  • Alectryon - Table of Contents
  • Alectryon - Index - Warning: This page is very large.

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

  • Proviola - Table of Contents
  • Proviola - Index - Warning: This page is very large.

• An interactive view of the timing information for each line in each file.

  Autogenerated by a script adapted from Microsoft Research's SSReflect library. Hovering over a line will display the time taken for the command to run as a tooltip.

  • Timing - Table of Contents

The HoTT Book

We have an index linking various theorems and definitions from the HoTT Book to the HoTT library.

• Index for the HoTT Book - autogenerated by Alectryon.
• Index for the HoTT Book - autogenerated by Proviola.
• Index for the HoTT Book - autogenerated by Coqdoc.

We also have solutions to some exercises from the HoTT Book:

• HoTT Book Exercises - autogenerated by Alectryon.
• HoTT Book Exercises - autogenerated by Proviola.
• HoTT Book Exercises - autogenerated by Coqdoc.

Dependency graphs

We autogenerate dependency graphs using the dpdgraph tool of Anne Pacalet and Yves Bertot. This allows us to create the following images using GraphViz, borrowing a script from MathClasses.

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

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

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

JsHoTT - Run the HoTT library in Javascript!

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

Coq-bench

HoTT is routinely benched in Coq-bench. See:

• Our Coq version 8.15 bench.
• Our Coq version dev bench.