Re: [HoTT] Bishop's work on type theory

[Michael Shulman <shu...@sandiego.edu>]

On 5/5/18, Michael Shulman <shu...@sandiego.edu> wrote:
> I think the problem is that it's not consistent about what a
> "proposition" is.  If a "proposition" is a setoid in which all
> elements are equal, then to be consistent, the equality relations of
> other setoids should also be valued in "propositions" of *this* sort,
> not the original collection of "propositions" you started with.
> Otherwise, I think you won't necessarily be able to take the quotient
> of a setoid by a "proposition"-valued equivalence relation, which is
> the whole point of introducing setoids in the first place.  But down
> this route lies infinity.

I take that back: this doesn't lead to an infinite sequence, instead
it stops after one iteration, at a result that coincides with (1):

> 1. Use propositions as types, as in MLTT Type-valued setoids and the
> ex/lex completion.

After all, "a proposition is a setoid in which any two elements are
equal" is essentially the same as "a proposition is a type".  This is
of course a perfectly good way to get a category of setoids (although
from a semantic point of view it is too limiting, restricting you to
categories that arise as ex/lex completions), and I believe it's how a
lot of people have interpreted Bishop's mathematics inside MLTT (for
instance).  But unless I'm confused, it's not what Bishop is trying to
do in this manuscript; he definitely seems to want the equality
relations of his setoids to be proof-irrelevant predicates.