"Sets in Types, Types in Sets" establishes that the calculus of constructions is bi-interpretable with ZFC + infinitely many inaccessibles.
Are there any more results like this higher up the large cardinal hierarchy? What would a type theory capable of expressing stronger large cardinal properties look like? (without just jamming them in as axioms via Sets in Types)