<p><span class="h-card" translate="no"><a href="https://types.pl/@bhaktishh" class="u-url mention">@<span>bhaktishh</span></a></span> The way I think of it (probably there are better explanations out there): in impredicative type theories you have a universe that can quantify over all type universes; in a predicative type theory, trying to quantify over the type universe puts you one universe higher.</p><p>System F has impredicative quantification. MLTT with Type:Type has impredicative quantification. CoC has impredicative quantification via Prop.</p><p>Whereas MLTT with a strict universe hierarchy is predicative.</p>