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

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

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 only know of three ways to get a well-behaved category of setoids:

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

2. Define a morphism of setoids to be not an operation respecting
equality but a total functional relation, as in the tripos-to-topos
construction and the ex/reg completion.  I personally believe this is
the correct solution in the most generality, but Bishop-style
constructivists don't seem to like it.

3. Assume the axiom of choice, which causes options (1) and (2) to coincide.


On 5/5/18, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote:
>
>
> On 05/05/2018, 05:27, "homotopyt...@googlegroups.com on behalf of
> Michael Shulman" <homotopyt...@googlegroups.com on behalf of
> shu...@sandiego.edu> wrote:
>
>>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.
>
> Why not? If we identify propositions with setoids that are internally
> propositions (all elements are equal) and identify propositions upto
> logical equality we get unique choice.
>
> What do I miss here?
> Thorsten
>
>
>>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
>