The size of HITs is unaffected by the size of path-constructor inputs

[mikeshulman]

Because the path-constructors of a HIT are axioms that aren't visible when the type itself is defined as a Private Inductive, the size of their inputs doesn't affect the size of the resulting HIT in the way that it should. This caused a universe problem in exercise 10.11 to go undetected by its Coq formalization.

It seems that we ought be able to fix this with an extra hack. One such hack is used in Suspension.v, but I don't immediately see how to translate that hack to V. Any suggestions?

[JasonGross]

I'm not sure I completely understand, but does passing around the universes explicitly in the induction principle fix things? (If you need two universes to be related, you can do let enforce_lt := Type@{i} : Type@{j} in or let enforce_le := idmap : Type@{i} -> Type@{j} in.)

[mikeshulman]

The problem is, I think, in the axiom setext rather than the induction principle. Will those tricks work in an axiom?

[spitters]

Is it related to this one?

Require Import HoTT.
Require Import quotient.

Definition Type2:=Type.
Definition Type1:=Type:Type2.

Variable A:Type1.
Variable rel :A-> A-> Type2.
Variable relset: setrel rel.

Definition Quot:Type1:= quotient relset.
(* However, this quotient should be in Type2, the maximum of the two types *).

We discussed this before. @mattam82 has a patch, but I don't know whether it has been pushed already.

[mikeshulman]

It seems like very much the same problem. I'm curious how this could be fixed by a patch to Coq rather than a hack on top of private HITs. It doesn't seem to me that in general you'd want the size of an inductive type to be raised by the size of its parameters; isn't the problem rather that the size of Quot should be large because R appears in the constructor related_classes_eq, which Coq doesn't see because it's an axiom rather than an actual constructor?

[JasonGross]

If we get polymorphically-discharged module-local universe variables, that should work, right? If you tell me what the universes should look like in pseudo-Coq-code, I might be able to suggest either a feature or kludges or both.

[mikeshulman]

Yes, polymorphically-discharged module-local universe variables would do the trick; then we could write

Module Export CumulativeHierarchy.

Universes U U'.

