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

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

On 09/10/16 19:56, Joyal, André wrote:
> There are many variations. For example, a homotopy equivalence can be defined to
> be a pair of maps  f:a--->b and g:b--->a equipped with a pair of homotopies
> alpha:gf--->id_a and beta:fg --->id_b satisfying *one*(and only one) of the adjunction (=triangle) identities.

I am aware of that, but thanks for bringing it up again.

Perhaps what you bring up is related to the fact that if the type R x y 
is a retract of the type Id_X x y for all x,y:X, then in fact the two 
types are equivalent for all x,y. (Where R : X -> X -> U is arbitrary.)

(So in my example only *one* composition to the identity is enough to 
get the *other* composition to be the identity too.)

Although I can see formal proofs that Joyal-equivalence is a proposition 
(or h-proposition), I am still trying to find the best formal proof that 
uncovers the essence of this fact. This is why I asked the question of 
were this formulation of equivalence comes from.

This seems similar to trying to understand, as discussed in other 
messages in this list, the J combinator, expressing induction on Id, as 
a reformulation of the Yoneda Lemma, when types are seeing as 
omega-groupoids.

Best,
Martin