Joyal equivalence II

[Martin Escardo]

Define (where "=" is the identity type)

f:X->Y has a section := Sigma(s:Y->X), f.s = id.
f:X->Y has a retraction := Sigma(r:Y->X), r.f = id.

f:X->Y is a Joyal equivalence := f has a section
* f has a retraction.

We discussed that the type "f is a Joyal equivalence" is always a
proposition, although the types "f has a section" and "f has a
retraction" are not in general propositions, but rather structure or
data on f, of course.

For X:U and A:X->U, define

there is a unique x:X s.t. A(x) := isContr(Sigma(x:X), A(x)),
there is at most one x:X s.t. A(x) := isProp (Sigma(x:X), A(x)).

These (are always propositions and hence) are not in general
equivalent to the naive formulations copied from first-order
mathematics in set theory to type theory.

With this terminology, "f:X->Y is a Voevodsky equivalence" reads "for
every y:Y there is a unique x:X such that f(x)=y".

Now, it is easy to check that, for any A,B:U,

isProp(A * B) <-> (A -> isProp B) * (B -> isProp A),

where of course the logical equivalence can be replaced by an
equivalence, by univalence, as the lhs and rhs types are propositions,
but this is unimportant here.

Because we know that the Joyal equivalence of f:X->Y is always a
proposition, it follows that we always have

f has a section -> f has at most one retraction, and
f has a retraction -> f has at most one section.

Hence we recover what is true in set theory, for types more general
than sets, by considering the right notion of there-is-at-most-one.

But surely homotopy theorists knew this too.

Notice also that, in each implication, it is possible to change the
Sigma in the premise to an existential quantifier (a -1-truncated
Sigma), because the conclusion is a proposition, to get the same
conclusion. And conversely if we had stated the result with the
existential quantifier, we would recover the result with Sigma, as it
is a stronger hypothesis (or has more data available).

(What are the shortest proofs of each of these two implications in
univalent type theory?)

Martin