Skip to content
This repository has been archived by the owner on Apr 21, 2018. It is now read-only.

Latest commit

 

History

History
6 lines (5 loc) · 670 Bytes

README.md

File metadata and controls

6 lines (5 loc) · 670 Bytes
Raw

I ended up having trouble using the bundled and canonical structure based algebraic hierarchy of this project, so I ported some of MathClasses's unbundled and typeclass based to HoTT in HoTTClasses. You should probably use that.

The following projects also have some form of Homotopy Type Theory and algebra:

  • UniMath (not based on HoTT, not higher inductive types).
  • Lean2 (alternative theorem prover to Coq).
  • possibly others, especially since I don't plan to update this README.