3 ms·

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

• orangea 4y ago
  Why more useful than non-homotopy type theory?
  • remexre 4y ago
    Is there a non-homotopy type theory with univalence?
• jnash 4y ago
  Not more useful in practice than Dependent Types and/or Refinement Types. F* (F-Star) is a good example of this.