Re: [HoTT] Re: Joyal's version of the notion of equivalence

[Martin Escardo <escardo...@googlemail.com>]

On 12/10/16 23:17, Vladimir Voevodsky wrote:
> I think the clearest formulation is my original one - as the condition
> of contractibility of the h-fibers.
>
> This is also the first form in which it was introduced and the first
> explicit formulation and proof of the fact that it is a proposition.

Vladimir, I agree with what you say above.

I was just trying to understand a particular, interesting case of a 
situation where we have types P(f) and Q(f) that are not hpropositions 
in general, but such that the product type P(f)xQ(f) is always an 
hproposition, as explained in my previous messages.

I hoped to get a motivation from homotopy theory, and Andre tried to 
explain this to me.

I do find it rather interesting that the cartesian product of two such 
types that are not in general hpropositions is always an hproposition.

A function can have a section in zillions of ways, and also have 
retraction in just as many ways, and we know in set theory that a 
function can have both a section and a retraction in at most one way. 
This is not surprising. But it does surprise me, for the moment, that 
this is the case in univalent mathematics too, given that we do know 
that the type of two-sided inverses is in general *not* an hproposition.

Best,
Martin