The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

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