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.