Hacker News Reader

Comment by auggierose | Hacker News Reader

I really wish somebody could explain the Univalence axiom to me. Without assuming that I know category theory or algebraic topology. You know, just like you can explain the axioms of set theory pretty easily. I mean, if it is a foundation, there should be an easy way to explain it. And not in metaphors, please, but in a precise way.

View on HN

At a very high level the univalence axiom says that set operations may not look at the elements of a set. Consider the cartesian product versus set union. The cartesian product does not look at the elements of the sets, but the union does. If A and B share an element then this element will appear only once in A union B, so the number of elements in the union depends on the actual elements in A and B. In contrast, the number of elements in A x B only depends on the number of elements in A and B. The cartesian product does not care about the internals of elements themselves. With infinite sets it's not clear what number of elements means. Mathematicians say that the number of elements in A and B is the same if there is a way to pair each element in A with an unique element in B. The condition that set operations don't depend on the elements in the set can then be expressed as follows. If there is a pairing of elements between A and A' and between B and B' then there is a pairing between op(A,B) and op(A',B'). The univalence axiom basically says that all set operations in HoTT are of this type.

To connect with the conventional terminology: we call A and A' equivalent if there exists such a pairing. Equality is the relation that all operations must respect: if A = A' and B = B' then op(A,B) = op(A',B'). The univalence axiom says that equality of sets is equivalence of sets.

Given an equivalence between (all the values of) two types, you can assume the types are equal, i.e. substitute one for the other in any value, no matter how complex (including functions on values/types etc.).

The value/function conversion is called a "transport" and it actually depends on which equality you've chosen (called "paths" in HoTT).

E.g. bool <-> bit can map false => 0, true => 1 or false => 1, true => 0.

So `(a: bool, b: bool) => a && b` can be "transported" to `(a: bit, b: bit) => a & b` or to `(a: bit, b: bit) => !(!a & !b)` (which is `a | b`).

Of course, bit tricks aren't that useful, but two types which are defined differently (e.g. from different libraries, or different versions of the same library), yet contain the same information, would be interchangeable given a "path" (in the case of the Univalence Axiom, a proof of equivalence).

The other important addition in HoTT is defining non-trivial "paths" (equalities) between values of a type when you define the type - this is used in the HoTT book to describe integer, rational and real numbers, in a way reminiscent of quotient sets.

I doubt that it can be explained in less than fifteen pages.

https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf

Well, it is a start. Fourteen pages anyone? Once we are down to five pages I'll give it a(nother) shot.

In example 2.2, to distinguish between an element and a function a better example is to consider a constant such as 7 can be an element of R or a constant function. With type theory notation, 1:R versus \x:R.1, another important point is that you have to specify the arity of the function, so that 1:R, \(x:R).1, \(x:R,y:R).1, \(x:C,y:C).1 are four different types, the first a constant, the second a constant function of one real variable, and the last a function of arity two whose variable type is the C the complex field.

I'm reading page four, perhaps type theory can distinguish among pure function, lazy functions, side-effect functions and other types of functions that are implemented by a procedure which can be lazy or not. So pi:R,(\x:R.pi) and (\x:Haskell-Action()).pi in which the last is a non pure lazy program for computing all digits of pi, are two different types, that is they belong to different universes.

you should read it, it's an easy one, at least it's how I feel after reading 3 pages (usually I stop long before that)

It's not bad, but man the way the author throws around multivariate (e.g. non-curried) functions all over the place is sooo confusing. I remember reading a λ-calculus book that would do that and it's really not fun to try and parse (see the bottom of pg. 7).

But I will say it's very cool to see how HoTT derives all the basic tools you'd use in propositional calculus (A: A -> A, :(A -> (B -> C)) -> ((A->B) -> (A->C)), and so on).

An isomorphism is a structural correspondence between two objects. In HoTT a type's structure is its points, paths between points, paths between paths... etc. Note that "path" is an abstract idea: it's a construction parameterized on two points that is reflexive, symmetric, and transitive.

Now, the whole universe of types itself has a path structure.

Univalence says that isomorphisms of types are the same as paths between types.

In a way it bridges the gap between structural isomorphism and Leibniz equality.

The bird's eye overview of the univalence axiom is as follows.

In homotopy type theory, we have in addition to familiar types like the type of natural numbers or the type of lists of strings the "universe type U". Its inhabitants are the types themselves.

Just as we write "5 : Int", we can also write "Int : U".

The univalence axiom specifies when two inhabitants of U should be deemed equal. The remaining axioms of type theory don't settle this question.

Can you write "U : _"? If so, what fills in the blank? It seems to parallel "Value :: Type", "Type :: Kind", and "Kind :: Sort" from FP.

Indeed, homotopy type theory employs a stratified approach to this question.

That is, what I've written "U" would more formally be written "U_0". We then have U_0 : U_1, U_1 : U_2, and so on. All the base types are inhabitans of U_0, that is we have Int : U_0, String : U_0, and so on.

In functional programming parlance, we'd have U_0 = Type, U_1 = Kind, U_2 = Sort.

There's a thing called "typical ambiguity" which allows us to drop the index in most cases (and let it be automatically inferred).

Thanks. HTT sounds interesting. I'll have to investigate further.

Reply on news.ycombinator.com