What does "univalent" mean?

269 Views Asked by At

I have heard of the Univalent Axiom in the search for a foundation of mathematics, "Univalent Foundations". The univalent axiom says:

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.

That doesn't directly say what "univalent" means. What does it mean? From uni- +‎ -valent, uni meaning "one" and valent meaning something like "preparation".

If I were to introduce non-mathematicians to the Univalent Foundations of Mathematics, such as introducing software engineers to it, they would ask the question "why is it called univalent?". How could I give a satisfying answer to that question?

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types.

That makes total sense.

But why is it called "univalent"? How can we create a deeper meaning out of this word to make it make more sense? Because right now, you might as well have just called it "The Foobar Foundations of Mathematics", as the word seems to have no real meaning. Why are they saying "univalent"?