Post #1846793

@zwarich Related to #1,#3, Lurie is working extremely informally, but there are other people doing higher category theory from the univalent point of view in ways that are more formal and also non-type-theoretic. So I don't think that univalence needs MLTT; the univalence axiom is usually phrased in MLTT, but it can also be expressed as the universal property of the object classifier and this makes sense even in a simply typed system.