Re: [HoTT] Univalence <-> equivalence induction

[Michael Shulman <shu...@sandiego.edu>]

I certainly knew that univalence is equivalent to
equivalence-induction *with* computation rule, which I think is what
is in Egbert's notes.  But I don't think I knew that you can do
without the computation rule.  Can you give a link to the "some years
ago" discussion claiming it strictly weaker?

On Fri, May 18, 2018 at 6:04 AM, Egbert Rijke <e.m....@gmail.com> wrote:
> Hi Martin,
>
> I think it was known. I taught this in my intro to HoTT class this semester:
>
> http://www.andrew.cmu.edu/user/erijke/hott/univalence.pdf
>
> Best wishes,
> Egbert
>
> On Fri, May 18, 2018 at 2:36 AM, Martín Hötzel Escardó
> <escardo...@gmail.com> wrote:
>>
>> Equivalence induction says that in order to prove something for all
>> equivalences, it is enough to prove it for all identity equivalences for all
>> types.
>>
>> This follows from univalence. But also, conversely, univalence follows
>> from it:
>>
>>    http://www.cs.bham.ac.uk/~mhe/agda-new/UF-Univalence.html#JEq
>>
>> Is this known? Some years ago it was claimed in this list that equivalence
>> induction would be strictly weaker than univalence.
>>
>> To prove the above, I apply a technique I learned from Peter Lumsdaine,
>> that given an abstract identity system (Id, refl , J) with no given
>> "computation rule" for J, produces another identity system (Id, refl , J' ,
>> J'-comp) with
>> a "propositional computation rule" J'-comp for J'.
>>
>>    http://www.cs.bham.ac.uk/~mhe/agda-new/Lumsdaine.html
>>
>> Martin
>>
>> --
>> 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.
>
>
>
>
> --
> egbertrijke.com
>
> --
> 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.