Remove some things from Set/Ordinals.v from global namespace?

[jdchristensen]

For example, factor1 and factor2 conflict with the ones defined in Factorization.v. Maybe they can be made into Local definitions? Probably some other things aren't intended to be global as well.

[jdchristensen]

image as well. The issue is that if I Require Import HoTT in external work, I now get the versions from Sets/Ordinal.v by default.

[Alizter]

I think that the real problem here is that the order things are imported in https://github.com/HoTT/HoTT/blob/master/theories/HoTT.v are wrong. The names we actually want to use should end up last, so folders like Sets should be imported exported earlier on.

We can also add some tests to Tests.v that check certain definitions are what we expect them to be. This will catch any name overloads that we don't want in the future.

I'm not sure making things local is the best idea, since someone might want to use the sets image more in the future. With my suggestion they can do Require Import HoTT. Import Sets.LocationOfImage. This isn't possible when things are made local.

[mikeshulman]

I've been thinking for a while that perhaps we really ought to be making more use of modules and namespaces. Instead of trying to give everything a long globally-unique name and then Require Importing everything, it would probably make more sense in many cases to give things shorter names that make sense in the context of their module (e.g. file) and then Require them and refer to them qualified by module name.

[jdchristensen]

It probably won't scale to keep everything globally unique all of the time, but it is handy when things are mostly unique, so that you can tell locally what something means without needing to check what was imported. And names written as Module.name can get pretty verbose.

In the case of Ordinals.v, couldn't that file just make use of the general image function we already have? It seems to be redoing something that we already have for a general modality.

[jdchristensen]

It turns out that Ordinals.v could just use Modality.image (Tr (-1)) f and the related facts about it, except for one minor thing: currently Ordinals.v defines its image using HIT.quotient which cheats a bit and defines the quotient of an hprop-valued relation on a type A : Type{i} to be in Type@{i}, even without knowing that the hprops land in Type@{i}. (At the very least, HIT.quotient should require the PropResizing axiom, so this usage is correctly tracked.) Ordinals.v makes use of this. So, to instead use Modality.image (Tr (-1)) in Ordinals.v, we could prove that the image it produces when the codomain is an hset is equivalent to a type in Type@{i}, assuming PropResizing. It's probably worth having this general fact recorded anyways, and then the second definition of image wouldn't be needed.

[mikeshulman]

Sounds excellent!

On Sat, Aug 7, 2021 at 3:03 PM Dan Christensen @.***> wrote:

It turns out that Ordinals.v could just use Modality.image (Tr (-1)) f and the related facts about it, except for one minor thing: currently Ordinals.v defines its image using HIT.quotient which cheats a bit and defines the quotient of an hprop-valued relation on a type A : Type{i} to be in Type@{i}, even without knowing that the hprops land in Type@{i}. (At the very least, HIT.quotient should require the PropResizing axiom, so this usage is correctly tracked.) Ordinals.v makes use of this. So, to instead use Modality.image (Tr (-1)) in Ordinals.v, we could prove that the image it produces when the codomain is an hset is equivalent to a type in Type@{i}, assuming PropResizing. It's probably worth having this general fact recorded anyways, and then the second definition of image wouldn't be needed.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/1567#issuecomment-894711547, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAE53SELYU5V6LESUEBN3K3T3WUT7ANCNFSM5BWQU4HQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email .

[jdchristensen]

I started this, but got bogged down a bit. Here are the steps I was thinking of:

• Change HIT.quotient to not cheat with universes. Probably simplest to just assume that A and the values R a b of the relation lie in the same universe u, and then make the HIT land in u as well.
• Add an alternate version of HIT.quotient, e.g. HIT.quotient_resized that assumes propositional resizing and proves that when A : Type@{u} and R : A -> A -> Type@{v} (prop valued), we can still construct the quotient in Type@{u} (with no constraints between u and v). This would be proved using the HIT above, not defined axiomatically.
• Ordinals.v would use quotient_resized, but otherwise stay unchanged at this point.

After that phase, then I would want to:

• Use quotient_resized to prove that Modality.image f can be chosen to lie in the same universe as the domain of f when the codomain is a set. This would essentially take what is currently in Ordinals.v and adapt it to be a proof of this fact. (This fact is a special case of the join construction, by the way.)
• Then Ordinals.v could be adapted to use Modality.image, along with the smallness property proved about it.

The first phase is making the library more honest about universe levels, and the second phase proves a special case of the join construction, and eliminates some redundancy.

I started the first step of the first phase, and most things build fine. (Of course Ordinals.v and its dependencies (only in the Sets folder) won't build until the second step is done, but that's expected.) The only two files I had trouble with here are natpair_integers.v and field_of_fractions.v. I'm sure it's easy to fix them, but the universe variables there are undocumented, so I don't know what constraints to aim for.

I'm going to put this aside, but if anyone else wants to tackle it, the outline above gives one possible approach. The few changes I made are shown in this gist.

[Alizter]

@jdchristensen We have Colimits/Quotient which is supposed to replace HIT/quotient.v. The only reason I kept the later around is because it is difficult to completely remove. It's unfortunate that it got used here. I have a branch somewhere which is attempting to do so, which I can try to resurrect.

[jdchristensen]

Thanks for pointing that out! So one task is:

• Remove HIT.quotient from the library, and use Colimits/Quotient instead.

The good news is that that is really orthogonal to the other changes I proposed, making it easier to do the other changes without getting bogged down in unfamiliar parts of the library. The other changes are:

• Add an alternate version of Colimits.Quotient, e.g. Colimits.Quotient_resized that assumes propositional resizing and proves that when A : Type@{u} and R : A -> A -> Type@{v} (prop valued), we can still construct the quotient in Type@{u} (with no constraints between u and v).
• Use Quotient_resized to prove that Modality.image f can be chosen to lie in the same universe as the domain of f when the codomain is a set. This would essentially take what is currently in Ordinals.v and adapt it to be a proof of this fact. (This fact is a special case of the join construction, by the way.)
• Adapt Ordinals.v to use Modality.image, along with the smallness property proved about it.