> I am not sure about (1). It might be an open > question even in the
> case when A and B are propositions.
If A and B are hProps, then (1) => (3) under function extensionality (not sure if you can do away with out here). The key idea is that there can be only one equivalence between hProps. To prove contractibility, we must show that (A, idequiv) = (B, e) for any equivalence e of A and B. Let us prove A = B by (1); what remains is proving that idequiv = transport (1) e. It now suffices to show that A ≃ A is an hProp for A an hProp. This follows from function extensionality.
I don't think you need function extensionality for contractibility and
Sigma to respect equivalence. We need funext for Pi to respect
equivalence, but there are no Pis here.
On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross <jason...@gmail.com> wrote:
> 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.
>
> --
> 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.