[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Excluded middle makes everything so much easier since you just work with booleans. Archimedean ordered rational integral domains... Given a commutative ring $R$, we could define the type of power series on $R$ as simply the sequence type $\mathbb{N} \to R$, with power series multiplication defined as convolution of sequences. Maybe we could just work with rational numbers, and sequences of functions of rational numbers as procedures for computation... We are going back to the constructive BHK version and postulating a Cauchy complete Archimedean ordered field, which could be defined without propositional truncations. Then we could show that under excluded middle the set of Dedekind cut structures on the rational numbers is a Cauchy complete Archimedean ordered field... You can't actually define an Archimedean ordered field without propositional truncations. The issue is that the archimedean property requires the existential quantifier. No judgmental equality, no universes, no higher inductive types, no coinductive types. Only the basic constructive BHK logical operators (function types, dependent product types, product types, dependent sum types, sum types, empty type, unit type, booleans type) and natural numbers type. Possibly excluded middle, where propositions are (-1)-truncated types... category: redirected to nlab