The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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