HoTT in Idris - Small, incomplete, and inconsistent formalization of homotopy type theory in Idris.

hoq - Language based on homotopy type theory with an interval.

homotopy.io - Web-based proof assistant for finitely-presented globular n-categories, for arbitrary n. (User Guide) (Code)