On Friday, 18 May 2018 17:41:00 UTC+2, Michael Shulman wrote: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.
Yes, this is the difference - or are you doing the same, Egbert?
Also, I should have said that I needed to adapt Peter's argument slightly - unfortunately, I couldn't use his result off-the-shelf. The main difference is that Peter works with a global identity system on all types (of a universe), whereas I work with an identity system on a single type, namely a universe. As a result, I can't define the type of left-cancellable maps using the notion of equality given by the identity system. Instead, I define it using the native (Martin-Loef) identity type, and with this little modification, Peter's argument goes through for the situation considered here.
Can you give a link to the "some years
ago" discussion claiming it strictly weaker?
I will try to dig it up tomorrow.
Martin
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ó
> <escar...@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 HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.