As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately

As a relative layperson alongside you, I'm not sure what precise deficit Lurie is addressing. But having spent some deep time in a proof assistant (Agda) lately, I think there is a related issue. Formally, equality can be "intensional" or "extensional". An intensional theory equality says that things are the same only when they are defined the same way. So, for instance, "the set of even primes" and "the set of primes less than 3" are not intensionally the same. In contrast, an extensional theory says that things are the same when they behave the same. Both sets answer the same membership questions the same way -- 2 is the only element of either -- so they are the same set. ZFC is fundamentally extensional -- one of its axioms is literally called the axiom of extensionality, defining equality in terms of membership. In deeply identifying the above sets, we lose some of the ability to distinguish them formally and model the way in which they are equivalent. That's one guess. Another, less specific guess is that it's much like how the dual of a vector space is isomorphic to the original vector space, but in a way that depends on certain arbitrary choices. Meanwhile, the dual of the dual is naturally isomorphic to the original vector space. Thus, there are qualities of equivalence that we're interested in. (But this example is perfectly well captured by linear algebra as it stands.)