FunextAxiom gives Universe inconsistency

[spitters]

I am getting a Universe Inconsistency in my development. Error: Universe inconsistency (cannot enforce HoTT.FunextAxiom.12 = Top.3367 because Top.3367 <= Top.3368 < HoTT.FunextAxiom.12).

I would imaging we want to make FunextAxiom polymorphic with Set Universe Polymorphism.

[mikeshulman]

If doing that fixes your problem, go for it!

[peterlefanulumsdaine]

I’m slightly confused — I’d thought that universe polymorphism was on by default now? But if not, then indeed go for it!

[spitters]

So am I. Turning it on it one place does not seem to solve the problem. Were any of the changes in to universe polymorphism documented already? If have seen the theoretical background slides by Matthieu, but don't recall seeing more technical documentation, i.e. which commands to type.

Apparently, just changing it in for FunExt does not solve my problem.

On Thu, Mar 21, 2013 at 9:50 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

I’m slightly confused — I’d thought that universe polymorphism was on by default now? But if not, then indeed go for it!

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15239437 .

[barras]

I think Matthieu insisted that Axioms be monomorphic, even when the option is set. Possibly, using Polymorphic Axiom instead of Axiom will do it. Otherwise, this gives a point to generalizing the axioms used. As a last resort, one could duplicate the axiom to (maybe) get out of the universe inconsistency, but then one will have polymorphic definitions constrained by two monomorphic universes... Not so nice.

[peterlefanulumsdaine]

Huh — that seems surprising; axioms seem like a very natural thing to want polymorphic. Was there some particular theoretical concern that argued for making them monomorphic by default?

[spitters]

As far as I can see it the conflicting terms may be: funext_axiom, apD10, isequiv_apD10

I made the following changes.

Polymorphic Axiom funext_axiom : Funext. Polymorphic Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) Polymorphic Class Funext := Polymorphic Context `{univalence_axiom : Univalence}.

Still no luck. It would be nice not to have to guess what is going on. Is there any documentation?

On Thu, Mar 21, 2013 at 11:11 AM, barras notifications@github.com wrote:

I think Matthieu insisted that Axioms be monomorphic, even when the option is set. Possibly, using Polymorphic Axiom instead of Axiom will do it. Otherwise, this gives a point to generalizing the axioms used. As a last resort, one could duplicate the axiom to (maybe) get out of the universe inconsistency, but then one will have polymorphic definitions constrained by two monomorphic universes... Not so nice.

— Reply to this email directly or view it on GitHub.

[JasonGross]

Do you have an example of code that causes this?

I don't know of any documentation, but I've run into problems where putting Polymorphic in front of everything in my development (https://bitbucket.org/JasonGross/catdb/commits/branch/polymorphic) did not get rid of all of my universe inconsistencies (and in fact had universe inconsistencies which were not present when compiled with Coq 8.4). Matthieu says that he's working on a better version (see https://github.com/HoTT/coq/issues/20#issuecomment-14444355).

[spitters]

I think that when we Instantiate an instance of the funext axiom, a universe level is fixed. Since we decide, we do not want to use type classes to track the universe dependencies, I started to remove all instances of `{funext}.

[mattam82]

There is no documentation yet. Set Printing Universes + Print foo should give you everything you need though. Axioms are not polymorphic, but this an overlook, the ones that I didn't want to make polymorphic are the local variables. In: Section Foo. Variable A : Type. ...

You don't expect A to be generating a new level at each occurrence. Making these variables polymorphic would be a huge change of representation also.

Still working on a better version...

[spitters]

I think that when we Instantiate an instance of the funext axiom, a universe level is fixed. Since we decided, we do not want to use type classes to track the universe dependencies, I started to remove all instances of `{funext}.

On Fri, Mar 22, 2013 at 6:51 AM, Matthieu Sozeau notifications@github.comwrote:

There is no documentation yet. Set Printing Universes + Print foo should give you everything you need though. Axioms are not polymorphic, but this an overlook, the ones that I didn't want to make polymorphic are the local variables. In: Section Foo. Variable A : Type. ...

You don't expect A to be generating a new level at each occurrence. Making these variables polymorphic would be a huge change of representation also.

Still working on a better version...

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15290754 .

[andrejbauer]

Wait wait, before you go off doing something like "remove all instances of `{funext}", is this really necessary? Personally it does not bother me at all.

