Hacker News Reader

Univalence seems generally useful for verified software engineering, if we could get it in a system with regularity.

Why more useful than non-homotopy type theory?

Is there a non-homotopy type theory with univalence?

Not more useful in practice than Dependent Types and/or Refinement Types. F* (F-Star) is a good example of this.