The Coq mailing list

[darktenaibre <darktenaibre AT isomorphis.me>]

On 07/17/2017 05:54 PM, Gaetan Gilbert wrote:
> If one proves [forall A B : Type@{i}, A = B :> Type@{j} -> A = B :> 
> Type@{k}] in the obvious destruct/reflexivity way there is a 
> constraint [j <= k].
>
> Does anyone know of a way to prove it without generating this constraint?
>
> (there are also constraints i <= j and i <= k but those are expected)
It looks likely to me that it is illegal to derive this with j = 1 and k 
= 0. I can imagine models in which it is validated (e.g. 
set-theoretical, or even syntactic ones which identify the "type-free" 
syntax), but probably counter-models as well. I think a syntactic model 
a la Tarski ought to invalidate this.

Another way to invalidate it could be to take this kind of approach 
(https://www.xn--pdrot-bsa.fr/articles/cpp2017.pdf), where I think one 
should be able to introduce junk at Type0 unobservable at Type1 using a 
mild variation of what happens at section 5 with a non-uniform 
translation of universes (translating "Type0" as "Type0 * bool" and 
"Type1" as "Type1"; I haven't checked this in details, so it might be 
wrong).