  In this work we consider an extension MFcind of the Minimalist Foundation MF
for predicative constructive mathematics with the addition of inductive and
coinductive definitions sufficient to generate Sambin's Positive topologies,
namely Martin-L\"of-Sambin formal topologies equipped with a Positivity
relation (used to describe pointfree formal closed subsets). In particular the
intensional level of MFcind, called mTTcind, is defined by extending with
coinductive definitions another theory mTTind extending the intensional level
mTT of MF with the sole addition of inductive definitions. In previous work we
have shown that mTTind is consistent with Formal Church's Thesis CT and the
Axiom of Choice AC via an interpretation in Aczel's CZF+REA. Our aim is to show
the expectation that the addition of coinductive definitions to mTTind does not
increase its consistency strength by reducing the consistency of mTTcind+CT+AC
to the consistency of CZF+REA through various interpretations. We actually
reach our goal in two ways. One way consists in first interpreting
mTTcind+CT+AC in the theory extending CZF with the Union Regular Extension
Axiom, REA_U, a strengthening of REA, and the Axiom of Relativized Dependent
Choice, RDC. The theory CZF+REA_U+RDC is then interpreted in MLS*, a version of
Martin-L\"of's type theory with Palmgren's superuniverse S. A last step
consists in interpreting MLS* back into CZF+REA. The alternative way consists
in first interpreting mTTcind+AC+CT directly in a version of Martin-L\"of's
type theory with Palmgren's superuniverse extended with CT, which is then
interpreted back to CZF+REA. A key benefit of the first way is that the theory
CZF+REA_U+RDC also supports the intended set-theoretic interpretation of the
extensional level of MFcind. Finally, all the theories considered, except
mTTcind+AC+CT, are shown to be of the same proof-theoretic strength.
