Univalence <-> equivalence induction

Univalence <-> equivalence induction

[Martín Hötzel Escardó]

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

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


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

Re: [HoTT] Univalence <-> equivalence induction

[Egbert Rijke]

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

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

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

Re: [HoTT] Univalence <-> equivalence induction

[Michael Shulman]

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.  Can you give a link to the "some years
ago" discussion claiming it strictly weaker?

On Fri, May 18, 2018 at 6:04 AM, Egbert Rijke <e.m....@gmail.com> 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ó
> <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
>
> --
> 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.

Re: [HoTT] Univalence <-> equivalence induction

[Martín Hötzel Escardó]

[-- 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 --]

Re: [HoTT] Univalence <-> equivalence induction

[Nicolai Kraus]

[-- 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 --]

Re: [HoTT] Univalence <-> equivalence induction

[Thierry Coquand]

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

 Nice! Maybe one can use the same idea on the other characterisation of univalence that
we have

 Pi (X:U) (e:Equiv A X)   Id S  (A,idA) (X,e)

where S = Sigma (X:U) Equiv A X

 This should follow from equivalence induction.
 Thierry

On 19 May 2018, at 20:09, Nicolai Kraus <nicola...@gmail.com<mailto:nicola...@gmail.com>> wrote:

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.


--
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: 4746 bytes --]