[spitters]

We decided not to use type classes to keep track of dependencies, but instead use Print Assumptions. The `{funext} look ugly.

It does seem to matter, my universe inconsistency just got one shorter :-S

On Fri, Mar 22, 2013 at 9:15 AM, Andrej Bauer notifications@github.comwrote:

Wait wait, before you go off doing something like "remove all instances of `{funext}", is this really necessary? Personally it does not bother me at all.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15295840 .

[mikeshulman]

What do you mean by 'we decided'? I thought we decided precisely to use typeclasses for axioms. On Mar 22, 2013 9:24 AM, "spitters" notifications@github.com wrote:

We decided not to use type classes to keep track of dependencies, but instead use Print Assumptions. The `{funext} look ugly.

It does seem to matter, my universe inconsistency just got one shorter :-S

On Fri, Mar 22, 2013 at 9:15 AM, Andrej Bauer notifications@github.comwrote:

Wait wait, before you go off doing something like "remove all instances of `{funext}", is this really necessary? Personally it does not bother me at all.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15295840> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15296235 .

[mikeshulman]

If the problem really is due to the Axioms, then maybe a better solution would be to rethink Peter's proposal and get rid of FunextAxiom, asking everyone to parametrize over a witness instead. On Mar 22, 2013 9:57 AM, "Michael Shulman" viritrilbia@gmail.com wrote:

What do you mean by 'we decided'? I thought we decided precisely to use typeclasses for axioms. On Mar 22, 2013 9:24 AM, "spitters" notifications@github.com wrote:

We decided not to use type classes to keep track of dependencies, but instead use Print Assumptions. The `{funext} look ugly.

It does seem to matter, my universe inconsistency just got one shorter :-S

On Fri, Mar 22, 2013 at 9:15 AM, Andrej Bauer notifications@github.comwrote:

Wait wait, before you go off doing something like "remove all instances of `{funext}", is this really necessary? Personally it does not bother me at all.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15295840> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15296235 .

[spitters]

We discussed Peter's option: (2): ensure that all files assuming the axiom have a single common ancestor assuming it, so that they share the same witness.

I may have gone further and concluded that we do not need type classes

for this anymore, because Yves suggested:

Coq provides a tool to let you know what axioms you rely on : "Print Assumptions". Why not use axioms and invoke that tool when we want if

a given proof relies on axioms?

And finally Steve concluded:

I don't think anyone is trying to "prove univalence", nor are we exploring the limits of homotopy in non-univalent type theory. We are using UA and function extensionality freely.

Doing without them would be a different program, but not univalent foundations.

On Fri, Mar 22, 2013 at 9:57 AM, Mike Shulman notifications@github.com wrote:

What do you mean by 'we decided'? I thought we decided precisely to use typeclasses for axioms. On Mar 22, 2013 9:24 AM, "spitters" notifications@github.com wrote:

We decided not to use type classes to keep track of dependencies, but instead use Print Assumptions. The `{funext} look ugly.

It does seem to matter, my universe inconsistency just got one shorter :-S

On Fri, Mar 22, 2013 at 9:15 AM, Andrej Bauer notifications@github.comwrote:

Wait wait, before you go off doing something like "remove all instances of `{funext}", is this really necessary? Personally it does not bother me at all.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15295840> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15296235 .

— Reply to this email directly or view it on GitHub.

[mikeshulman]

No, the conclusion was to supply the axiom files in case users don't want to explicitly parametrize over witnesses to the axioms. Our library itself still should. On Mar 22, 2013 10:06 AM, "spitters" notifications@github.com wrote:

We discussed Peter's option: (2): ensure that all files assuming the axiom have a single common ancestor assuming it, so that they share the same witness.

I may have gone further and concluded that we do not need type classes

for this anymore, because Yves suggested:

Coq provides a tool to let you know what axioms you rely on : "Print Assumptions". Why not use axioms and invoke that tool when we want if

a given proof relies on axioms?

And finally Steve concluded:

I don't think anyone is trying to "prove univalence", nor are we exploring the limits of homotopy in non-univalent type theory. We are using UA and function extensionality freely. Doing without them would be a different program, but not univalent

foundations.

On Fri, Mar 22, 2013 at 9:57 AM, Mike Shulman notifications@github.com wrote:

