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