Certainly (2) => (3), at least if you assume function extensionality; it
suffices to show that (\Sigma B, A ≃ B) is contractable, and since
contractibility and sigma respect equivalence, we can transfer the proof
that (\Sigma B, A = B) is contractable. I think the same is not true of
(1), though I'm not sure.

On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote:

> Consider the following three statements, for all types A and B:
>
>    (1)  (A ≃ B) -> (A = B)
>    (2)  (A ≃ B) ≃ (A = B)
>    (3)  isEquiv idtoeqv
>
> (3) is the full univalence axiom and we have implications (3) -> (2) ->
> (1), but can we say anything about the other directions? Do we have (1)
> -> (2) or (2) -> (3)? Can we construct models separating any/all of
> these three statements?
>
> Thanks,
> Ian
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>