Arend is a proof assistant based on homotopy type theory. It natively supports higher inductive types and a version of cubical syntax.