Files in theories/ folder

[jdchristensen]

I think we should have fewer files in the theories/ folder. Let's discuss options for reorganizing things here.

These files correspond to subfolders and import everything in the corresponding subfolder. I think it is useful to keep them.

Basics.v
Categories.v
HoTT.v
Pointed.v
Types.v
Truncations.v
WildCat.v

I'm not sure about these two. Maybe it's fine to keep them.

Utf8Minimal.v
Utf8.v

This file is empty and should be deleted (even if we make a Misc folder):

Misc.v

Even though we have a Tactics folder, this file does not index it and is independent. I suggest we rename it to Tactics/Core.v. I also suggest that we remove the Require Export Tactics.BinderApply. line, since that seems independent. But maybe we should add Require Export Basics.Tactics.?

Tactics.v

I think this file should move to Axioms/.

ExcludedMiddle.v

This file should move to Homotopy/.

NullHomotopy.v

Here are the files that require more discussion:

BoundedSearch.v
Constant.v
EquivGroupoids.v
Extensions.v
Factorization.v
Functorish.v
HFiber.v
Idempotents.v
Projective.v

Functorish.v is unused, but I now see that it overlaps a bit with work in #2153 (the changes to Types/Universe.v). I think we could just delete this file. The only question is whether to keep the Class Functorish and use it with the changes in #2153.

EquivGroupoids.v could be appended to Types/Equiv.v. OTOH, it isn't used anywhere in the whole library. OTOH, it takes ~0.1s to build, so would not be a big deal to include as part of Equiv.v.

Many of the others could go into the Homotopy/ folder, especially if we regard that as "things developed in HoTT using the foundations in the rest of Coq-HoTT". The one that fits the least well is BoundedSearch.v. But there is new work coming on "searchable types" and the related "compact types" that will probably go in Homotopy/, so maybe it's fine to also put it in Homotopy/? An alternative is a Misc/ folder that could contain a few things.

The work in #2153 on injective types also needs a home, but I think Homotopy/ would be fine for it as well.

[Alizter]

I'm not sure about these two. Maybe it's fine to keep them.

Utf8Minimal.v
Utf8.v

I've removed Utf8.v in #2156, but Utf8Minimal.v is used more commonly throughout mathclasses. I think the best thing to do would be to move it there. I will think about it some more.

This file is empty and should be deleted (even if we make a Misc folder):

Misc.v

Done in #2157.

Even though we have a Tactics folder, this file does not index it and is independent. I suggest we rename it to Tactics/Core.v. I also suggest that we remove the Require Export Tactics.BinderApply. line, since that seems independent. But maybe we should add Require Export Basics.Tactics.?

Tactics.v

I agree with moving this file, but I also noticed while ago that there is some material in there that belongs elsewhere. I would suggest that we clean this up too.

I think this file should move to Axioms/.

ExcludedMiddle.v

This one I disagree with since Axioms.v really contains files you can Require to have such an assumption in your file. I will come up with a better proposal later.

This file should move to Homotopy/.

NullHomotopy.v

Yes, this is a good idea. Done in #2158.

Here are the files that require more discussion:

BoundedSearch.v
Constant.v
EquivGroupoids.v
Extensions.v
Factorization.v
Functorish.v
HFiber.v
Idempotents.v
Projective.v

Functorish.v is unused, but I now see that it overlaps a bit with work in #2153 (the changes to Types/Universe.v). I think we could just delete this file. The only question is whether to keep the Class Functorish and use it with the changes in #2153.

Feel free to include any material like this in #2153. I think this can be generalized to wild cats but I haven't thought it through yet. I'm ok with simply deleting it also, but it would be good to think about it some more.

EquivGroupoids.v could be appended to Types/Equiv.v. OTOH, it isn't used anywhere in the whole library. OTOH, it takes ~0.1s to build, so would not be a big deal to include as part of Equiv.v.

That sounds sensible to me. I'll create a PR later.

Many of the others could go into the Homotopy/ folder, especially if we regard that as "things developed in HoTT using the foundations in the rest of Coq-HoTT". The one that fits the least well is BoundedSearch.v. But there is new work coming on "searchable types" and the related "compact types" that will probably go in Homotopy/, so maybe it's fine to also put it in Homotopy/? An alternative is a Misc/ folder that could contain a few things.

I'm ok with a Misc/ folder. I think including more and more things into Homotopy/ makes it a bit random, but I don't have a good definition of "homotopy theory" that doesn't touch everything else in the library. Maybe anything vaguely related to computing homotopy groups.

The work in #2153 on injective types also needs a home, but I think Homotopy/ would be fine for it as well.

Sounds sensible.

[jdchristensen]

A Misc folder is probably reasonable. In a sense, we already have one, namely the theories folder. For the things mentioned above that need discussion, which do you think should go in Misc and which in Homotopy?

BTW, we should make sure to update STYLE.md for any changes made if the moved files are mentioned there.

[jdchristensen]

About STYLE.md, NullHomotopy.v needs to be removed from the top-level list there.

I agree that ExcludedMiddle shouldn't move to Axioms. I thought about moving it to Basics, but it uses Types.Sum Types.Arrow Types.Empty. It could go into Misc, but that seems to suggest it is tangential. Is there a better name than "Misc" that would capture the idea of "Files that depend on things in Types and might still be core files, but don't fit elsewhere"?

Another alternative is to expand the idea of Types to include ExcludedMiddle.v, HFiber.v, IdentitySystems.v, etc. E.g. ExcludedMiddle_type and hfiber are kinds of type formers too.

Right now, things often end up in theories or Homotopy simply because they depend on files in Types.

(BTW, the Import line in ExcludedMiddle can have Types changed to the three listed above.)

[Alizter]

Thinking about this more, ExcludedMiddle.v might fit into Decidable.v, since it is really an assertion that every type is decidable.

[jdchristensen]

Thinking about this more, ExcludedMiddle.v might fit into Decidable.v, since it is really an assertion that every type is decidable.

You mean Basics/Decidable.v? It doesn't work, due to the dependencies on three files in Types/.