What do you mean by 'we decided'? I thought we decided precisely to use typeclasses for axioms. On Mar 22, 2013 9:24 AM, "spitters" notifications@github.com wrote:

We decided not to use type classes to keep track of dependencies, but instead use Print Assumptions. The `{funext} look ugly.

It does seem to matter, my universe inconsistency just got one shorter :-S

On Fri, Mar 22, 2013 at 9:15 AM, Andrej Bauer < notifications@github.com>wrote:

Wait wait, before you go off doing something like "remove all instances of `{funext}", is this really necessary? Personally it does not bother me at all.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15295840> .

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15296235> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15298289 .

[spitters]

Here is an explicit bug:

Theorem equiv_induction (P : forall U V, U <~> V -> Set) : (forall T, P T T (equiv_idmap T)) -> (forall U V (w : U <~> V), P U V w). Proof. intros H???. apply (@equivrect _ (@equivpath U V) ). intro x. destruct x. apply H. Defined. Check (@equiv_induction (fun (U:Set) (V:Set) w => Unit)). Error: Found type "Set" where "Type" was expected.

While if we add explicit casts to the first line: Theorem equiv_induction (P : forall (U:Set) (V:Set), U <~> V -> Set)

Coq is happy.

It is yet unclear to me whether this is orthogonal to the problem I got with funext.

[peterlefanulumsdaine]

Like Mike, I also thought we agreed to keep Funext assumptions local in the library, while providing the option to assume it globally for users of the library.

The polymorphism issues, I think, strongly confirm that we’re doing the right thing in the library. However, I’m still somewhat in favour of encouraging providing the axioms, albeit with a caveat about polymorphism until we (hopefully) work out how to make them polymorphic (for more on which see below).

Re my earlier question on why axioms are monomorphic: I think I understand this a bit now. While thinking of them as axioms makes poly seem natural, they’re of course just the same as variables, and from that point of view it seems more natural to have them mono; and I could imagine there might even be theoretical complications in trying to make them poly.

This is kind-of confirmed by a bit of mucking around — see here for the things I tried, and the code for testing whether it really is polymorphic: https://gist.github.com/peterlefanulumsdaine/7e599d3ecc917fa5a49d Basically, as far as I can find, there’s no way to make a polymorphic global assumption — Axiom, Variable, Parameter, etc, all appear to produce monomorphic things, even if one asks for Polymorphic Axiom, etc. Or rather, there does seem to be one way that works:

Definition funext_axiom : Funext.
  admit.
Defined.

but I think this may actually be a bug (or should I say “exploit”), since it produces a polymorphic definition funext_axiom, defined as equal to an opaque assumption funext_axiom_admitted, and this assumption is itself monomorphic! So I don’t know we should maybe use this as a temporary measure, or just accept for the meantime that if we want to be polymorphic, we need to use local assumptions or -warn-universe-inconsistency.

I’d be interested to hear Mathieu’s take on all this; on the other hand, he said he was working on rewriting the whole of how polymorphism works and hoped to have it out soon, so maybe from his point of view all these questions are obsolete now :-)

[spitters]

Thanks for investigating this! I see I should have pushed a bit further. I propose to use the exploit for now. Is it OK to put this in the library, temporarily? It will allow me to check in my work on the object classifier.

On Sat, Mar 23, 2013 at 12:31 PM, Peter LeFanu Lumsdaine notifications@github.com wrote:

Like Mike, I also thought we agreed to keep Funext assumptions local in the library, while providing the option to assume it globally for users of the library.

The polymorphism issues, I think, strongly confirm that we’re doing the right thing in the library. However, I’m still somewhat in favour of encouraging providing the axioms, albeit with a caveat about polymorphism until we (hopefully) work out how to make them polymorphic (for more on which see below).

Re my earlier question on why axioms are monomorphic: I think I understand this a bit now. While thinking of them as axioms makes poly seem natural, they’re of course just the same as variables, and from that point of view it seems more natural to have them mono; and I could imagine there might even be theoretical complications in trying to make them poly.

This is kind-of confirmed by a bit of mucking around — see here for the things I tried, and the code for testing whether it really is polymorphic: https://gist.github.com/peterlefanulumsdaine/7e599d3ecc917fa5a49d Basically, as far as I can find, there’s no way to make a polymorphic global assumption — Axiom, Variable, Parameter, etc, all appear to produce monomorphic things, even if one asks for Polymorphic Axiom, etc. Or rather, there does seem to be one way that works:

