Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
There's a short description of our HoTT version of the Milnor construction of projective spaces for any $\infty$-group in these talk notes. We thought a bit about using the Schubert calculus to define at least the types SU(n), but one really wants the deloopings. It's still an open problem to define the delooping BSU(2), or any other delooping of $S^3$, in Book HoTT. Egbert has a different approach using $\infty$-equivalence relations, but no construction yet. I like Mike's cohesive approach as the most elegant way.
@NoahSchweber maybe I'm not understanding the first question correctly, but don't Lawvere theories give you exactly what you want? First, we can take any algebraic theory and form its Lawvere theory, then its topological algebras are the finite product preserving functors into Top. You also mention Adams' theorem, the setting of which would be homotopy-coherent algebras (i.e., laws are only satisfied up to coherent higher homotopies) and these are modeled by $(\infty,1)$-finite product preserving functors into $\infty$Gpd. (But Lawvere theories are then generalized to the $\infty$-setting.)
In Gambino's thesis he does sheaf interpretation in two steps: first for presheaves and then for a local operator, so the first step is like Kripke models. It is not very topos-theoretic. The work is also interesting as it works for CZF. cs.le.ac.uk/people/ngambino/Publications/thesis.pdf
I couldn't find a freely accessible document defining the $ID_\nu$ systems, so I put a definition on the nLab here. See also the references recorded therein.
Sure: take something like F(O) = PRA + PR-TI(O), where PR-TI(O) expresses transfinite induction along O for primitive recursive predicates. There are of course many variations, according to which predicates you assert transfinite induction for, and which base theory you use.
I also can't find it in the paper, but your guess is very plausible: I would call the critical $\varepsilon$-numbers the ordinals of the form $\varphi(2,\alpha)$. For your other question: I personally have never seen the notation $\kappa_\alpha$ for a countable ordinal that I recall (and I've looked at a fair bit of proof-theoretical literature).
I'm not quite sure what your question is, but you should certainly have a look at Garner's, Understanding the small object argument: arxiv.org/abs/0712.0724
OK, I'll try (I'm beginning to have small doubts myself, but let's see): I'll use the ND-interpretation. Let G=$\forall x\exists y \psi(x,y)$ be Goodstein's theorem in $\Pi^0_2$-form. If PA+Con(ZFC) proves G, then there is (by the ND-theorem) a primitive recursive functional $f$ such that PA+Con(ZFC) proves $\forall x \psi(x,f(x))$. But there can be no such $f$. That should do it, but it's getting late here and I may be missing something.
By the above remark on the ordinal analysis of PA (or Dialectica interpretation). Specifically, this analysis of the provable $\Pi^0_2$-sentences also applies to PA+Con(ZFC).
Well, let T denote PA+Con(ZFC). Then T interprets ZFC, so if T is consistent, so is ZFC, so T is stronger in consistency than ZFC. However, ZFC proves Goodstein's theorem, but PA does not.
Oh, sorry, you should pick T with more arithmetical sentences, say ZFC. PA+Con(ZFC) is stronger than ZFC in consistency-strength, but ZFC has much more of true arithmetic.
@JoelDavidHamkins; what counts as “natural”? :) If you can come up with a “natural” true $\Pi^0_1$-sentence $\varphi$ that proves Con(T) for some T stronger than PA in consistency-strength, then PA+$\varphi$ would be a “natural” counterexample based on PA.
Joel David Hamkins, I don't know about ZFC, but for theories for which we have ordinal analyses (or, say, functional interpretation), we can typically add any set of true $\Pi^0_1$-sentences without changing the provably recursive functions ($\Pi^0_2$-sentences).
