Abstract It is well known that over Heyting arithmetic with finite types, the effective principle of the formal Church thesis, stating that all number-theoretic functional relations are computable, is inconsistent with Brouwer’s intuitionistic principles on the continuum, in particular, the fan theorem. Here, we build two arithmetic quasi-toposes, validating on the one hand Brouwer’s continuity principles, including the Fan theorem, and on the other hand, a restricted form of Church’s Thesis, called the Type-theoretic Church Thesis and written $\textsf{TCT}$ , expressing that all morphisms of the considered quasi-topos are computable. One quasi-topos is constructed by formalizing the category of assemblies $\mathbf{Asm}$ within Hyland’s effective topos using intuitionistic Zermelo-Fraenkel set theory $\mathbf{IZF}$ extended with Brouwer’s continuity principles as our meta-theory. The other quasi-topos is obtained as an elementary quotient completion in the same intuitionistic meta-theory. While in previous work by the first author with F. Pasquali and G. Rosolini, it has been shown that these two quasi-toposes are equivalent when working within the classical $\mathbf{ZFC}$ set theory; here, we show that this is no longer the case when working within $\mathbf{IZF}$ . We also observe that the aforementioned inconsistency is resolved in such quasi-toposes by the non-validity of the axiom of unique choice on the natural numbers and that no non-trivial topos can validate the effective principle $\textsf{TCT}$ together with Brouwer’s continuity principles altogether.

The Minimalist Foundation, for short MF , was conceived by the first author with G. Sambin in 2005, and fully formalized in 2009, as a common core among the most relevant constructive and classical foundations for mathematics. To better accomplish its minimality, MF was designed as a two-level type theory, with an intensional level mTT , an extensional one emTT , and an interpretation of the latter into the first. Here, we first show that the two levels of MF are indeed equiconsistent by interpreting mTT into emTT . Then, we show that the classical extension emTT c is equiconsistent with emTT by suitably extending the Gödel-Gentzen double-negation translation of classical logic in the intuitionistic one. As a consequence, MF turns out to be compatible with classical predicative mathematics à la Weyl, contrary to the most relevant foundations for constructive mathematics. Finally, we show that the chain of equiconsistency results for MF can be straightforwardly extended to its impredicative version to deduce that Coquand-Huet's Calculus of Constructions equipped with basic inductive types is equiconsistent with its extensional and classical versions too.

Abstract In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in point-free topology. Our work is complementary to a previous one with M. E. Maietti, where we showed that, in dependent type theory, the well-known concept of wellfounded trees has a topological counterpart in terms of proof-relevant inductively generated formal covers used to provide a predicative and constructive representation of complete suplattices. The proofs performed within Martin–Löf’s type theory and the Minimalist Foundation have been checked in the Agda proof assistant.