[HoTT-reading-group] Isomorphism's & Equality

[Jason Gross]

With the univalence axiom, your goal is very easy; if you have (H : A ≃ B)
and ua is the univalence axiom, then you have (ap P (ua H) : P A = P B)
(and (X = Y -> X -> Y) is an easy path induction).

Without univalence, it's unprovable in general.  Consider A ≡ unit,
B ≡ unit * unit, and P x ≡ (unit = x).  Then we have unit ≃ unit * unit,
and we have P unit (by refl), but we don't have P (unit * unit) (which is
unit = unit * unit), unless we have univalence/propositional extensionality.

However, you can prove it for almost any appropriately concrete type family
not involving equality (or anything else where the only way to construct it
is when things are judgmentally equal).  The benefit of having
computational univalence is that you don't have to do so manually.

-Jason


On Mon, Feb 10, 2014 at 8:17 PM, Gregory Malecha <gmalecha at cs.harvard.edu>wrote:

> Hello --
>
> I was thinking a little bit more about the proof today, and I'm wondering
> if the following statement is provable:
>
> Goal forall (A B : Type), A \equiv B -> forall (P : Type -> Prop), P A ->
> P B.
>
> (here \equiv is meant to be HoTT equivalence of types)
>
> In particular, this gets at the idea that you can not write a proposition
> that distinguishes two equivalent types, i.e. Type is a setoid and no
> function in the language can distinguish equivalent values in the setoid.
>
> You can also make this stronger using [transport] (or whatever it is
> called in HoTT):
>
> Goal forall (A B : Type) (pf : \equiv A B)
>             (E : Type -> Type)
>             (P : forall x, E x -> Prop),
>        forall a : E A, P A a ->
>                        P B (@transport A B pf E a).
>
> The idea here is you can get arbitrary amounts of other data associated
> with the type (e.g. eliminators) and everything will still work. Neither of
> these is provable in vanilla Coq, though you can prove both by giving
> richer types for [P] that guarantee that they respect equivalence.
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>
> _______________________________________________
> HoTT-reading-group mailing list
> HoTT-reading-group at mit.edu
> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140210/f117c617/attachment-0001.htm