blob: cd8c4ad7dfda46a80a1cd5db977e34d19eba48fa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Set Universe Polymorphism.
Module Type S.
Parameter Inline T@{i} : Type@{i+1}.
End S.
Module F (X : S).
Definition X@{j i} : Type@{j} := X.T@{i}.
End F.
Module M.
Definition T@{i} := Type@{i}.
End M.
Module N := F(M).
Require Import Hurkens.
Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.
|
