On Monday, October 16, 2017 at 11:01:13 AM UTC-4, Michael Shulman wrote:

On Mon, Oct 16, 2017 at 5:30 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> 1. The addition of universes is an open problem. Basically the logical
> strength of the theory goes up and the proof of Harper and Pfenning
> needs to be redone. (They exploited the fact that LF doesn't have
> large eliminations to do a recursion on the size of the type.)
>
> I would be rather surprised if this couldn't be made to work, though.

Me too.

I was thinking that where you'd really get in trouble is with impredicative quantifiers. From what I understand, hereditary substitutions are a variant of cut elimination, which can't directly handle impredicativity. But so far, HoTT has added impredicativity with an axiom, so maybe it'll work out somehow. Like HoTT's proof-theoretic strength would be impredicative, but its "coherence strength" would still be predicative in some weird sense. That would be a bit unnatural though, in my opinion.