@hackage / hoq

A language based on homotopy type theory with an interval type