[logic-ml] intuitionistic type theory and inaccessible cardinals