Re: [HoTT] Univalence <-> equivalence induction

[Nicolai Kraus <nicola...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1985 bytes --]

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


[-- Attachment #2: Type: text/html, Size: 3244 bytes --]