Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory.
Can anyone tell me, in functional programming terms or through practical examples, how exactly is HoTT going to change the way we view mathematics, and what are the implications of HoTT on proof assistants? Thanks!
I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior version. Lots of attempts have been made previously to add extensionality features to type theory that have been missing relative to e.g. set theory, but they often have some kind of caveat to them that is kind of unsatisfying. One might say that HoTT solves these issues because the mathematics is appropriate for a proper computational interpretation of what equality is, and trying to follow orthodox mathematical practice was part of the problem with previous approaches.
So, what is the difference? Traditionally people think of equality as being like an intrinsic property. Two things are equal when they "are actually the same" or something. This shows up in approaches to equality wanting to make it computationally irrelevant. There's nothing interesting about a proof that two things are equal, because they just are equal, and the proof has nothing to record.
However, this is not how intensional Martin-löf type theory works, actually. Values of identity type are computationally relevant, and the eliminator only reduces when the value computes to refl. So in some sense, it leaves open the possibility that we can have non-trivial proofs that say how two things are equal, not just that they are equal. It just happens that there are no basic ways in the usual presentation to say how two things are eqal other than 'they just are.' In some ways, induction already introduces at least open terms of identity type that do not behave exactly like the 'these two things just are equal' term (refl). HoTT just wishes to add new closed terms (hence the difficulty with computational behavior).
In some ways, this notion of non-trivial ways of how two things are considered equal is no surprise computationally. In type theory we often consider two things 'actually the same' when they really aren't. $λx.x$ is the same as $λy.y$ when we are using the α rule, but they are clearly not exactly the same symbol strings. And we have different collections of rules we may use at any given time to determine which symbol strings we consider 'actually the same;' α vs. α-β vs. α-β-η. So it is clear that 'actually the same' is a fictional idea, not reality.
The thing that most easily allows us to pretend that these technically distinct things are actually the same is decidability. It's easy to test whether two lambda terms are α equivalent, so we don't really need to keep track of how they are α equivalent, since we can just test them whenever necessary. Of course, we also need to not be able to tell the difference between α equivalent things anywhere. But then we can just say that α equivalent things are equal via 'they just are.'
But, this doesn't work for extensional equality of things like functions or quotients. It may not be possible to automatically decide that two values of type T are related by relation R for the purpose of introducing equality in T/R. In set theory, this is explained by saying that values of T/R are 'equivalence classes' of T, but this is not really a sensible explanation computationally, because it may not be possible to compute that equivalence class.
Older approaches to adding quotients to type theory generally involve allowing you to prove equality explicitly via R, but then maintaining the fiction by throwing away the proof, and making sure no one can ever really ask for it. The HoTT approach is to not throw it away. There are actual values of the identity type that contain witnesses of R. When we define functions from T/R, we give values for inclusions from T, say |x| and |y|. And if r : R x y, we also give a case that receives r, explaining how |x| and |y| are related, so that we can use it to explain how to mediate between their images.
This essentially eliminates careful engineering necessary to avoid undecidable problems for these sorts of constructs, because we aren't just discarding the provided evidence. These content-ful mediations also give richer ways for constructions to 'respect' the equalities of other things, which is useful. The type theories that make all this work have pretty complex engineering of their own, but in a way it seems satisfying to take seriously the idea of computing explanations for how things may be interchanged, rather than merely ensuring that no one will care if they are interchanged.
A last aspect, and the genuine "homotopy" one arguably, is that it makes sense to consider two things to be equal in actually distinct ways. In fact, it makes sense to consider an actual single thing equal to itself in distinct ways. This shows up readily in extensional equality of types. Traditional equality of types is very intensional; only types defined the same way are equal. But, as long as we have invertible mappings between two types, we could imagine translating things written for one to the other. This is what univalence allows, making types with invertible mappings between them equal.
But, for instance, there are two distinct invertible mappings from Bool to itself: the identity function and not. So, even though every construction respects these mappings, and we are able to consider them equalities mediating from Bool to itself, they are themselves distinct. This suggests a couple things.
The essential feature of equality is preservation by all constructions, not that things are exactly the same in exactly one way.
It might be interesting to consider other proofs that things are equal to not necessarily be 'the same' proof as every other. For instance, perhaps the multiple ways of β reducing terms with multiple redexes might not be considered exactly the same proof. Of course, if we do want to consider them the same, HoTT also tells us that we can do so by having a non-trivial mediation between different reductions that explains how to reorder the individual reductions (say).
I think it's also reasonable to take the position that these should genuinely be called something different, like "path", while "equality" is reserved for situations where there are mediations 'all the way up', possibly becominge genuinely trivial above some level (although that isn't necessary). But this is a novel and potentially very useful notion of extensionality for types/the universe that was not (to my knowledge) being considered in type theory prior to HoTT.
Definitions that allow you to create types that work this way by fiat (like HITs, mentioned in the other answer) also seem potentially very interesting for programming. For instance, one could define the lambda terms with distinct proofs of β equivalence, although I'm unsure what exactly one would do with them.
I won't lie: I don't understand the homotopy part of homotopy type theory. But I have a decent grasp of Univalence, which is the axiom at the heart of Homotopy Type Theory (HoTT).
The main idea of univalence is that we treat equivalences (essentially, isomorphisms) as equalities. When two types are isomorphic, you have a way to get from one to the other and back, and the round-trip is the identity in both directions. But there's no way to lift properties between isomorphic types: if you have a proof that 2 is the only even prime for unary natural numbers, you can't automatically lift the proof of that property to binary natural numbers, even though you can convert 2 back and forth between the formats.
The eliminator for equality (sometimes also called the $J$ axiom) allows you to lift any property between equal things. So if we have an equality for every isomorphism, then we could transport the above property from unary to binary numbers. This is what univalence gives us: an axiomatic way to lift properties over isomorphisms.
The main implications of this are:
There are also some cool things you can do with univalence. You can define Higher Inductive Types (HITs), where in addition to giving data constructors for inductive types, you give path constructors, which are equalities that must hold. When you pattern match, you then have to show that you preserve these equalities.
HITs allow you to do things like "define integers as a natural plus a sign but, but ensure that positive and negative 0 are truly equal.
However, there are some strange consequences to univalence. First, it means that we cannot have $Refl : x \equiv x$ as the sole way to construct an equality proof, because univalence lets us construct equalities between things that are definitely not syntactically identical. This means that univalence is incompatible with "Uniqueness of identity proofs" and axiom $K$. In practice, this means that the rules of dependent pattern matching must be weakened to be consistent with univalence. Jesper Cockx has a whole line of research on how to do this well.
The other problem is that we lose "canonicity" i.e. the idea that every term can be fully evaluated to a value in canonical form. For equality, Refl is the only canonical proof of equality. So this means that when running programs, sometimes we get "stuck" on the use of univalence as an axiom. This makes sense: we basically said "pretend I have a function that transforms isomorphisms into equalities". We never gave that function, so if we try to evaluate code that calls it, we'll get stuck.
The main effort to solve this problem is Cubical Type Theory. Cubical models equality in such a way that canonicity is preserved, but univalence can be proved as a theorem in the language. So univalence is now not an axiom, it's an actual function that can be applied.
If you're interested in this more, there are two main resources I'm familiar with. The HoTT Book is the canonical reference. There's also Univalent Foundations in Agda, which is less focused on the homotopy theory, and more on the implications that univalence has for logic. I'm sure there are also more books I'm not familiar with. The Cubical Agda paper is also good.
