What is "univalent" about univalent logic and foundations?

Question

This is a perhaps naive question about terminology.

I know that "a bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy)" ref.

But this does not make clear why this term was chosen here.

I also wonder whether the term has further motivation, viz bivalence in logic, or the term univalence in other fields?

I would guess a term like "multi-valent" seems more fitting, considering that:

"intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions { ⊤ , ⊥ } from classical logic, each proof of a propositional formula is considered a valid propositional value, thus by Heyting's notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs." here.

Answer 1

From nlab's article

The name univalence (due to Voevodsky) comes from the following reasoning. A fibration or bundle $p:E→B$ of some sort is commonly said to be universal if every other bundle of the same sort is a pullback of $p$ in a unique way (up to homotopy). Less commonly, a bundle is said to be versal if every other bundle is a pullback of it in some way, not necessarily unique. By contrast, a bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy). In the language of (∞,1)-category theory, a univalent bundle is an object classifier.

The univalence axiom does not literally say that anything is univalent in this sense. However, it is equivalent to saying that the canonical fibration over $\mathsf{Type}$ is univalent: every fibration with small fibers is an essentially unique pullback of this one (while those with large fibers are not, they are pullbacks of the next higher $\mathsf{Type}_1$). For a description of this equivalence, see section 4.8 of the HoTT Book (syntactically) and Gepner-Kock (semantically).

Essentially, while a category theorist could probably imagine that universes in Martin-löf type theory are 'like' object classifiers, the equality between types is too intensional for it to literally make sense. One could exhibit things as pullbacks in ways that are not provably equal (because they are merely isomorphic/equivalent, not exactly the same definition). The univalence axiom is the extensionality principle needed to make universes proper object classifiers.

Incidentally, univalence/homotopy type theory is not necessarily intuitionistic. Voevodsky's first model for type theory extended with the univalence axiom also modeled excluded middle (if my understanding is correct), and I don't think he really had any qualms about using classical axioms like that. It is just the case that many people who work with type theory, including homotopy type theory, recognize that it can be useful to not assume excluded middle/choice/etc.