The question is: "From a constructivist viewpoint though, can we ever realize the actual object which is infinite?" Unless you specialize to decidable objects (excluded middle for equality) then there is no easy way to _avoid_ infinite objects. One may get a hint of this from the following example: in the category of N-sets (sets with a distinguished self-map) let A be the two-element set in which the distinguished self-map has a unique fixed point. In Cats and Allegories (1.925) we point out that A^A, the object of self-maps of A, falls apart as a coproduct (disjoint union) of continuously many N-sets. Hence if one takes the set of equivalence classes of A^A, where the equivalence relation is the double-negation of equality, one obtains a discrete set (it has trivial N-action) whose cardinality is the continuum. But that's just a hint. Consider the following theorem for topoi. Let T be the initial object in the category of topoi and logical morphisms. _No axiom of infinity._ Let 1 be the terminator in T. Let Omega be its power object. Let P be Omega^Omega, the object of self-maps on Omega. There's a subobject, M, of P on which we may define the structure of a rig (a ring without negation) that mimics the natural numbers. In particular the set of global sections, that is, maps from 1 to M with its inherited rig structure, is isomorphic to the standard natural numbers. Because the global sections can be misleading in an arbitrary topos it's worth pointing out that M mimics the natural numbers even from an internal point of view. For instance given any pair of polynomials, f(x_1,...,x_n), g(x_1,...,x_n) with natural-number coefficients the the first-order sentence \exists_{x_1,...,x_n\in M} f(x_1,...,x_n) = g(x_1,...,x_n) is satisfied in T iff it is satisfied in the standard natural numbers. An elaboration of this argument allows us to construct a topos-object in T whose topos of global sections is isomorphic to the free topos with natural-numbers-object. And, as for M, an equation in the theory of topoi is internally true for this internal topos iff it is true for the free topos with NNO. Lest one think I'm butting up against the consistency proof, the truth value in T of 0 = 1 in M is not totally false. (That is, M is "somewhat inconsistent" from the internal point of view.) From the external point of view, though, the two maps from the terminator to M that name 0 and 1 are not equal (from the internal point of view their equalizer is non-trivial). In particular we can find f,g so that the first-order sentence above has no standard solutions but is not totally false in T. The slogan: once you've given up excluded middle there's no gain in giving up the axiom of infinity.