A universal property, in the sense of category theory, generally expresses that a map involving hom-sets, induced by composition with some canonical map(s), is an isomorphism. In type theory we express this using equivalences of hom-types. For instance, the universal property of the sum type says that for any , the induced map
is an equivalence.
Universal properties are very useful, but since saying that a map between function types is an equivalence requires knowing when two functions are equal, they seem to depend irreducibly on function extensionality (“funext”). Contrary to this impression, in this post I want to talk about a way to define, construct, and use universal properties that does not require function extensionality.
First, however, I should perhaps say a little bit about why one might care. Here are a few reasons:
- Maybe you just like to avoid unnecessary assumptions.
- Maybe you want to define things that compute, rather than getting stuck on the function extensionality axiom.
- Maybe you want to your terms to be free of unnecessary “funext redexes”, making them easier to reason about. Here by a “funext redex” I mean a path obtained by applying funext to a homotopy to get a path between functions, then applying that path at an argument to get a path between function values. (Following the book, by a “homotopy” I mean an element of .) Clearly we could just have applied the homotopy in the first place. Once we have a type theory in which paths in function types literally are homotopies, this won’t be a problem, but for now, it makes life easier if we can avoid introducing funext redexes in the first place.
- Finally, this is not a very good reason, but I’ll mention it since it was actually what started me looking into this in the first place: maybe you want to declare a coercion that conforms to Coq’s “uniform inheritance condition”, which means that it can’t depend on an extra hypothesis of funext.
Onwards! To begin with, as you may know, type theory already includes an excellent way to express some universal properties without funext, namely induction principles. The induction principle for sum types makes perfect sense, and importantly is usable, without funext; whereas if we assume funext then the induction principle is equivalent (modulo judgmentality of computation) to the universal property.
So why is this not good enough? Well, to prove the universal property from the induction principle for , we need to apply that induction principle not only with motive , but also with motive being a type of homotopies between functions into . That’s not a problem here, but in some situations, we may want to express a universal property that doesn’t apply to all type families, so that we can’t assert a general induction principle.
A prime example is the notion of reflective subuniverse. As stated in the book, it involves an equivalence of hom-types: there is a reflector and maps such that for any type in the subuniverse, the induced map is an equivalence. Like any universal property, this is unprovable and unusable without funext. However, it’s tricky to state an induction principle for : if we did the obvious thing and ask it to induct into all families of types in the subuniverse, we would get not a reflective subuniverse but the stronger notion of a modality.
Another, closely related, example is the notion of local type. Given a map , a type is called -local if the induced map is an equivalence. Again, this is unprovable and unusable without funext, but because we’re only talking about a property of a particular type , we can’t express it as an induction principle.
In considering whether there is any way around this, our first thought might be to take the definition of equivalence, applied to a map such as or , and replace all the occurrences of paths in function types by homotopies. This certainly gives a notion that is equivalent to the original if we have funext, and which at least doesn’t appear to require funext. However, it seems that in order to actually avoid funext, we have to be quite careful in choosing one out of the many definitions of “equivalence”.
To get an idea of where the problem lies, suppose we assert that is an “equivalence” in the following sense: for every there is a , such that , and for any we have (plus, of course, a coherence). Now, one of the things we’d like to know, which certainly ought to follow from being an “equivalence”, is that if become the same upon precomposition with , they should already be the same. We are doing without funext, so “the same” should mean a homotopy, i.e. we would like to imply . We naturally want to write
but there is a problem, namely that the “rec” operation need not preserve homotopies. It preserves equalities (paths), of course, since everything does, but without funext, we can’t make a homotopy into an equality.
The same problems arise with most of the other definitions of equivalence, but it turns out that there is one of them that works (after a bit of modification). This definition is not one of the better-known ones (in fact, I don’t think it appears in the book at all): a map is an equivalence if and only if (1) is split surjective, i.e. there is a such that , and (2) for all , the induced map is also split surjective. Moreover, this is even a good definition of equivalence, i.e. if we assume funext then it is an hprop. (There is, I believe, no hope of any definition of equivalence being an hprop without funext, since any notion of equivalence will involve functions as part of its data.) Proving this is a nice exercise.
This definition is kind of cute because it is a direct enhancement of the propositions-as-types translation of “ is surjective and injective”. The PAT notion of “surjective” is split surjectivity, while the ordinary PAT notion of “injective” would say that for all we have ; we simply add the assumption that the latter map is a section of . (I don’t remember who first pointed this definition out to me.)
Let’s take this definition and funext-reduce it in the case of a precomposition map . Split surjectivity, with paths made into homotopies, says that for any there is a , such that . This is exactly what we had before: maps extend along . However, making paths into homotopies in the second clause says that given and a homotopy , we have a homotopy such that . Thus, it exactly solves the problem we saw before!
We are not quite golden yet, however. What if we want to extend this to higher homotopies? That is, suppose we have two homotopies and a 2-homotopy ; can we conclude that ? This definition seems insufficient to show that without funext. Since we are assuming directly that functions and homotopies extend, maybe we need to assume directly that all higher homotopies extend as well. But is that possible?
Looking back at our chosen definition of equivalence, we are struck by the fact that it treats paths and points in an entirely analogous way. Moreover, clauses (1) and (2) are completely independent; neither depends on the other! Therefore, it admits a very simple recursive extension to all higher paths. We define what it means for a map to be n-path-split by recursion on n as follows:
- Every map is (uniquely) 0-path-split.
- is -path-split if (1) it is split surjective, and (2) for all , the induced map is -path-split.
Thus, our previous notion of equivalence is what we now call “2-path-split”. It’s not hard to show by induction that (assuming funext) “n-path-split” is a good notion of equivalence whenever . Moreover, we can put them all together: say that is ∞-path-split if it is n-path-split for all n. This is also a good notion of equivalence (since by funext, the dependent product of hprops is an hprop).
The notions of n-path-split as n goes to infinity are closely related to the higher notions of coherent adjoint equivalence. We expect, from homotopy theory, that if instead of cutting off the definition of half-adjoint equivalence after one 2-path coherence, we added also the second 2-coherence and one 3-coherence, or both 2- and 3-coherences and a 4-coherence, etc., we would get good notions of equivalence. At each step we add two new data; if we added only one, we would no longer have a good notion. The tower of path-splitness is entirely analogous, but easier to express and work with internally, because the two new data we add at each step don’t depend on the data added at any previous step; they depend only on the original map .
If we now funext-reduce ∞-path-splitness in the case of a precomposition map, we get a notion of universal property, expressed completely in terms of homotopies, that can deal with all higher homotopies as well. Given , we define what it means for a type family to be n-extendable along :
- Every is (uniquely) 0-extendable along .
- is -extendable along if (1) for every we have a such that , and (2) for all , the family is -extendable.
Similarly, we have ∞-extendable families. We can now express an equivalence such as by saying that the constant family is ∞-extendable along . Note that we’ve come almost full circle: this is very close to the induction principles we began with, except that we’re only allowing “induction” into families of a very special recursively defined sort.
If we assume funext, then ∞-extendability is equivalent to saying that is ∞-path-split, and hence to saying that it’s an equivalence. However, both directions of the equivalence between ∞-extendability and ∞-path-splitness require funext, and in the absence of funext, ∞-extendability seems to be more useful.
I’ve formalized reflective subuniverses in Coq using this definition of the universal property, and the theory turns out to be entirely free of funext. I don’t have a proof that funext is never needed, but the evidence so far is clear.
To end with, let me say something about localization. Recall from above that given , we define a type to be -local if is an equivalence. Since this is a precomposition map, we can ask instead that it is ∞-extendable, to get a notion of “-local” that’s usable without funext. Now the localization of an arbitrary type is supposed to be its reflection into -local types, i.e. an -local type with a map such that for any -local , we have an equivalence .
We’ve known for a long time that can be constructed as a HIT. Simply take a definition of equivalence, funext reduce it, and make it into constructors of . The easiest one to do this with is “bi-invertibility” (having both a section and a retraction), since it doesn’t involve higher paths; we get
Inductive : Type :=
| to_local :
| local_e1 :
| local_s1 : , local_e1 g (f s) = g s
| local_e2 :
| local_r2 : , local_e2 (h f) t = h t.
However, the proof that is -local and has the right universal property has always required funext. But now, with ∞-extendable maps, we can avoid this: instead of the latter four constructors above, we instead add a constructor asserting that the constant family is ∞-extendable along .
This is admittedly a different kind of constructor than we usually see for HITs; it’s parametrized over natural numbers and it has a different “shape” for each natural number. But there seems to be no problem formulating the induction principle and working with it. And semantically, we should be able to replace this constructor by an infinite number of more ordinary ones and then apply the usual methods.
In particular, note that this constructor inserts paths of all dimensions. Have we seen a HIT like that before? I don’t remember for sure, but I can’t think of any right now.
Postscript: Everything in this post has been formalized in the HoTT Coq library. Here is the pull request.