Universe Polymorphism Issue

[td202]

Context

Using the HoTT library, it is difficult to construct IsHSet instances for composite types involving nat. There seem to be a couple of contributing factors:

• nat is at type Set whereas other basic types (e.g. Unit and Empty) are at Type1 (which is a higher universe).
• the universe polymorphism is insufficiently polymorphic.

Consider:

Lemma hset_nat_plus_Unit : IsHSet (nat + Unit).
  refine (@hset_sum _ _ _ _). (* Fails *)

This code fails because hset_sum expects the type of nat to be at least Type1 (effectively).
This suggests the following alternative:

Lemma hset_nat_plus_Unit : IsHSet ((nat:Type1) + Unit).
  refine (@hset_sum _ _ _ _).
  (* Goal: ISHSet nat *)
  exact hset_nat. (* Fails *)

The problem here seems to be that hset_nat considers nat at type Set, but what is needed is nat at type Type1. I would expect the universe polymorphism to support this.

Example

Here is an example that illustrates the issue:

Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
Inductive Unit : Type1 := tt : Unit.
Inductive A : Type := a : A | b : A.
Definition P (A : Type) := Unit.
Definition foo : P A := tt.
Lemma bar : P (A : Type1).
  exact foo. (* Fails with universe inconsistency *)

In HoTT, or in Coq (8.5beta2) with the definitions of P and foo polymorphic, this fails. In Coq without the definitions being polymorphic, it works. (Maybe this is more of a Coq issue than a HoTT issue?)

[mikeshulman]

Probably related to #754, #774.

[mattam82]

Hi, your example should not fail as P@{Top.1} (A : Type1) and P@{Set} A (note that A : Set) both reduce to Unit. It did in 8.5beta2 but doesn't in the current 8.5 branch, this was a bug. In your original problem, you expect IsHSet@{i} to be coercible to IsHSet@{j} with i < j. The universe system does not support this currently and you have to use an explicit coercion there. We are working on extending cumulativity to inductive so that this is indeed accepted.

[spitters]

Coq trunk now has cumulative inductive types.
coq/coq@4148906

[Alizter]

Seems to work now, therefore I am closing this issue. If you still have a problem, feel free to open.