I have now had a chance to read over the first manuscript more
carefully. It is quite fascinating! I think that in modern language,
his system would be called a higher-order logic over a dependent type
theory. There are some warts from a modern perspective, but I think
it's quite astonishing how close Bishop's system is to modern
dependent type theories and higher-order logics, if in fact there was
historically no communication.
What nowadays we call "types", Bishop calls "classes"; and what we
call "functions" between types he calls "operations". He has
"power-classes" and "subclasses" which behave roughly like power-types
and sub-types in higher-order logic, along with a separate logic of
formulas that depend on classes. In particular, propositions are, as
far as I can tell, proof-irrelevant, and *not* identified with types!
He uses the Leibniz equality of HOL (two terms are equal if they
satisfy the same predicates) to formulate the beta and eta rules for
his Pi, Sigma, etc. classes, and includes (p26) the function
extensionality and propositional extensionality axioms again using
this Leibniz equality.
Some other interesting notes about Bishop's system:
1. He has a class of all classes. I think this means his system is
vulnerable to Girard's paradox and hence inconsistent. This is
amusing given his remark (p15) that "A contradiction would be just an
indication that we were indulging in meaningless formalism," although
to be fair he also says later (p26) that "If aspects of the
formalization are meaningless, experience will sooner or later let us
know." Of course, this should be fixable as usual by introducing a
hierarchy of universes.
2. His "sets" (p16) are classes (types) equipped with an equivalence
relation valued in *propositions* (more precisely, equipped with a
subclass of A x A satisfying reflexivity, symmetry, and transitivity).
So they are like setoids defined in Coq with Prop-valued equality
(where Prop satisfies propositional extensionality), not setoids
defined in MLTT with Type-valued equality.
3. He includes the axiom of choice (p12) formulated in terms of his
(proof-irrelevant) propositions, as well as what seems to be a Hilbert
choice operator (though it's not clear to me whether this applies in
open contexts or not). Since he has powerclasses with propositional
extensionality, I think this means that Diaconescu's argument proves
LEM, which he obviously wouldn't want. It's harder for me to guess
how this should be fixed, since without some kind of AC, setoids don't
satisfy the principle of unique choice.
4. He makes the class of all sets into a set (p19) with equality
meaning the mere existence of an isomorphism. But later (p21) he
refers to this set more properly as the set of "cardinal numbers".
5. He also defines a category (p19) to have a class of objects (no
equality relation imposed) and dependent *sets* (classes with equality
relation) of morphisms between any two objects.
6. As we did informally in the HoTT Book, he first introduces
non-dependent function types and then formulates dependent ones (which
he calls "guarded") in terms of a type family expressed as a
non-dependent function into the universe (rather than as a type
expression containing a variable).
It's quite possible, though, that I am misinterpreting some or all of
this; his notation is so different that it's easy to get confused. If
so, I hope someone will set me straight.