I'm reading about the calculus of construction Nederpelt & Geuvers' book "Type theory and formal proof".
I can see that CoC allows us to extend the curry howard isomorphism from simply typed lambda calculus to full predicate logic. I can see how CoC allows one to do higher order logic in type theory.
But when I think of a "construction", I think of a mathematical, not logical notion, namely the informal idea of "constructing an object from other objects" (e.g. constructing the real numbers from the rationals, or constructing a product topological space from two topological spaces).
Is this latter concept of "construction" actually what the "calculus of constructions" refers to? Is this why it is called that way? I would find this surprising (but interesting), given that CoC by Nederpelt & Geuvers is being presented primarily as a tool to do predicate logic in.
Also, they present a "construction" as a term of e.g. type $*\to *$ (or $Type\to Type$. i.e. it takes a type to a type). But it seems to me that the two examples given above are not examples of this: e.g. the construction of the reals cannot be performed on an arbitrary type, it can only be performed on the rational numbers.