Interesting! At least I had not been aware of it. I think there's another very short way to see that "equivalence induction without computation rule" implies univalence. Recall the Capriotti/Licata/Orton-Pitts observation which says that ua + ua-beta (i.e. a function A~B -> A=B which is a section of A=B -> A~B) imply full univalence; see arXiv:1712.04890, 4.6. By distributivity of Pi and Sigma, we can write the type of pairs (ua,ua-beta) as a type family P indexed over equivalences: for types A,B and an equivalence e: A~B, we define P(A,B,e) := Sigma (p:A=B). id2equiv(p)=e. To inhabit P, we apply equivalence induction. It seems there are many such "coherification"-constructions in HoTT. -- Nicolai On 18/05/18 07:36, Martín Hötzel Escardó 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.