Mike Shulman
Mike Shulman
(Im)predicativity, in the sense relevant here (i.e. propositional resizing), is mentioned in section 3.5. I just meant it hadn't been mentioned yet in the introduction, which is where this comment...
1. You're right, it should be "is an n-type". 2. This follows from the commutation of truncations with loop-spaces, Corollary 7.3.14: $\pi_k(\Vert A\Vert_n ) = \Vert \Omega^k (\Vert A\Vert_n) \Vert_0...
If you don't mind, I'm going to reopen it because (1), at least, is a typo that should be fixed.
Do you mean to say that KP isn't "predicative" because it is classical? I think a theory can be both predicative and classical, since without function-sets you can't construct impredicative...
What do you think of my proposed solution with the footnote?
What if the footnote says "more precisely 'predicative', which includes some theories with classical logic"?
Also the word "representatives" is perhaps a bit misleading to use at all because with this approach we are *not* selecting canonical "representatives of equivalence classes" for isomorphism of sets...
How would `Asai.Tty.Make` work then?
I suppose that's all it could do. But I'd want the same code to be able to deal with both textual and graphical terms, so my Range module would include...