What is known, and what is published, on the reverse mathematics of the nest of results called Hilbert's Theorem 90?
[Math] Reverse mathematics of Hilbert’s Theorem 90
lo.logicnt.number-theoryproof-theoryreverse-math
Related Solutions
Before I attempt to address your specific questions, let me give a thought provoking non-answer:
Reverse mathematics is impossible (and irrelevant) in HoTT!
This is because HoTT fully supports proof-relevant mathematics, so when you refer to a theorem you necessarily refer to a proof of that theorem. The question whether the hypotheses are necessary doesn't make sense in this context since the hypotheses are part of the theorem itself!
Now that your thoughts have been provoked, let me amend the above statement:
HoTT is not the end of reverse mathematics!
Actually, it just makes the reverse (and constructive) mathematics questions even more obvious. The most fundamental reason why reverse mathematics exists is the incredible power of the existential quantifier. In HoTT, that is immediately obvious. A plain existential statement is interpreted as a dependent sum type in HoTT: "$\sum_{x:A} P(x)$ is inhabited" is the right way to say that "there is an $x$ of type $A$ such that $P(x)$." By definition, every inhabitant $x:A$ of this type is equipped with a justification of $P(x)$. To get the usual existential quantifier, one must truncate $\sum_{x:A} P(x)$ to a proposition. This raises the question: can this truncation be reversed? What are the necessary hypotheses to reverse this truncation? This is what reverse mathematics questions get turned into when translated into the language of HoTT. Note how "mathematical" the reverse mathematics question has become! This is no surprise to practicing reverse mathematicians but it is very interesting how reverse mathematics becomes less mythical in this context.
I will now add what I know about each of your questions. Since I'm still learning about HoTT, these answers are far from complete or definitive. I hope that experts will chime in at some point.
The above sort of addresses this question. An additional difficulty is that it seems that there is still some work to be done in understanding models of HoTT. The soundness and completeness theorems obtained by Awodey & Warren and Gambino & Garner are almost there but Awodey points out some subtle issues. I don't know if these issues are problematic enough to make it difficult to establish non-provability results for HoTT.
HoTT is perhaps too strong for use as a base system for classical reverse mathematics. The reason is basically the same as why ZF is often too strong for that purpose. Note, however that even ZF is not completely useless. For example, as witnessed by a great deal of literature, ZF is a perfectly fine base theory for the analysis of choice principles. HoTT is more promising as a base system for constructive reverse mathematics but the constructivity of the univalence axiom is currently an open problem.
I don't think the univalence axiom is that problematic. The law of excluded middle always clashes with the propositions-as-types interpretation. The correct way to formulate the law of excluded middle in HoTT is to restrict it to propositions — types with at most one element. This version of the law of excluded middle does not clash with univalence and captures all of the normal uses.
I don't think anyone has addressed the question whether HoTT is a conservative extension of BISH (say) or how far it is from being a conservative extension.
It's difficult to make a comparison. The base system RCA0 was explicitly designed to capture basic computability theory. HoTT wasn't designed that way but other aspects of computability were important design components.
I don't see much gain in using proof assistants for reverse mathematics but I might be nearsighted.
Yes, some additional axioms such as propositional resizing, the law of excluded middle, and the axiom of choice have been analyzed to some extent. HoTT is so young that very little of this has been done yet.
Reverse math usually means work in subsystems of arithmetic. That goes a bit beyond analysis---Simpson's book has plenty of classic results from the theory of countable groups, rings, and fields, and much of the more recent focus in the area has been countable combinatorics. But all of these are basically about sets of natural numbers and things those can code.
As a sociological matter, addressing the same question with deeply different base theories usually isn't called reverse math. For instance, one could argue that Shelah's proof of the independence of the Whitehead problem is in some sense a result in reverse math (or at least, that a stronger result showing the equivalence of the Whitehead problem with ZFC plus some additional axiom would be), but that's not how people usually use the term: determining what can be proven in extensions of ZFC is a branch of set theory, not reverse math. Similarly, there's work on what can be proven in very weak theories of arithmetic (like arithmetic with only bounded quantifiers), but that usually doesn't get called reverse math either.
So I think most people would think that those geometric aren't quite in the field called "reverse mathematics", as it's currently understood, but are closely related results which belong to the broader philosophical umbrella which spawned reverse math.
Best Answer
It is provable in RCA0 that if $K$ is a finite Galois extension of $F$ with Galois group $G$ then $H^1(G,L^\times)$ is trivial (every cocycle $a:G \to L^\times$ is a coboundary).
The finite Galois theory in RCA0 was discussed by Friedman, Simpson and Smith in Countable algebra and set existence axioms [APAL 25 (1983), 141–181; MR0725732]. The executive summary is that finite Galois theory works fine in RCA0.
The usual proof of Theorem 90 works in RCA0. The linear independence of characters is provable using only $\Sigma^0_1$-induction since one can check linear dependence by testing at a fixed finite basis of $L$ over $K$. It follows that if $a:G \to L^\times$ is a cocycle then there is a $x \in L^\times$ such that $y = \sum_{\sigma \in G} a(\sigma)\sigma(x)$ is nonzero. Standard algebraic manipulations then show that $a(\sigma) = y/\sigma(y)$, i.e. $a$ is a coboundary.
Infinite Galois extensions are more subtle as discussed in my paper with Jeff Hirst and Paul Shafer. For Theorem 90, it seems that the issue is a definitional one more than anything else.
If $K$ is an infinite Galois extension of $F$ such that $F$ is a subset of $K$ (as opposed to being merely embeddable in $K$) then the Galois group $G$ of $K$ over $F$ is a separably closed subgroup of permutations of $K$. Then $G$ can be represented as a complete separable metric space in the usual manner and one can make sense of the idea of a continuous cocycle $a:G \to L^\times$. In that scenario, RCA0 does prove that $H^1(G,L^\times)$ is trivial since every continuous cocycle is a lifting of a cocycle from a finite Galois subextension.
In the general case where $F$ is merely embeddable in $K$, several issues arise. Galois theory still makes sense over WKL0 but the Galois group $G$ is not necessarily separably closed. It is unclear what a continuous cocycle would be in that case. So the main issue is to define $H^1(G,L^\times)$ before proving anything about it. Note that this case is impossible in ACA0 since we can always comprehend the range of an embedding. So, assuming ACA0, $H^1(G,L^\times)$ is always well defined and always trivial.