Re: [HoTT] Univalence <-> equivalence induction

["Martín Hötzel Escardó" <"escardo..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 3266 bytes --]

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 
> <javascript:>> 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 <javascript:>> 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 <javascript:>. 
>
> >> 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 <javascript:>. 
> > For more options, visit https://groups.google.com/d/optout. 
>

[-- Attachment #1.2: Type: text/html, Size: 7472 bytes --]