Is simply typed lambda calculus with fixed-point combinator Turing-complete? There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the following quote from  Boltzmann Samplers for Closed Simply-Typed Lambda Terms (2017).

Extended with
  a fix-point operator, simply-typed lambda terms can be used as the intermediate
  language for compiling Turing-complete functional languages.

However, I haven't found proof of this statement.
Could you please suggest where I could find the proof or the guideline of how to prove this statement? Thank you.
 A: The simply-typed $\lambda$-calculus with the fixpoint combinator but without a primitive integer type is not Turing-complete, at least not in the usual sense (Church integers and computation as $\beta$-reduction).  This is a consequence of a result of Statman [1], stating that (somewhat surprisingly) termination in that calculus is decidable.
Perhaps what you want is the simply-typed $\lambda$-calculus with a fixpoint combinator and a primitive integer type, together with its constructors (zero and successor) and destructors (ether a single "case" destructor, or if-then-else and predecessor).  This is known as PCF and showing that it is Turing-complete is a straightforward programming exercise (I don't think there is a reference for it in the literature).
[1] Richard Statman. On the lambdaY calculus. Ann. Pure Appl. Logic 130(1-3): 325-337 (2004)
A: Damiano is right, the answer is no: it is not Turing complete.
Supposing to define natural numbers as some type (o->o)->o->o, 
even with fixpoints you cannot define the predecessor (that would be
enough to have equality, and then, by Goedel characterization via
mu-recursion, all computable functions).
In fact, by just adding fixpoints you only get partial polynomials
instead of the total polynomials of the traditional calculus.
This can also be seen by generalizing Schwichtenberg approach
(see e.g. Functions Definable in the Simply-Typed Lambda Calculus)
Instead of normal forms you must consider bohm-trees, now, that have
very limited shapes due to
typing constraints. Head variables in terms are the same as in the
traditional case, and the proof proceeds in a very similar way.
