排中律(law of excluded middle)は任意の階数\(i\)と型\(P:\mathcal {U}(i)\)に対して、\(P\)が命題ならば\(P\lor \neg P\)が真であることを要請する。