Library Coq.Logic.SetIsType
The Set universe seen as a synonym for Type
 
 After loading this file, Set becomes just another name for Type.
    This allows easily performing a Set-to-Type migration, or at least
    test whether a development relies or not on specific features of
    Set: simply insert some Require Export of this file at starting
    points of the development and try to recompile...  
 
Notation "'Set'" := 
Type (
only parsing).