Private Inductive V : Type@{U'} :=
| set {A : Type@{U}} (f : A -> V) : V.

Axiom setext : forall {A B : Type@{U}} (R : A -> B -> hProp@{U})
  (bitot_R : bitotal R) (h : RPushout R -> V),
set (h o (inL R)) = set (h o (inR R)).

Actually, maybe it would work right now to write

Module Export CumulativeHierarchy.

Private Inductive V : Type@{U'} :=
| set {A : Type@{U}} (f : A -> V) : V.

Axiom setext : forall {A B : Type@{U}} (R : A -> B -> hProp@{U})
  (bitot_R : bitotal R) (h : RPushout R -> V@{U' U}),
set (h o (inL R)) = set (h o (inR R)).

? That wouldn't generalize to all HITs, but the definition of V already knows about a universe that has to be smaller than the one that it lives in.

[JasonGross]

Doesn't V take two universes? Do you mean V@{U' U} in the second example? That should constrain the body of h to only be able to use set with types in U (i.e., with types in the same universe as the A and B passed to setext).

[mikeshulman]

Yes, V takes two universes; I made a typo in my comment at first and fixed it immediately. (-:

I think the constraint that you say is the correct one: a given instance of V is defined with a particular universe U as the domain of set. We might in theory want to allow R to take values in a different universe, with V being in a universe larger than both, but in practice I don't think requiring R to live in the same universe as A and B is a serious problem.

[JasonGross]

Ha. Github doesn't update with edits unless you refresh the page, it seems. (They are also not reflected in emails. I wonder if this is a place where Google Wave would be better than gmail.)

Anyway, yes, I think your second example will work, assuming that you check to see which order universes go in (arguments first would make sense, but I'm not 100% sure).

[mikeshulman]

It's definitely the other way round for V.

[spitters]

The patch adds user syntax Type@{(max U V)}. We can then write:

Private Inductive quotient (sR:setrel R@{U V}): Type @{(max U V)} :=
  | class_of : (A:Type@{U}) -> quotient sR.

On Sat, Oct 11, 2014 at 10:49 PM, Mike Shulman notifications@github.com wrote:

It seems like very much the same problem. I'm curious how this could be fixed by a patch to Coq rather than a hack on top of private HITs. It doesn't seem to me that in general you'd want the size of an inductive type to be raised by the size of its parameters; isn't the problem rather that the size of Quot should be large because R appears in the constructor related_classes_eq, which Coq doesn't see because it's an axiom rather than an actual constructor?

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/565#issuecomment-58764050.

[mikeshulman]

Ah, I see! Yes, that would be a useful syntax.

[mikeshulman]

For the record, hit.Localization is also affected by this issue. So when we get around to fixing it, we should fix it there too.

[JasonGross]

I fixing this for quotient, and the anomalies bit me.

[mikeshulman]

Bummer! Is that syntax supposed to be allowed, though? @mattam82 's comment in the other thread about algebraic universes suggests to me maybe not.

[JasonGross]

It's certainly not supposed to give anomalies. I think it should be allowed whenever it doesn't result in algebraic universes on the right, and, as I understand it, this is a case in which it would not. For example, it's fine to say that prod@{i j} A B lives in Type@{max(i, j)}, so it should be fine, here, too. More precisely, we've moving quotient@{i j} from living in Type@{i} to living in Type@{max(i, j)}, so there should be no additional constraints to enforce.

[mikeshulman]

Yes, of course nothing is supposed to give anomalies. And you're right, it should be allowed here if it's allowed in prod.

[JasonGross]

Anomalies have been fixed in most recent trunk, and it looks like it might have been giving anomalies only in not-universe-polymorphic mode, but I haven't tested.

[spitters]

As this is now part of: https://github.com/HoTT/HoTT/blob/master/STYLE.md#universes-and-hits shall we close this?

[mikeshulman]

Well, we should actually implement the fix first, shouldn't we?

[spitters]

@mattam82 I am trying the quotient example above. I though the notation max was now allowed. However, it is missing from https://coq.inria.fr/refman/Reference-Manual032.html#sec784

Coq tells me:

Syntax error: [universe] expected after '@{' (in [constr:sort]).

[JasonGross]

I think the syntax is Type@{max(U, V)}

[mikeshulman]

Changing the definition of quotient to

    Private Inductive quotient {sR: is_mere_relation _ R@{U V}} : Type@{max(U, V)} :=
    | class_of : A -> quotient.

gives me a universe inconsistency.

[mattam82]

We should investigate why the uses provoke an inconsistency in V.v. I suppose this could be due to the absence of the implicit resizing with this new definition.

[Alizter]

The solution we seem to be taking now is to have a very small collection of HITs where we are very explicit about the universes. Since we are generally inclined to define new HITs in terms of these old HITs I would say this solves our universe issue, at least partially.

There are of course questions such as: Which HITs can I write in terms of the ones we have defined? I don't think anybody has a good answer for this yet, apart from on a case by case basis. Ultimately, I think it is unrelated to this issue.

Given that we implement HITs as a "hack" I wouldn't be surprised if universe levels are inconsistent. Until coq has native HITs, whatever they may be, I don't think this issue can really be resolved.

@mikeshulman What do you think?

[mikeshulman]

It seems that we are now able to ensure that our HITs live in the correct universes at least in the "basic" cases, so there should be no inconsistencies (absent bugs in Coq). I suggest we perhaps add a bit of documentation on how to make sure this works with future basic HITs that may be defined, and then close this issue.

[mikeshulman]

Actually I'm not sure any more that this issue was fixed by #1105. We now have V.v working with the new Quotient, and the new Quotient has the right universes, but it's still not clear that V itself has the right universes.

[mikeshulman]

In particular, if the definition of setext is annotated with universes like so:

Axiom setext : forall {A B : Type@{U}} (R : A -> B -> hProp@{U})
  (bitot_R : bitotal R) (h : SPushout R -> V),
set@{U' U} (h o (spushl R)) = set (h o (spushr R)).

(which I think is correct), then the definition of setext' fails with a universe mismatch. So in order to fix this I think we really do need to solve HoTT/book#724. The obvious hope is to use bisimulation instead of equality in V. But currently, we use the modified induction principle V_ind' to define the bisimulation, so this isn't completely trivial.