Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Split up ReflectiveSubuniverse.v into smaller files
I think splitting up ReflectiveSubuniverse.v will be beneficial for readability. At the moment we have one big file (~2000 lines) which makes it very difficult to read and find things in. I propose splitting these up into smaller files as follows:
- Core.v containing the definition of ReflectiveSubuniverses (basically up to ln 252). And Restrictions and Unions from the end.
- Functor.v containg results about the functoriality of ReflectiveSubuniveres.
- Equiv.v containg results about O-equivalences (O_inverts)
- Type.v contain results about the interaction of RSUs and various type constructors
- Decidable.v about the interaction with decidability
- Monad.v about the monad stuff
- Connected.v about O-connected types
- Map.v about O-local maps
- ConnMap.v about O-connected maps
These would all of course be indexed by a ReflectiveSubuniverse.v file which means the rest of the library would remain untouched.
In principle, I'm certainly in favor of this (and perhaps something similar for Modality.v). Probably they should all be in a subdirectory Modalities/ReflectiveSubuniverse.
The reason I haven't done this before is that the module-wrangling seemed difficult. I wanted there to be just one "ReflectiveSubuniverse_Theory" module that a user could import rather than having to import separate modules for all the separate files, and a single Coq module can't span multiple files. Perhaps the main index file could contain one module that Exports all the modules from all the sub-files. But the individual sub-files would have to manually import the appropriate modules from each other, and if for instance the ConnMap_Theory module imports the Connected_Theory module and then both are imported from the index file, I think we might end up with two copies of the Connected_Theory module, which might be a problem for typeclass inference, unification, etc. Some multiple-inheritance issue like that already arose somewhere in the modalities library I think. But please try it and find out!
It's also come to my attention that there are people working on universe minimization in coq currently. As I understand, this will lead to a point where records can be just as polymorphic as modules. If this is the case, the modalities library ought to be redesigned using records (or classes). Hopefully we won't have the overly restrictive universe levels that I ran into recently with the seperation RSU.
I don't know what universe minimization refers to here, but I can't imagine a semantically consistent way that records could be as polymorphic as modules, since a polymorphic object is itself larger than any given universe and hence cannot belong to any universe.
@mikeshulman I don't know the details fully yet either, but we will see in the future. Regarding semantics I have even less of an idea.
@mikeshulman Also, what does "replete" mean? I couldn't find it in RSS or in HTT. Should we perhaps include a definition in the documentation?
On what are you basing your expectation that universe minimization would enable records with polymorphic fields?
https://ncatlab.org/nlab/show/replete+subcategory
@mikeshulman Nothing serious, I have just been chatting with Andreas Lynge. Looking back over the emails, I think I may have misunderstood. He suggested that it may be possible to rewrite the parts of the library using records and classes (might be speculation I don't know).
He did however agree that it would seem possible to relax the signature requirements of modules with respect to universes. I.e. have some sort of mechanism that coq can insert extra universes if it needs to, without having to change the signature of a parameter of a module type.
But most likely I have misunderstood.
@mikeshulman I had an attempt at splitting it up but as you said there are multiple copies of the same things floating around which is causing unification problems. It doesn't look like this is possible currently.
I'm going to close this issue for now since I don't see anything coming out of it. You are correct that "module-wrangling" is causing much difficulty here. If in the future we manage to rid ourselves of having to use modules somehow, this might serve as a basis for refactoring the modalities library.
I do not understand why we use module types instead records and classes. Considering the inflexibility with universes in module types, I would try using records and classes before module types. Records and classes instead of module types might make the modalities library easier to understand as well. But @mikeshulman maybe you know the reason for using module types in the modalities library?
The issue with records and classes is that an individual instance of a record or class is not universe-polymorphic. With module types we can have that "a modality" is simultaneously defined on all universes, rather than having separate notions of "modality on U" for all universes U. This matters when considering for instance whether the universe of modal types is modal.
Does the original suggestion to split as:
- Core.v containing the definition of ReflectiveSubuniverses (basically up to ln 252). And Restrictions and Unions from the end.
- Functor.v containg results about the functoriality of ReflectiveSubuniveres.
- Equiv.v containg results about O-equivalences (O_inverts)
- Type.v contain results about the interaction of RSUs and various type constructors
- Decidable.v about the interaction with decidability
- Monad.v about the monad stuff
- Connected.v about O-connected types
- Map.v about O-local maps
- ConnMap.v about O-connected maps
still make sense @mikeshulman ?
That sounds too fine-grained to me. While a huge file poses problems, it's also hard to find things when they are spread among many files. In particular, I think connected maps and connected types should be together. Not sure of the details of the rest, but maybe more should be in the Core file.
I think you are right that this is too fine-grained. Perhaps we should start small. How about splitting off the results about connected maps? We would have two files Core.v and ConnMap.v.
I'd say that the name of the main file should remain unchanged. But I think you should wait until Mike gives his opinion.
Hmm. Let me ponder.
We also don't have to respect the current division into ReflectiveSubuniverses and Modalities. For instance, if we wanted to (I'm not necessarily suggesting this), we could put all the theory of connected types, connected maps, and modal maps in a file together with the definition of the modal factorization system for a modality.
I think there are two pieces of ReflectiveSubuniverse that feel to me kind of separate and split-off-able. One consists of the facts that the subuniverse is closed under, or the reflector preserves, various type constructors. The other consists of all the various subsidiary classes of types and maps: connected types, connected morphisms, modal morphisms, O-equivalences.
Here's another possible refactoring: for any Subuniverse, we can define the notion of a map being fiberwise in that subuniverse, and prove a bunch of things about it like closure under pullbacks and equivalences and homotopies. Then since the connected types for any reflective subuniverse form a subuniverse themselves (though not a reflective one), we get both modal maps and connected maps as instances of this general notion, and unify lemmas like mapinO_isequiv with conn_map_isequiv and so on. Would that be worth it?
The stuff in ObjectClassifier.v should also be generalizable to the classifier of morphisms with fibers in any subuniverse. And if we were willing to move the definition of Subuniverse and its classifier earlier, then we could make TruncType n definitionally equal to Type_ (Tr n), since IsTrunc n is definitionally (though not syntactically) equal to In (Tr n).
@mikeshulman Since a lot of things changed since this issue was opened, do you think it is still worth pursuing?
Yes, I do. After #1238 it's much more feasible than previously.
However, I won't have time to do it myself in the near future.