According to Feferman [1]}, a formal theory \(T\)  is adequate for an informal body of mathematics \(M\) ,
if every concept, argument, and result of \(M\)  is represented by a (basic or defined) concept, proof,
and a theorem, respectively, of \(T\) . Additionally, \(T\)  is faithful to \(M\) , if
every basic concept of \(T\)  corresponds to a basic concept of \(M\)  and every
axiom and rule of \(T\)  corresponds to or is implicit in the assumptions and reasoning followed in \(M\)  i.e., \(T\) 
does not go beyond \(M\)  conceptually or in principle. The use of strong negation in \(\mathrm {TCF}\) , and especially in its “total”
fragment, provides extra evidence for its adequacy as a formal system for \(\mathrm {BISH}\) . As dependent operations are crucial to
\(\mathrm {BISH}\)  (see [2]}), one needs to add dependency to \(\mathrm {TCF}\) , in order to get an adequate formalisation of \(\mathrm {BISH}\) .
Such an extension of \(\mathrm {TCF}\)  is an important open problem of independent interest. The use of inductive and
coinductive predicates in \(\mathrm {TCF}\)  prevent \(\mathrm {TCF}\)  from being a faithful formalisation for \(\mathrm {BISH}\) .
Although inductive definitions with rules of countably many premises are included in the extension\(\mathrm {BISH}^*\) 
is the system corresponding to [3]} and to the constructive topology of Bishop spaces (see [4]}, [5]}, [6]}
and [7]}), while \(\mathrm {BISH}\)  is the system corresponding to [8]}.
\(\mathrm {BISH}^*\)  of \(\mathrm {BISH}\) , coinduction is not present in Bishop-style constructive mathematics.
