New answers tagged

1 vote

Adding type constructors to universes

$Γ.\mathrm{El}(a) ⊢ U\ \mathrm{type}$ is valid because $Γ ⊢ U\ \mathrm{type}$ is valid for all $Γ$. Just pick $Γ.\mathrm{El}(a)$ as the context. For one, there is no reason to have the $a$ in that ...
Dan Doel's user avatar
  • 2,687

Top 50 recent answers are included