The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

What error message do you get if you do [into H; pose (H : @peq@{Set} Type@{Set} T1 T2).]?  In particular, which universe variable is it refusing to minimize, and why?  (My approach to [Set] with universe polymorphism is mostly "don't use it".  Note that [@eq Type@{i} A B -> @eq Type@{j} A B] does not hold for [i > j], but you don't run into these other problems, which are generally a result of Coq refusing to minimize some universes to Set (allowing minimization in these cases has resulted in even more issues, sometimes in cases where [Set] was not explicitly mentioned, so Mathieu chose to forbid some minimizations).)

On Sun, May 8, 2016, 3:24 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 05/08/2016 02:30 PM, Jason Gross wrote:
> It's not provable unless you assume, e.g., univalence.  (The other
> direction, @eq Set S1 S2 -> @eq Type S1 S2, however, is provable in vanilla
> Coq.)  Since Coq is consistent with univalence, it's not possible to have
> two Sets that are @eq Type but provably not @eq Set.  (If you just want two
> that are @eq Type and not provable @eq Set, S1 and S2 in the context of
> your goal after [intros] will do.)  I don't know if there are any models
> which would validate this, but the HoTT mailing list might be a reasonable
> place to ask.  (Under the homotopy interpretation, the idea would be that
> somehow all of the paths between S1 and S2 "go through" types which do not
> live in Set.)
>
> -Jason

Thanks for the quick reply, Jason.

My primary concern is if using certain "more generic" lemmas and tactics
that do things in Type instead of Set is a problem - which it appears to
be (for example, using eq_rect to get a more generic definition, when
eq_rec would suffice for some usages).

I could start using Polymorphic definitions - but it will still be the
case sometimes that I will have a relationship R T1 T2 where T1 and T2
are initially at some higher universe level (such as Type), but reduce
to a lower one (such as Set) at some point.  Which could then break the
intention of R, even if R is polymorphic.

Does Coq have a way to declare universe minimization as a type of
reduction on terms?  Meaning that if I have R T1 T2 where T1 and T2 are
both Types, but reduction/substitution changes this to R S1 S2 where S1
and S2 are both Sets, can some kind of reduction also modify R's
implicit universe arguments?

For example:

Polymorphic Definition peq@{i} {T:Type@{i}}(S1 S2:T) := eq S1 S2.

Variables S1 S2 : Set.
Definition T1 : Type := S1.
Definition T2 : Type := S2.

Goal peq T1 T2 -> @eq Set S1 S2.
cbv.

Even though peq is polymorphic, once the peq term is constructed on T1
T2, the universe level is fixed, and there is no way to prove this goal.

-- Jonathan

>
> On Sun, May 8, 2016 at 2:10 PM, Jonathan Leivent <jonikelee AT gmail.com>
> wrote:
>
>> I'm hitting some problems that I think are related to equalities in
>> different universes.  For example, consider:
>>
>> Goal forall S1 S2:Set, @eq Type S1 S2 -> @eq Set S1 S2.
>>
>> Is this provable in Coq?  If not, then does that mean it is possible to
>> have two Sets in Coq such that they are (@eq Type) but not (@eq Set)?  What
>> would that possibly mean?
>>
>> -- Jonathan
>>
>>
>>