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 
> <neelaka...@gmail.com <javascript:>> 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.