analysis (differential/integral calculus, functional analysis, topology) metric space, normed vector space open ball, open subset, neighbourhood convergence, limit of a sequence compactness, sequential compactness … There are many possible definitions of the (two-sided, Dedekind) real numbers type in dependent type theory. If the dependent type theory has a type universe or a type of all propositions, then one can translate the impredicative definition of the Dedekind real numbers over to dependent type theory. However, in dependent type theory without a type universe or a type of all propositions, the impredicative definition of the Dedekind real numbers no longer works. Nonetheless, it is possible to define the type of real numbers via inference rules as a type with a type family of domains of the structural Dedekind cut associated with each real number. We shall assume the minimum amount of type formers in dependent type theory to define Dedekind cuts of the rational numbers: The types in the dependent type theory form the (infinity,1)-categorical version of a Heyting category with exponential objects and a natural numbers object. In addition, if one has a type of all propositions in the dependent type theory, one can define the type of real numbers as the type of all (two-sided) Dedekind cuts, which are subtypes or predicates of the product type which satisfy the following axioms: Dedekind cuts are bounded: Dedekind cuts are rounded: Dedekind cuts are disjoint: Dedekind cuts are located: Usually, Dedekind cuts are presented as pairs of predicates