The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

> Le 23 mai 2019 à 17:04, Burak Ekici 
> <ekcburak AT hotmail.com>
>  a écrit :
> 
> Dear all,
> 
> What exactly the "type-in-type" option is doing? My vague understanding 
> is that it disables universe consistency checks and allows for 
> inconsistent construction of large types. Is that the case? I wonder if 
> it is making Coq inherently inconsistent or just unsafe?

Hi,

It does allow for inconsistent constructions of large types. 
One can easily derive False in this setup by applying a
variant of Hurkens paradox. For example Coq.Logic.Hurkens.TypeNeqSmallType.

Best,
— Matthieu