In this paper we show how infinite objects can be defined in a constructive type theory. The type theory that we use is a variant of Martin-Lof's Intuitionistic Type Theory. We show how one can express the intuition that infinite objects are understood through a limiting process without having to introduce partial objects in the theory. This means that we can adhere to the propositions-as-types principle. The type of infinite objects thus contains only total elements. The approximation is expressed through a sequence of types that approximate the type of infinite objects. We give two semantic accounts of types of infinite objects. The first is lattice theoretic and shows how these types can be understood as fixed points. The second is category theoretic and shows the duality between types of infinite objects and the ordinary recursive type definitions.