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