|
Well, it's saying more than that. It states that the notions of 'equivalence' and 'isomorphism' are basically the same thing in this new language (NB: I'm not really a mathematician). Equality is already a very overloaded term in mathematics, but roughly means "these are the same thing" - X^2 is 'equal to' X * X for example, or in most cases we think simply of the identity relation on some set or whatever. Isomorphism states that two things can be 'transformed' into each other through the existence of a function, along with its inverse. For example, the sets {A, B, C} and {1, 2, 3} are not equal, but isomorphic because you can define a bijection between them: A = 1, B = 2, C = 3. In some sense equality is 'more rigid' than an isomorphism, obviously. Also, you have to choose the bijection explicitly here because in this case, more than 1 valid one exists, which is another aspect of an isomorphisms 'identity'. The univalence axiom states that in this new constructive mathematical framework, 'equality' and 'isomorphism' are exactly the same thing. I suppose in some sense you can view concepts like "object identity" and "object state" in some languages like Java in the same bucket, because while two Java objects may be "equal in terms of state" (members all the same) they might not be "equal in terms of identity" (because they point to different heap objects). But this kind of distinction mostly doesn't make sense in functional programming languages because you often throw the notion of 'value identity' out the window, so 'equality' in these languages is defined solely as mathematical equality - that we can 'normalize' two expressions to the same final form. 'isomorphism' then, normally just has an interpretation like two functions `a -> b` and its inverse `b -> a`, so even in these languages, we aren't quite talking about the same things. HoTT is much more radical than all of this when you look at it together of course - because it's more like saying if you have two proofs that x = y, you can think of 'x' and 'y' as points in space, and proof of equality is a path from x to y in this space - so two proofs of equality are just two distinct paths. The 'space' on which these points exist is actually not sets but 'types', which is like a set, but also including propositions too. So now the set 'X' and propositions about X exist together. Proving some proposition requires 'constructing' a value of that propositions' type, using the elements and propositions already existing. In a language like Haskell, to implement a function of type 'f :: A -> B' requires being able to 'construct' a B given a value of type A - to do this, in effect, is a proof that 'A -> B' does in fact exist, because you built it. Also, under this interpretation of 'space', which is topological, equivalent paths give rise to notions of 'homotopy' (saying a path A can be 'morphed into' a path B), so if you have two 'paths' representing the proofs of x = y, these 'paths' admit a homotopy between them. And furthermore you can have notions of homotopies between homotopies, etc etc. So things get very 'higher order'. Types can also be viewed as an 'infinity groupoid', which is a thing that not only has elements and isomorphisms between elements, but isomorphisms between isomorphisms, and isomorphisms between those, infinitely. So if you squint you can see how this infinity-groupoid notion of 'higher order' isomorphisms between other isomorphisms, and higher order homotopies, are all very closely linked. It's all very strange and unifying and delightful. That's the extremely handwavy explanation that is might be pretty fluffy, but it might help. |
"When is one thing equal to some other thing", by Mazur