As for (2): The argument you refer to doesn't make much sense to me, since $\sigma$ is not interpreted as a fibration, so why does the question arise as to whether it has a section? That's why I suggested there might be some confusion going on – although I'm probably also confused :-)

I agree it's an incredible kind of reasoning - that's part of the fun! And you're right that to give a full unpacking we have to interpret Type by a univalent universe, $U$, with corresponding fibration $\Sigma_{A:U} T(A)\to U$ (universe a la Tarski with decoding $T$). And then nat_rect is represented by a section of a certain fibration with base space $\text{Map}(\text{nat},U)$. But it's frankly easier to understand in the type-theoretic notation, remembering to understand constructs constructively/continuously.

A thorough answer to this question will be quite long. In the meantime, may suggest section 4 of John R. Longley's survey, Notions of Computability at Higher Types I, [homepages.inf.ed.ac.uk/jrl/Research/notions1.pdf] ?

Just for reference: In other contexts, completion with respect to a family of ideals does occur, where one takes the directed system of finite (possibly repeated) products of ideals in the family, and then takes the limit of the resulting diagram. This nicely generalizes the completion wrt a single ideal.

@Noldorin: When developing a proof system, you might have an intended model in mind, but you don't necessarily have to say anything about semantics. You might even want to allow for several intended models (e.g., a full set theoretical one and a computable one). For systems with a minimum of strength there will always be non-standard models (incompleteness). Henkin semantics is just a way to get completeness by allowing all possible models. Therefore, it is circular to have Henkin semantics in mind during the design of a system ("I want just those models I'll end up with!").

@Noldorin: I think you're right that those table rows are a bit misleading. Perhaps the meaning is that a logic is a "higher-order type theory" if there is a type for propositions, so that the logic embeds in the types. Otherwise, the logic is built on top of the type theory. But if so, then Agda and others should have been included in that category. A more interesting comparison would be according to the features of the type theory: predicative/impredicative, extensional?, polymorphic?, dependent?, and so on.

@Noldorin: I don't know of short summary, but with a constructive system you can in principle extract witnesses to existential statements and computable functions for $\forall\exists$-statements and so on. However, constructive and classical logic can be interpreted in each other, so in that sense they're equivalent. And for instance both Coq and Isabelle/HOL allow program extraction from constructive proofs.

@Noldorin: Concerning constructive/classical logic: both are used, with for example Coq being popular for constructive reasoning (though also supporting classical logic), while the various HOL systems are popular for classical reasoning.

For an overview of the different provers, you might like Freek Wiedijk's "Comparing mathematical provers", cs.ru.nl/~freek/comparison/diffs.pdf John Harrison's book, "Handbook of Practical Logic and Automated Reasoning", contains the description of an interactive theorem prover in the LCF style. The code is available online: cl.cam.ac.uk/~jrh13/atp/index.html