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

[Jason Gross]

I'm not sure what you mean by "The interesting question, is why is it
provable?"

Univalence can't be proven within Coq because Coq is compatible with
proof-irrelevance for equality, which contradicts univalence (on, e.g., the
type bool = bool).

A formulation of computational univalence in Coq is a collection of
reduction rules for pattern matching on univalence, possibly together with
a proof that the reduction algorithm is terminating, confluent, and
strongly normalizing up to propositional equality.  For example, one
reduction rule is
∀ (X Y : Type) (e : X ≃ Y) (B : Type → Type) (f : X → B X)
  match ua e in (_ = T) return (T → B T) with
    | eq_refl ⇒ f
  end
  ≡
  λ (x : Y) ⇒
    match ua e in (_ = T) return B T with
      | eq_refl ⇒ f (e⁻¹ x)
    end

I'm pretty sure that most reduction rules for univalence that don't require
returning an arbitrary inductive type can be proven in Coq.  (For example,
this can can be proven, I believe, using the fact that e⁻¹ = ua⁻¹ (eq_sym
(ua e)), and then [case (ua e); reflexivity.].)  And even the ones that
require returning an arbitrary inductive type might be made to work with
typeclasses for w-types (a project I might try to play with when I have
time).

-Jason


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

> That's what I figured. The interesting question, is why is it provable?
> And given this, it seems that univalence can not be proven within Coq (in
> retrospect this makes sense) though now it is less clear to me what a
> computational formulation of it will be.
>
>
> On Mon, Feb 10, 2014 at 9:11 PM, Jason Gross <jasongross9 at gmail.com>wrote:
>
>> 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
>>>
>>>
>>
>
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140210/528b735b/attachment.htm