3

Universal properties without function extensionality

 3 years ago
source link: https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

Universal properties without function extensionality

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 A+B says that for any X, the induced map

(A+B \to X) \to (A\to X)\times (B\to X)

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:

  1. Maybe you just like to avoid unnecessary assumptions.
  2. Maybe you want to define things that compute, rather than getting stuck on the function extensionality axiom.
  3. 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” f\sim g I mean an element of \prod_{x:A} (f x = g x).) 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.
  4. 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 (A+B \to X) \to (A\to X)\times (B\to X) from the induction principle for A+B, we need to apply that induction principle not only with motive X, but also with motive being a type of homotopies between functions into X. 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 \bigcirc and maps A\to \bigcirc A such that for any type B in the subuniverse, the induced map (\bigcirc A \to B) \to (A\to B) is an equivalence. Like any universal property, this is unprovable and unusable without funext. However, it’s tricky to state an induction principle for \bigcirc A: 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 f:S\to T, a type X is called f-local if the induced map (T\to X) \to (S\to X) is an equivalence. Again, this is unprovable and unusable without funext, but because we’re only talking about a property of a particular type X, 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 (\bigcirc A \to B) \to (A\to B) or (T\to X) \to (S\to X), 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 (-\circ f): (\bigcirc A \to B) \to (A\to B) is an “equivalence” in the following sense: for every g:A\to B there is a \mathrm{rec}(g):\bigcirc A\to B, such that \mathrm{rec}(g) \circ f \sim g, and for any h:\bigcirc A \to B we have h\sim \mathrm{rec}(h\circ f) (plus, of course, a coherence). Now, one of the things we’d like to know, which certainly ought to follow from (-\circ f) being an “equivalence”, is that if g,h:\bigcirc A\to B become the same upon precomposition with f, they should already be the same. We are doing without funext, so “the same” should mean a homotopy, i.e. we would like g\circ f \sim h\circ f to imply g\circ h. 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 f:X\to Y is an equivalence if and only if (1) f is split surjective, i.e. there is a g:Y\to X such that f\circ g \sim \mathrm{id}, and (2) for all x,y:X, the induced map \mathrm{ap}_f : (x=y) \to (f x = f y) 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 “f is surjective and injective”. The PAT notion of “surjective” is split surjectivity, while the ordinary PAT notion of “injective” would say that for all x,y:X we have (f x = f y) \to (x = y); we simply add the assumption that the latter map is a section of \mathrm{ap}_f. (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 (-\circ f): (\bigcirc A \to B) \to (A\to B). Split surjectivity, with paths made into homotopies, says that for any g:A\to B there is a \mathrm{rec}(g):\bigcirc A\to B, such that \mathrm{rec}(g) \circ f \sim g. This is exactly what we had before: maps A\to B extend along f. However, making paths into homotopies in the second clause says that given h,k:\bigcirc A \to B and a homotopy p : h\circ f \sim k \circ f, we have a homotopy \mathrm{rec}(p):h\circ k such that \mathrm{rec}(p)\circ f = p. 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 p,q:h\sim k and a 2-homotopy p\circ f \sim q\circ f; can we conclude that p\sim q? 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 f:X\to Y to be n-path-split by recursion on n as follows:

  • Every map is (uniquely) 0-path-split.
  • f is (n+1)-path-split if (1) it is split surjective, and (2) for all x,y:X, the induced map \mathrm{ap}_f : (x=y) \to (f x = f y) is n-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 n\ge 2. Moreover, we can put them all together: say that f 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 f.

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 f:A\to B, we define what it means for a type family C:B\to \mathcal{U} to be n-extendable along f:

  • Every C is (uniquely) 0-extendable along f.
  • C is (n+1)-extendable along f if (1) for every g:\prod_{a:A} C(f(a)) we have a \mathrm{rec}(g) : \prod_{b:B} C(b) such that \mathrm{rec}(g) \circ f \sim g, and (2) for all h,k:\prod_{b:B} C(b), the family \lambda b . (h b = k b) is n-extendable.

Similarly, we have ∞-extendable families. We can now express an equivalence such as (-\circ f): (\bigcirc A \to B) \to (A\to B) by saying that the constant family \lambda (x:\bigcirc A). B is ∞-extendable along f:A\to \bigcirc A. 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 (-\circ f) 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 f:S\to T, we define a type X to be f-local if (T\to X) \to (S\to X) is an equivalence. Since this is a precomposition map, we can ask instead that it is ∞-extendable, to get a notion of “f-local” that’s usable without funext. Now the localization of an arbitrary type X is supposed to be its reflection into f-local types, i.e. an f-local type L_f X with a map X\to L_f X such that for any f-local Y, we have an equivalence (L_f X \to Y) \to (X\to Y).

We’ve known for a long time that L_f X can be constructed as a HIT. Simply take a definition of equivalence, funext reduce it, and make it into constructors of L_f X. 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 L_f X : Type :=
| to_local : X \to L_f X
| local_e1 : \forall (g : S \to L_f X), T \to L_f X
| local_s1 : \forall (g : S \to L_f X) (s : S), local_e1 g (f s) = g s
| local_e2 : \forall (g : S \to L_f X), T \to L_f X
| local_r2 : \forall (h : T \to L_f X) (t : T), local_e2 (h \circ f) t = h t.

However, the proof that L_f X is f-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 \lambda (x:T). L_f X is ∞-extendable along f:S\to T.

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.


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK