Smallness

[Alizter]

@jdchristensen This is the stuff from Smallness.v that doesn't rely on the join construction. When we finish the join construction, we can think about adding the other results in.

TODO:

• check all the comments and see if they make sense.
• resolve comments about naming convention. Should we pick islocally_small or islocallysmall? I think the latter.
• Should IsLocallySmall be an inductive type? Experience from IsTrunc suggests that this might be a good idea. (Edit: Probably not)
• Make IsLocallySmall and IsSmall typeclasses?
• Make IsSmall cumulative?

[jdchristensen]

Here's an idea for how to organize things. Rename the folder PropResizing to Smallness or some more general name. Have Smallness/Core.v give just the most basic definitions, e.g. things that can go through with minimal dependencies (e.g. a subset of Basics.Overture Basics.Tactics Basics.Trunc, which are what PropResizing.v depends on). Change the contents of PropResizing to use IsSmall instead of the separate axioms currently there. (This will of course require trivial changes to other places in the library that use those axioms.) Have new files Smallness/JoinConstruction.v which contains the join construction, and Smallness/Smallness.v (?) which contains most of what is currently in the file Smallness.v from my repo.

What do you think, @Alizter?

(I'm also hoping we can reduce the number of files in the theories folder, putting things in appropriate subfolders.)

[Alizter]

@jdchristensen That sounds sensible, I will try to do that.

[Alizter]

I had a go at turning IsLocallySmall into an inductive type but I am having trouble proving it is a hprop. I can get an inversion based proof to the end, but too many universes get introduced. I will hold off on that for now.

[jdchristensen]

Here's an idea for how to organize things.

(I won't repeat it all. See above.)

A further expansion of this idea would be to have a top-level folder theories/Universes which would include things about propositional resizing and smallness, as discussed above, but would also contain the top-level files ObjectClassifier.v, DProp.v, HProp.v, HSet.v, TruncType.v, and any other files that work with universe levels and/or create subuniverses. (And then maybe contrib/UniverseLevel.v could be put there too, even though it isn't needed in practice.)

Other related files are Spaces/BAut.v and Spaces/BAut/*, as well as Modalities/ReflectiveSubuniverse.v. The latter should stay where it is, but I'm not sure about the BAut material. It might make sense to have it in Universes/ as well, so it is alongside ObjectClassifier.v. Or it could stay in Spaces/.

Of course, Types/Universe.v is related, but would remain where it is.

[Alizter]

I've pushed some commits moving things around like you've suggested. I'll continue to work on Smallness when have the time.

[jdchristensen]

Thanks, I think this is good. I've updated STYLE.md to reflect the current situation, and also wrote it assuming that Smallness.v would be moved there. Should we do that now?

[Alizter]

Yes, I will move Smallness.v there, but first I wanted to move out the core file. I had an attempt at doing this a few months ago, but I got stuck updating some other files to do with prop resizing. I can't find that attempt now, but I will have a fresh go at this.

[jdchristensen]

When you move the PropResizing stuff, can you update STYLE.md to stay in sync?

[jdchristensen]

BTW, one of my students will be using universes and propresizing a fair bit, so it might be nice to get at least part of this PR merged soon.

[Alizter]

@jdchristensen In that case, I'll see if I can make some progress with this.

[jdchristensen]

Maybe Spaces/Universe.v should move to Universes/Automorphisms.v, or something like that? It depends on BAut.v and BAut/Rigid.v, so this would suggest that maybe those should move to the new Universes/ folder. It might still make sense to leave the Spaces/BAut/ folder in the current location with the other files in contains, since those are about specific spaces? Or maybe everything should move to Universes/?

[Alizter]

I've pushed a commit using IsSmall in PropResizing, being careful to keep the same universe variables since it can be very sensitive later in the library. However, two results are now homeless:

• issmall_inhabited_issmall
• islocally_small_trunc

I don't really know where to put these.

Edit: For now I've put them in PropResizing.

[Alizter]

I'm still unsure about BAut/. It contains many spaces so it seems kind of wrong to move that. I think we should perhaps just move BAut.v and then explode the contents of BAut since these are all spaces.

Alternatively, we just leave BAut/ alone and just move BAut.v to Universes/.

[jdchristensen]

I'm still unsure about BAut/. It contains many spaces so it seems kind of wrong to move that. I think we should perhaps just move BAut.v and then explode the contents of BAut since these are all spaces.

BAut/ really only contains three things: BAut Bool, BAut Cantor and a file about Rigid types. The file about Rigid types is general theory, while the other two are particular spaces. So I propose:

• Move Spaces/BAut.v to Universes/BAut.v
• Move Spaces/BAut/Rigid.v to Universes/Rigid.v
• Leave the other files in Spaces/BAut/ as they are, still in this folder.

I also think we should rename Universes/Universe.v to Universes/Automorphisms.v.

I think it was a good idea to move the things in PropResizing/ to MetaTheory.

[jdchristensen]

Coq is giving me some weird behaviour with the issmall_hprop instance. For some reason, even when I specify the universe variables in smalltype@{i j}, it generates fresh ones if it has used the instance. Here's an example:

Require Import Basics.Overture.
Definition test@{i j|} `{PropResizing} (P : Type@{j}) `{IsHProp P} : Type@{i}.
Proof.
  exact (smalltype@{i j} P).
  Fail Defined.
  (* Universe HoTT.PropResizing.ImpredicativeTruncation.1105 is unbound. *)
  Restart.
  pose (T := smalltype@{i j} P).
  (* T := smalltype@{HoTT.PropResizing.ImpredicativeTruncation.1093
                    HoTT.PropResizing.ImpredicativeTruncation.1094} P *)
  exact T.
  Fail Defined.
  (* Universe HoTT.PropResizing.ImpredicativeTruncation.1107 is unbound. *)
  Restart.
  pose (T := @smalltype@{i j} P (issmall_hprop@{i j} P _)).
  (* T := smalltype@{i j} P : Type@{i} *)
  exact T.
Defined.

This is with 8.19.1. If I write smalltype@{i j}, it should be looking for a proof of IsSmall@{i j}, and so it should apply issmall_hprop@{i j}. But for some reason it doesn't.

[Alizter]

@jdchristensen Does Set Universe Minimization ToSet help?

[Alizter]

I get the same failures on 8.20. I'm not really sure why fresh universes are introduced.

[jdchristensen]

Does Set Universe Minimization ToSet help?

No, it doesn't.

I get the same failures on 8.20. I'm not really sure why fresh universes are introduced.

Is this a bug in Coq? I'm trying to make a minimal version in vanilla Coq, but am having trouble. During typeclass search, Coq is failing to use hypotheses in the local context to resolve goals.

[jdchristensen]

This LGTM. I'm puzzled by the universe issues in typeclass search, and so we should definitely figure them out, but I'm ok with merging this and leaving that as a separate task. There is also more to import from my Smallness.v file, but it depends on the join construction, which is part of another PR.

[Alizter]

Could IsSmall being cumulative have something to do with it? I'm also thinking that there might be a stray universe somewhere, but I cannot see where it would be.

[Alizter]

Yes, setting IsSmall to be NonCumulative allows your example to succeed. That's interesting. I guess we have a dodgy variance with the universe variables which we need to fix.

[Alizter]

I've fixed the variance by putting a = before i in the definition of IsSmall@{=i j}. The reference manual has the relevant documentation: https://coq.inria.fr/doc/v8.20/refman/addendum/universe-polymorphism.html#cumulative-noncumulative

[Alizter]

Actually, that broke some things, so I've reverted. Unfortunately, I am out of time today, but it is something to do with the variance.

[jdchristensen]

The default variance looks correct to me:

IsSmall@{i j} : Type@{j} -> Type@{max(i+1,j)}
(* +i *j |=  *)

If X satisfies IsSmall@{i j} and i' and j' are two other universes with i <= i' and such that X is also in universe j', then we expect to have IsSmall@{i' j'} X as well.

However, I do see how this flexibility causes Coq to be unsure of what to do. When it is looking for an instance to prove IsSmall@{i' j'} X, it is free to search for an instance of IsSmall@{i j} X with i <= i', which introduces extra universe variables. (This is why I had a comment in Smallness.v saying

(** Note: making [IsSmall] Cumulative makes the following two not necessary, but also means that Coq can't guess universe variables as well in other spots in the file. *)

If we get rid of this flexibility, then we need to reintroduce the lift_issmall and lower_issmall definitions and use them again. I'm not sure what is best: having typeclass inference not introduce variables (but needing to explicitly lift and lower in one or two spots) or the reverse.

[jdchristensen]

I'd lean towards removing the cumulativity. Since this is all about tracking universe levels, it's probably best to be explicit. And having typeclass inference work well will simplify many things.

[jdchristensen]

I'm making good progress and will push something soon.

[jdchristensen]

It turns out that I only ever needed cumulativity in the universe j, while it is the cumulativity in the universe i that caused Coq problems. So by marking i as invariant (=i), we end up with the best of both worlds: typeclass inference works well, and we don't need to do any manual lifting.

This LGTM.

[jdchristensen]

I'd like to get this out to my students, so I'm going to merge. Feel free to make another PR if you spot any things that can still be improved.