From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 20 Jul 2017 18:36:51 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Cc: awo...@cmu.edu, b.a.w.s...@gmail.com, ri...@cam.ac.uk Message-Id: <7cf42606-2ef4-4575-ad0e-da78e2bca514@googlegroups.com> In-Reply-To: References: <9971190E-3BFB-4ECC-ACFA-466D4936D838@cmu.edu> Subject: Re: [HoTT] Weaker forms of univalence MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1097_591050591.1500601011376" ------=_Part_1097_591050591.1500601011376 Content-Type: multipart/alternative; boundary="----=_Part_1098_1687924405.1500601011377" ------=_Part_1098_1687924405.1500601011377 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Why wouldn't a skeletal LCCC be a model of (1) + UIP? On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote: > > But is it known that this is definitely weaker? E.g. are there models=20 > that satisfy invariance but not the computation rule?=20 > > On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey > wrote:=20 > > I think we=E2=80=99ve been through this before:=20 > >=20 > > (1) (A =E2=89=83 B) -> (A =3D B)=20 > >=20 > > is logically equivalent to what may be called =E2=80=9Cinvariance=E2=80= =9D:=20 > >=20 > > if P(X) is any type depending on a type variable X, then given= =20 > any equivalence e : A =E2=89=83 B , we have P(A) =E2=89=83 P(B).=20 > >=20 > > if we add to this a certain =E2=80=9Ccomputation rule=E2=80=9D, we get = something=20 > logically equivalent to UA:=20 > > assume p : A =E2=89=83 B =E2=86=92 A =3D B; then given e : A =E2=89=83 = B, we have p(e) : A =3D B is=20 > a path in U.=20 > > Since we can transport along this path in any family of types over U,= =20 > and transport is always an equivalence,=20 > > there is a transport p(e)=E2=88=97 : A =E2=89=83 B in the identity fami= ly.=20 > > The required =E2=80=9Ccomputation rule=E2=80=9D states that p(e)=E2=88= =97 =3D e.=20 > >=20 > > Steve=20 > >=20 > >=20 > >=20 > >> On Jul 20, 2017, at 8:56 AM, Bas Spitters > wrote:=20 > >>=20 > >>> It was observed previously on this list,=20 > >> Maybe we should be using our wiki more?=20 > >> https://ncatlab.org/homotopytypetheory/=20 > >>=20 > >>=20 > >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman > wrote:=20 > >>> It was observed previously on this list, I think, that full univalenc= e=20 > >>> (3) is equivalent to=20 > >>>=20 > >>> (4) forall A, IsContr( Sigma(B:U) (A =E2=89=83 B) ).=20 > >>>=20 > >>> This follows from the fact that a fiberwise map is a fiberwise=20 > >>> equivalence as soon as it induces an equivalence on total spaces, and= =20 > >>> the fact that based path spaces are contractible. But the=20 > >>> contractibility of based path spaces also gives (2) -> (4), and hence= =20 > >>> (2) -> (3).=20 > >>>=20 > >>> I am not sure about (1). It might be an open question even in the=20 > >>> case when A and B are propositions.=20 > >>>=20 > >>>=20 > >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton > wrote:=20 > >>>> Consider the following three statements, for all types A and B:=20 > >>>>=20 > >>>> (1) (A =E2=89=83 B) -> (A =3D B)=20 > >>>> (2) (A =E2=89=83 B) =E2=89=83 (A =3D B)=20 > >>>> (3) isEquiv idtoeqv=20 > >>>>=20 > >>>> (3) is the full univalence axiom and we have implications (3) -> (2)= =20 > -> (1),=20 > >>>> but can we say anything about the other directions? Do we have (1) -= >=20 > (2) or=20 > >>>> (2) -> (3)? Can we construct models separating any/all of these thre= e=20 > >>>> statements?=20 > >>>>=20 > >>>> Thanks,=20 > >>>> Ian > ------=_Part_1098_1687924405.1500601011377 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Why wouldn't a skeletal LCCC be a model of (1) + UIP?<= br>
On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrot= e:
But is it known that this is= definitely weaker? =C2=A0E.g. are there models
that satisfy invariance but not the computation rule?

On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey <awo...@cmu.edu> wro= te:
> I think we=E2=80=99ve been through this before:
>
> =C2=A0(1) =C2=A0(A =E2=89=83 B) -> (A =3D B)
>
> is logically equivalent to what may be called =E2=80=9Cinvariance= =E2=80=9D:
>
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 if P(X) is any type depending on a typ= e variable X, then given any equivalence e : A =E2=89=83 B , we have P(A) = =E2=89=83 P(B).
>
> if we add to this a certain =E2=80=9Ccomputation rule=E2=80=9D, we= get something logically equivalent to UA:
> assume p : A =E2=89=83 B =E2=86=92 A =3D B; then given e : A =E2= =89=83 B, we have p(e) : A =3D B is a path in U.
> Since we can transport along this path in any family of types over= U, and transport is always an equivalence,
> there is a transport p(e)=E2=88=97 : A =E2=89=83 B in the identity= family.
> The required =E2=80=9Ccomputation rule=E2=80=9D states that p(e)= =E2=88=97 =3D e.
>
> Steve
>
>
>
>> On Jul 20, 2017, at 8:56 AM, Bas Spitters <b.a.w...@gmail.com> wrote:
>>
>>> It was observed previously on this list,
>> Maybe we should be using our wiki more?
>> https://ncatlab.org/= homotopytypetheory/
>>
>>
>> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman <shu...@sandi= ego.edu> wrote:
>>> It was observed previously on this list, I think, that ful= l univalence
>>> (3) is equivalent to
>>>
>>> (4) =C2=A0forall A, IsContr( Sigma(B:U) (A =E2=89=83 B) ).
>>>
>>> This follows from the fact that a fiberwise map is a fiber= wise
>>> equivalence as soon as it induces an equivalence on total = spaces, and
>>> the fact that based path spaces are contractible. =C2=A0Bu= t the
>>> contractibility of based path spaces also gives (2) -> = (4), and hence
>>> (2) -> (3).
>>>
>>> I am not sure about (1). =C2=A0It might be an open questio= n even in the
>>> case when A and B are propositions.
>>>
>>>
>>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton <ri...@cam.ac.u= k> wrote:
>>>> Consider the following three statements, for all types= A and B:
>>>>
>>>> =C2=A0(1) =C2=A0(A =E2=89=83 B) -> (A =3D B)
>>>> =C2=A0(2) =C2=A0(A =E2=89=83 B) =E2=89=83 (A =3D B)
>>>> =C2=A0(3) =C2=A0isEquiv idtoeqv
>>>>
>>>> (3) is the full univalence axiom and we have implicati= ons (3) -> (2) -> (1),
>>>> but can we say anything about the other directions? Do= we have (1) -> (2) or
>>>> (2) -> (3)? Can we construct models separating any/= all of these three
>>>> statements?
>>>>
>>>> Thanks,
>>>> Ian
------=_Part_1098_1687924405.1500601011377-- ------=_Part_1097_591050591.1500601011376--