<p><span class="h-card" translate="no"><a href="https://types.pl/@ionchy" class="u-url mention">@<span>ionchy</span></a></span> types that depend on types r the pis but `Type` is the Kind of all types (it's predicative so there's like an explicit universe jump as far as i understand)</p><p>but i seee what u mean thank u !! that makes a lot more sense</p>
