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

[Gregory Malecha]

Hi, Jason --

I'm not sure if this conversation has become too specialized for the list
in general, so it might be worthwhile taking it offline. It may only be of
interest to the more computer-sciency people.

What you say seems strange to me from a computational perspective. From a
logical perspective, this works nicely, but when I think about computation,
I usually think about running a program and it isn't clear what this
reduction rule would translate to in assembly language. For me, and perhaps
I am wrong, the key notion of computation is a compositional semantics.
I..e. I should be able to look at various pieces of the programming
language and compile them independently. This is essential to support
lambda abstraction, i.e. if I have a program:

match foobar in (_ = T) return (T → B T) with
  | eq_refl ⇒ f
end

(the same as your program except [ua e] is replaced with [foobar]) then I
would need to know how to compile it without knowing what foobar is.
[foobar] may come from an external library, be a parameter to my function,
etc.

The rule that you give above is a program equivalence, and is likely
provable, but I don't think of something like it as a reduction rule.

Perhaps that is me showing my narrow-minded computer science perspective.


On Mon, Feb 10, 2014 at 11:04 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> 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/
>>
>
>


-- 
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/20140211/4a23fe9d/attachment-0001.htm