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.