Coq Definition funext_axiom : Funext. admit. Defined.

but I think this may actually be a bug (or should I say “exploit”), since it produces a polymorphic definition funext_axiom, defined as equal to an opaque assumption funext_axiom_admitted, and this assumption is itself monomorphic! So I don’t know we should maybe use this as a temporary measure, or just accept for the meantime that if we want to be polymorphic, we need to use local assumptions or -warn-universe-inconsistency.

I’d be interested to hear Mathieu’s take on all this; on the other hand, he said he was working on rewriting the whole of how polymorphism works and hoped to have it out soon, so maybe from his point of view all these questions are obsolete now :-)

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Bas, does the stuff you want to check in not work with local assumptions instead of axioms?

[spitters]

You mean adding another axiom Funext2, locally in the file, I doubt it, but I could try ?

On Sat, Mar 23, 2013 at 8:30 PM, Mike Shulman notifications@github.comwrote:

Bas, does the stuff you want to check in not work with local assumptions instead of axioms?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15348904 .

[mikeshulman]

No, I mean

Section AssumeFunext.
Context `{Funext}.

[peterlefanulumsdaine]

How about we ask Mathieu? If he says polymorphic axioms/variables are just around the corner, then it seems fine to me to add the exploit to the library for now — no need for Bas to change his code from the style he prefers. If there’s some technical difficulty with polymorphic axioms and they’re not coming in the foreseeable future, then I’m not sure what I feel — I guess probably taking the axiom files out for now?

On Sat, Mar 23, 2013 at 8:54 PM, Mike Shulman notifications@github.comwrote:

No, I mean

Section AssumeFunext. Context `{Funext}.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15349157 .

[mikeshulman]

Bas, is the code you want to check in to be added to the library itself, or in a separate dependent development? On Mar 23, 2013 11:57 PM, "Peter LeFanu Lumsdaine" notifications@github.com wrote:

How about we ask Mathieu? If he says polymorphic axioms/variables are just around the corner, then it seems fine to me to add the exploit to the library for now — no need for Bas to change his code from the style he prefers. If there’s some technical difficulty with polymorphic axioms and they’re not coming in the foreseeable future, then I’m not sure what I feel — I guess probably taking the axiom files out for now?

On Sat, Mar 23, 2013 at 8:54 PM, Mike Shulman notifications@github.comwrote:

No, I mean

Section AssumeFunext. Context `{Funext}.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15349157> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15351055 .

[mattam82]

Indeed, they're just around the corner, there's no technical difficulty with them. Also the admit trick shouldn't work, because it adds an axiom and hence fixes the polymorphic universes. It's a bug.

[spitters]

I think it should go into the library itself, they are basic constructions.

On Sun, Mar 24, 2013 at 12:30 AM, Mike Shulman notifications@github.comwrote:

Bas, is the code you want to check in to be added to the library itself, or in a separate dependent development? On Mar 23, 2013 11:57 PM, "Peter LeFanu Lumsdaine" < notifications@github.com> wrote:

How about we ask Mathieu? If he says polymorphic axioms/variables are just around the corner, then it seems fine to me to add the exploit to the library for now — no need for Bas to change his code from the style he prefers. If there’s some technical difficulty with polymorphic axioms and they’re not coming in the foreseeable future, then I’m not sure what I feel — I guess probably taking the axiom files out for now?

On Sat, Mar 23, 2013 at 8:54 PM, Mike Shulman notifications@github.comwrote:

No, I mean

Section AssumeFunext. Context `{Funext}.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15349157> .

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/HoTT/issues/99#issuecomment-15351055> .

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/99#issuecomment-15351345 .

[mikeshulman]

Well, then it should probably follow the library convention of explicit parametrization rather than axioms anyway.

[JasonGross]

Is it too cumbersome to separate the file into multiple sections, each with its own funext variable, or to stick `{Funext} in each construction, rather than in the section context? (I believe that variables in sections get the same universe-levels across all the functions defined in that section.)

(On the other hand, if there's a problem with universe polymorphism inside a single construction, then the only thing I can think of is to have two funext parameters, and to explicitly use them separately.)

[spitters]

Universe Polymorphism now works much better. I am closing this.