Closed mikeshulman closed 4 years ago
I'm glad you are bringing this up for discussion! Thanks for laying out the full story so clearly.
When I was first thinking about formalizing some things from CORS, which only assumes one universe, I certainly felt that the complicated framework of modules and universe polymorphic modalities was a huge amount of overhead that got in the way of what are in many cases simple ideas. This was enough of a problem that I still haven't understood how modalities work in the library. I'm sure with a few pointers I could get up to speed, but it would be nice if that burden simply wasn't there.
I am also concerned by the issue of what the current implementation means semantically, although it could in fact be that the current approach is in some ways closer to the ∞-topos world, where a reflective subcategory makes no mention of a universe at all. Still, I think it would be better to be on more solid semantic ground, and to avoid features that are specific to Coq.
And I agree with your other criticisms of the current approach as well.
I don't fully understand your proposal for an inductive definition of AccModality. Without suspensions, won't we need to prove that the separated modality exists? And if so, shouldn't that proof not need accessibility? Oh, but maybe all of that is in the coercion you mention later. I guess I wonder whether anything in the library will become circular with the proposal.
If this were done, how would the issue about the universal of modal types being modal be handled for a lex modality? Would it only work for accessible lex modalities? Or could one still in some places work with polymorphic modalities, but only when needed?
BTW, after some digging, I found a source of non-accessible localizations of spaces based on the fact that in the category of groups you can nullify wrt a proper class. I won't clutter up this thread with more info, but I'm just mentioning it to point out that the non-accessible case isn't trivial.
Sorry that I wasn't more clear. The order that I'm thinking of doing things in is:
The way I'm envisioning things working in practice is that most of the time the user only needs to talk about single-universe Modalities. Particular examples like truncation will be (obtained through AccModality as) polymorphic elements of Modality. (Perhaps for this to work we'll need to do something like parametrize an element of Modality by two universes, one for the size of the types being reflected and one for the size of the types being eliminated into.) On those few occasions where we really do need an abstract polymorphic (accessible) modality, we just assume an element of AccModality instead, and hopefully can mostly treat it like an ordinary Modality through the coercion. So the casual user of the library would hopefully not need to look under the hood at the definition of AccModality, or perhaps even be aware of it depending on what they're doing.
Re lex modalities, I spoke sloppily: I only know how to prove that the universe of modal types is modal when the lex modality is accessible. So nothing is lost there, relative to current technology, by restricting to the accessible case.
I think it might still in theory be possible to say things about polymorphic non-accessible modalities, e.g. by hypothesizing explicitly two Modalities on different universes whose modal types and reflectors coincide on the smaller universe. It would be kind of cumbersome, but I don't know of any use case for it yet either. I'm interested to hear that non-accessible localizations of spaces are known to exist (is there any chance of that proof working constructively?); but are we ever likely to want to apply such a localization universe-polymorphically?
Oh, and another question to deal with is whether and where to assume funext. The current definition of reflective subuniverses in the library uses the notion of ooExtendableAlong
to avoid funext (as I wrote about in gory detail here). This was originally done because it was hard to parametrize modules over an assumption of funext, but it has the additional advantage of avoiding funext redexes. This seems particularly valuable to me because in the accessible case the eliminator obtained from the explicit construction as a HIT enables direct funext-free proofs of many facts, so it would be a shame if to gain the additional generality of deriving those facts from a general theory of modalities we had to introduce unnecessary funext-redexes.
(Whenever I talk about avoiding funext, people ask whether I care about models where it fails. No, I don't know of any such models -- it's mainly that in Book HoTT it's tedious and annoying to constantly have to manually beta-reduce funext-redexes when you could avoid introducing them in the first place. And one can hope, at least, that when axioms aren't involved a definition can sometimes be completely computed by Coq.)
But ooExtendableAlong
is another layer of complication for the newcomer relative to IsEquiv
, so one could make an argument for doing away with it too. I'd probably incline to keep it, at least for now, but I'm interested to hear other opinions too.
(In fact, according to my sketch I think we need funext already at step (2), to show that an Empty-null type is contractible. But that is probably easy to avoid, e.g. by including a separate constructor of AccModality for Tr(-2).)
A few more thoughts:
About the non-accessible reflective subcategories: it's on my to do list to learn more about this and to try to see if it works constructively. I suspect that it does.
About funext: I like the idea of avoiding it. The ExtendableAlong stuff is a bit confusing, but I think could be made easier for the newcomer with a short summary at the top of Extensions.v. It could describe the three main types, ExtensionAlong, ExtendableAlong and ooExtendableAlong, and say that in the presence of funext ExtendableAlong n+2 and ooExtendableAlong are equivalent to the restriction map being an equivalence which is the same as saying that every map has a unique extension. I think just that much is most of what people need to know.
About the inductive type AccModality. First, shouldn't it be called AccRSU or something like that? Second, here's another idea for how to define AccRSU. It could be a record consisting of an indexing type I, families A, B : I -> Type, a family of functions f : forall i, A i -> B i, and a function s : I -> nat. The last bit indicates that f i should be formally suspended s i times. That is, when defining the local types, you look at the (s i)-fold identity types. Just an idea to make it closer to how we already think of the data for an accessible RSU.
My last observation is that some parts of the theory go through without knowing that the subuniverse is reflective, but just knowing that one or more types has a reflection. E.g. parts of CORS are written assuming that you have a map eta : X -> X', where X' is in a subuniverse and eta has the right universal property, but without using that every X has such a reflection. For results like that, you need even less machinery. For example, some of them won't need HITs. If things are reorganized, is it worth recording such "objectwise" results somewhere?
I wasn't making a distinction between RSUs and modalities yet. Yes, the most general thing would be a generating family for an RSU. Your suggestion is good too; it might be useful to avoid the inductiveness.
Regarding your last question, are there interesting examples where particular types have reflections but not all types do?
@mikeshulman What about connected types? We can construct a connected cover for some types but not all. This is kind of like a reflector but I haven't checked it.
It's not a reflector; for one thing it goes the other way. And isn't the n-connected cover of a type just the fiber of the map to its n-truncation?
Oh right the projection goes the other way, never mind.
We don't know that cohomological localizations exist for all cohomology theories, but I suspect one can find particular examples that exist for a particular space. There could be something similar about hypercompletion. But the place we do this in CORS is Prop 2.24: we characterize when a map X -> X' is an L-separated reflector without needing to know that the subuniverse of L-separated types is reflective. We then use this to prove that it is reflective. Of course, one could universally quantify 2.24 over all X, but that seems unnecessary.
There are several other results in CORS also stated without assuming that the L-separated types form a reflective subuniverse since they occur before we prove this.
I don't think it's very important, but it's a lightweight way to handle some things. For many results, all you need to have is a subuniverse and a single reflector X -> X', and you can prove the result.
Well, it should be easy enough to unbundle the notion of RSU in that way. Start with a Subuniverse
that's just a function Type -> hProp
, then define a Reflector O X
for a subuniverse O
to be a type OX
in O
with a map X -> OX
and a universal property, and finally define a ReflectiveSubuniverse
to be a subuniverse together with a reflector for every type.
Perhaps IsReflective O X
should be a typeclass, so that we can use the same notation for the unit map regardless of whether only X is reflective or whether the entire subuniverse is.
I suppose "being reflective" could also be a typeclass property of a subuniverse, but I'd be more inclined to bundle that one up, in part so that we can continue coercing an RSU to its reflector. Although in the case of a single reflective type we'd have to use a different notation for the reflected object. Hm.
Since this comment is more of a design discussion rather than about the implementation, I thought I'd put it in this issue instead of in the pull request. One thing I'm wondering is whether AccRSU (and AccModality) are trying to do too much. They include constructors that match the usual meaning of accessible (generated by a family of maps), but they also included constructors like ContrRSU, IdentityRSU and SepRSU that aren't literally described using generators. These are redundant, and also a bit confusing since they are handled differently than the cases described using generators. And in principle there might be other ways in which one can define a polymorphic family of RSUs. Should those be added to AccRSU as they are found? E.g. does double-negation fit into this? Or what if I come up with a non-accessible but polymorphic family via the group theory approach?
An alternative is to accept that there will be different kinds of data that can give rise to a polymorphic family of RSUs. The first is the family of truncations. The second is a generating family of maps. A third is the L' construction. And there are maybe more. If these are separated out, then the truncations could be defined as they were before, minimizing the changes needed to the library, and also avoiding needing the ExtendableAlong stuff in Overture.v.
A counterargument is probably that in order to state polymorphic theorems, the hypotheses need to be some data that produce polymorphic RSUs, and you don't want to restate theorems for every kind of input. But I think there may be only one theorem of this type, the one about the universe of modal types for a lex modality. And I still wonder if it might be possible to state this as something involving two lex modalities, one of which is assumed to live in a strictly larger universe and which extends the other one.
Anyways, just some things to think about before the current implementation gets too far along...
Well, as the name suggests, AccRSU
was supposed to represent accessible RSUs, so non-accessible examples like double-negation or group-theoretic nullifications wouldn't fit. I was thinking of the extra constructors as just a technical convenience mainly for the purpose of IsTrunc (although they would also apply to more general accessible RSUs of separated objects), and since no other example is likely to have the central position in the library that IsTrunc does, I wouldn't expect to want to add anything else in the future.
The theorem about the universe of modal types is actually for an accessible lex modality; accessibility is actually used in its proof, it isn't just a convenience giving a way to state a theorem about a polymorphic modality. And I actually hope there are more theorems of this sort waiting to be found -- to prove things about the identity types of more general modalities and RSUs, we expect to need univalence to do encode-decode-type arguments, and modal properties of the universe seem to be a good way to apply such arguments to localization HITs. But it's also certainly true that, at least informally, such a theorem can be stated by referring to two modalities, as indeed we did in RSS (one accessible modality and its "canonical accessible extension" to a higher universe).
Your suggestion is, I believe, more or less what I was originally trying to do however-many-years ago, before I gave it up as impossible and started using modules in the first place. However, Coq's universe polymorphism is now more flexible and powerful, and I've learned a lot more about how to tune it (in part through fighting with those same modules), so it's quite possible that this approach would actually work. I certainly agree that in principle it seems like it should. Perhaps I/we should try it and see.
I still think it's overkill to define an accessible subuniverse in Overture.v. All we need at that point is the n-truncated subuniverses, which can be defined directly without ExtendableAlong. Later they can be shown to be special cases of the concept of an accessible subuniverse, when things are being proved about them. And if AccRSU comes later, it could coerce some of its terms to definitionally equal subuniverses to the ones directly defined in Overture.v, if that's helpful.
(Being new here, I can still imagine the reaction someone will have if the first thing they need to read before understanding Contr, etc, is ooExtendableAlong...)
Yes, that's certainly a good point. I think I was mainly hoping to avoid the current problem that IsTrunc n
and In (Tr n)
are definitionally but not syntactically equal -- and that we can't declare global instances in both directions without creating loops -- by setting things up so that the former could be merely a notation for the latter. But that problem is admittedly quite minor, and so far #1224 has its own even more serious issues with unfolding. So I think I'll try dropping that route for now, as you suggest, and see how far we can get with the naive approach.
Right, I see now what you were trying to achieve. Not sure if I have a good suggestion for how to deal with it.
Another comment about the redundancy in AccRSU: with the proposal you have, every time you want to prove a result about something in AccRSU, you have to prove it for the literally accessible ones, and then also for the n-truncations. Now presumably there would be a lemma saying that the n-truncations are equivalent to certain accessible RSUs, so you can reduce to the case of an accessible RSU, but it seems strange to have a redundant set-up and then to repeatedly use a lemma to work around this...
One could alternatively have AccRSU represent a literally accessible subuniverse, and then have a typeclass IsAccessible that says that there merely exists a term in AccRSU that produces a subuniverse equivalent to the given subuniverse. Then terms of type AccRSU as well as n-truncations would satisfy IsAccessible via a typeclass instance, and all results about accessible subuniverses would apply to either case. But the proofs (of hprops) could assume to have generators.
Again, just an idea, as I still haven't fully wrapped my head around how the Modalities directory works and how things will fit together.
Currently our library for modalities (including reflective subuniverses) uses Coq's modules and module types: instead of the obvious approach of each modality being an element of a record type called (say)
Modality
, each "family of modalities" (truncations, localizations, etc.) is a module that instantiates a particular "module type". The reason for doing it this way was that an individual element of a record type cannot be universe-polymorphic, although the record type itself can be; thus with the obvious approach we would have a separate type of "modalities on universe U" for each U. Which is not a problem for many purposes, but it becomes an issue when we want to say things like "the universe of modal types is modal" (for a lex modality) or "the universe of modal types is separated" (for any RSU); the latter can be finessed as in CORS, but the former less so. In addition, when working with practical examples (notably truncation) we want to know that a type X has only one truncation, which happens to live in the same universe as X, but satisfies a polymorphic elimination principle mapping into types in any universe. I wrote a long blog post about this almost 5 years ago.This way of representing modalities does however have notable problems. For instance:
So recently I've started pondering whether another approach is possible. Note that nearly all universe-polymorphic modalities are accessible, and thus actually determined by a small amount of data. (In fact, I think the only modalities that I don't know to be accessible in general are double-negation and those constructed impredicatively.) So my proposal is to have two notions of modality (and reflective subuniverse, etc. -- everything I say applies to both):
A record type of modalities, which is universe-polymorphic in the usual way: thus an element of
Modality@{i}
is an operation on the universeType@{i}
that satisfies an elimination principle only into other types inType@{i}
.A record type of accessible modalities, for which an element of
AccModality@{a}
is a "generator" that itself lives in universeType@{a}
.Then there would be a coercion from (2) to (1) that is polymorphic:
AccModality@{a} >-> Modality@{i}
for anyi >= a
. So most of the time we can work with ordinary one-universe modalities, but when we need accessibility, or when we need universe-polymorphism, we can restrict to the accessible ones.My first thought was that an element of
AccModality
would be just literally a generating family, as we now use for localization and nullification. The main problem with this that I see is that we want the universe-polymorphic notion of truncatedness to be defined early on inBasics
, but to define truncation as a localization we need spheres of all dimensions and some theory of suspensions, and it would be weird to have to put those in Basics.So today I had a slightly different idea: the type
AccModality
, which is defined inBasics
, is an inductive type generated by constructors such asOf course there is some duplication here, since Sep(Loc(f)) = Loc(Susp(f)), but that's the point -- with this we can define in
Basics
at least what the modal types are for a givenAccModality
, includingIsTrunc
for the truncations, without needing to have suspensions and spheres. (This will have the additional advantage of makingIsTrunc n
syntactically, and not just definitionally, equal toIn (Tr n)
.) Then in a laterModalities
directory we can use HITs to actually construct localizations, including truncations, define the coercionAccModality >-> Modality
, and so on.Thoughts? Of course we'd need to experiment to find out how well this would actually work, and I probably don't have time to try it myself right now. But I think something like this is worth trying.