From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 23 Mar 2017 05:16:37 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Cc: Thierry...@cse.gu.se, vlad...@ias.edu, univalent-...@googlegroups.com Message-Id: In-Reply-To: References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <96ed5e86-5564-4d98-a759-5a3301968501@googlegroups.com> <7EFC9320-4852-469F-9609-16C27D969316@ias.edu> <4f4bcfe8-5d25-42f4-9bf2-ebf5748d629a@googlegroups.com> Subject: Re: [HoTT] about the HTS MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_355_242605208.1490271397333" ------=_Part_355_242605208.1490271397333 Content-Type: multipart/alternative; boundary="----=_Part_356_1443870429.1490271397334" ------=_Part_356_1443870429.1490271397334 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Mike has explained to me that the approach I'm thinking of is not cohesion.= =20 Sorry about that. On Thursday, March 23, 2017 at 7:33:32 AM UTC-4, Michael Shulman wrote: > > Unless I misunderstand, that's not at all what cohesion is about.=20 > Lawvere's cohesion is about relating discrete sets to space-like=20 > objects (in the non-homotopical up-to-homeomorphism sense). Higher=20 > cohesion is about relating oo-groupoids to "topological oo-groupoids"=20 > in an analogous way.=20 > > On Thu, Mar 23, 2017 at 4:22 AM, Matt Oliveri > wrote:=20 > > Thanks.=20 > >=20 > > I agree that with the sSet option, with an equality reflection rule, it= =20 > > would be infeasible to check judgments without extra stuff from outside= =20 > the=20 > > type theory proper. But what's wrong with that? We add extra stuff=20 > anyway,=20 > > like type classes, proof scripts, and implicit arguments. To me, it=20 > seems=20 > > that the practical concern of checking the truth of judgments does not= =20 > need=20 > > to be solved by the design of the core type theory. Indeed, it seems=20 > like=20 > > better separation of concerns *not* to solve it there.=20 > >=20 > > Anyway, my understanding of bSet, from what Thierry Coquand said, is=20 > that=20 > > it'd be a more OTT-like version of sSet, which is more ETT-like. So=20 > instead=20 > > of paths between bSets being reflectable to judgmental equalities, they= =20 > > would be "strict propositions" (sProp), whose elements are not only all= =20 > > (typally) equal, but they also have no computational content. So any=20 > > "transport" across a strict equality reduces away, as long as it doesn'= t=20 > > change the type. (It doesn't have to be (judgmentally equal to)=20 > > reflexivity.)=20 > >=20 > > I figure the idea is that bSet should be able to do everything sSet can= ,=20 > > just with extra computationally-irrelevant transports thrown in to=20 > appease a=20 > > decidable type checker.=20 > >=20 > > I don't actually see how either of these universes would help define=20 > > semi-simplicial types. I didn't realize that was the goal here. I=20 > thought we=20 > > were just trying to make set-level math more convenient.=20 > >=20 > > -----------=20 > >=20 > > Though I haven't given it a serious thinking-about, I figured that stuf= f=20 > > with cohesion would be a good way to make semi-simplicial types=20 > definable,=20 > > without adding non-fibrant types.=20 > > (https://homotopytypetheory.org/2015/09/25/realcohesion/) It sounded=20 > like=20 > > cohesion gives you a set-level view of non-hsets, so I figured you=20 > should be=20 > > able to use strict equality in the construction of non-hsets that way.= =20 > >=20 > > I suppose strict sets and cohesion can be combined. A set-level view of= =20 > > things should yield only strict sets, not arbitrary hsets. (I guess tha= t=20 > > requires a whole hierarchy of strict set universes. But unlike HTS,=20 > they're=20 > > all "included" in the univalent universes, not the other way around.)= =20 > >=20 > > On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote:=20 > >>=20 > >> 1. As Thierry pointed out previously, the problem with sSet is that if= =20 > we=20 > >> postulate that nat:sSet, then for any (small) type T, the function typ= e=20 > T ->=20 > >> nat is in sSet, e.g. nat -> nat is in sSet.=20 > >>=20 > >> Since it is possible to construct two elements of nat -> nat the=20 > equality=20 > >> between which is an undecidable proposition, it implies that the=20 > >> definitional equality in any sufficiently advanced type system with=20 > sSet and=20 > >> nat:sSet is undecidable.=20 > >>=20 > >> That means that witnesses, in some language, of definitional equality= =20 > need=20 > >> to be carried around and therefore the design of a proof assistant=20 > where the=20 > >> proof term is the proof is not possible in this system.=20 > >>=20 > >> 2. It is not so clear what would happen with only bSet and nat:bSet.= =20 > >>=20 > >> Vladimir.=20 > >>=20 > >>=20 > >>=20 > >>=20 > >>=20 > >> On Mar 22, 2017, at 5:49 PM, Thierry Coquand =20 > wrote:=20 > >>=20 > >>=20 > >> If my note was correct, it describes in the cubical set model two=20 > >> univalent universes=20 > >> (subpresheaf of the first universe) that satisfy=20 > >>=20 > >> (1) if A : sSet and p : Path A a b then a =3D b : A and= p=20 > is=20 > >> the constant path a=20 > >> (equality reflection rule)=20 > >>=20 > >> (2) if A : bSet and p and q of type Path A a b then p =3D q : Pat= h A=20 > a=20 > >> b=20 > >> (judgemental form of UIP)=20 > >>=20 > >> Maybe (1) or (2) could be used instead of HTS (and we would remain in= =20 > an=20 > >> univalent=20 > >> theory, where all types are fibrant)=20 > >>=20 > >> For testing this, one question is: can we define semi-simplicial=20 > types=20 > >> in (1)? in (2)?=20 > >>=20 > >> Best regards,=20 > >> Thierry=20 > >>=20 > >>=20 > >>=20 > >> On 20 Mar 2017, at 16:12, Matt Oliveri wrote:=20 > >>=20 > >> So the answer was yes, right? Problem solved?=20 > >>=20 > >> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:=20 > >>>=20 > >>> Just a thought=E2=80=A6 Can we devise a version of the HTS where exac= t=20 > equality=20 > >>> types are not available for the universes such that, even with the=20 > exact=20 > >>> equality, HTS would remain a univalent theory.=20 > >>>=20 > >>> Maybe only some types should be equipped with the exact equality and= =20 > this=20 > >>> should be a special quality of types.=20 > >>>=20 > >>> Vladimir.=20 > >>>=20 > >>> PS If there are higher inductive types then the exact equality should= =20 > not=20 > >>> be available for them either.=20 > >>=20 > >>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > Groups=20 > >> "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > >> email to HomotopyTypeThe...@googlegroups.com .=20 > > >> For more options, visit https://groups.google.com/d/optout.=20 > >>=20 > >>=20 > >>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > Groups=20 > >> "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > >> email to HomotopyTypeThe...@googlegroups.com .=20 > > >> For more options, visit https://groups.google.com/d/optout.=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups=20 > > "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > > email to HomotopyTypeThe...@googlegroups.com .=20 > > For more options, visit https://groups.google.com/d/optout.=20 > ------=_Part_356_1443870429.1490271397334 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Mike has explained to me that the approach I'm thinkin= g of is not cohesion. Sorry about that.

On Thursday, March 23, 2017 = at 7:33:32 AM UTC-4, Michael Shulman wrote:
Unless I misunderstand, that's not at all what cohesion is= about.
Lawvere's cohesion is about relating discrete sets to space-like
objects (in the non-homotopical up-to-homeomorphism sense). =C2=A0Highe= r
cohesion is about relating oo-groupoids to "topological oo-groupoi= ds"
in an analogous way.

On Thu, Mar 23, 2017 at 4:22 AM, Matt Oliveri <atm...@gmail.com> w= rote:
> Thanks.
>
> I agree that with the sSet option, with an equality reflection rul= e, it
> would be infeasible to check judgments without extra stuff from ou= tside the
> type theory proper. But what's wrong with that? We add extra s= tuff anyway,
> like type classes, proof scripts, and implicit arguments. To me, i= t seems
> that the practical concern of checking the truth of judgments does= not need
> to be solved by the design of the core type theory. Indeed, it see= ms like
> better separation of concerns *not* to solve it there.
>
> Anyway, my understanding of bSet, from what Thierry Coquand said, = is that
> it'd be a more OTT-like version of sSet, which is more ETT-lik= e. So instead
> of paths between bSets being reflectable to judgmental equalities,= they
> would be "strict propositions" (sProp), whose elements a= re not only all
> (typally) equal, but they also have no computational content. So a= ny
> "transport" across a strict equality reduces away, as lo= ng as it doesn't
> change the type. (It doesn't have to be (judgmentally equal to= )
> reflexivity.)
>
> I figure the idea is that bSet should be able to do everything sSe= t can,
> just with extra computationally-irrelevant transports thrown in to= appease a
> decidable type checker.
>
> I don't actually see how either of these universes would help = define
> semi-simplicial types. I didn't realize that was the goal here= . I thought we
> were just trying to make set-level math more convenient.
>
> -----------
>
> Though I haven't given it a serious thinking-about, I figured = that stuff
> with cohesion would be a good way to make semi-simplicial types de= finable,
> without adding non-fibrant types.
> (https://homotopytypetheory.org/2015/09= /25/realcohesion/) It sounded like
> cohesion gives you a set-level view of non-hsets, so I figured you= should be
> able to use strict equality in the construction of non-hsets that = way.
>
> I suppose strict sets and cohesion can be combined. A set-level vi= ew of
> things should yield only strict sets, not arbitrary hsets. (I gues= s that
> requires a whole hierarchy of strict set universes. But unlike HTS= , they're
> all "included" in the univalent universes, not the other= way around.)
>
> On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote:
>>
>> 1. As Thierry pointed out previously, the problem with sSet is= that if we
>> postulate that nat:sSet, then for any (small) type T, the func= tion type T ->
>> nat is in sSet, e.g. nat -> nat is in sSet.
>>
>> Since it is possible to construct two elements of nat -> na= t the equality
>> between which is an undecidable proposition, it implies that t= he
>> definitional equality in any sufficiently advanced type system= with sSet and
>> nat:sSet is undecidable.
>>
>> That means that witnesses, in some language, of definitional e= quality need
>> to be carried around and therefore the design of a proof assis= tant where the
>> proof term is the proof is not possible in this system.
>>
>> 2. It is not so clear what would happen with only bSet and nat= :bSet.
>>
>> Vladimir.
>>
>>
>>
>>
>>
>> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thier...@c= se.gu.se> wrote:
>>
>>
>> If my note was correct, it describes in the cubical set model = two
>> univalent universes
>> (subpresheaf of the first universe) =C2=A0that satisfy
>>
>> =C2=A0(1) =C2=A0 if =C2=A0 A : sSet =C2=A0 =C2=A0and =C2=A0 p = : Path A a b =C2=A0 then =C2=A0 a =3D b : A =C2=A0and p is
>> the constant path a
>> (equality reflection rule)
>>
>> =C2=A0(2) =C2=A0 if A : bSet and p and q of type Path A a b = =C2=A0 then p =3D q : Path A a
>> b
>> (judgemental form of UIP)
>>
>> =C2=A0Maybe (1) or (2) could be used instead of HTS (and we wo= uld remain in an
>> univalent
>> theory, where all types are fibrant)
>>
>> =C2=A0For testing this, one question is: =C2=A0can we define s= emi-simplicial types
>> in (1)? in (2)?
>>
>> =C2=A0Best regards,
>> =C2=A0Thierry
>>
>>
>>
>> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com= > wrote:
>>
>> So the answer was yes, right? Problem solved?
>>
>> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
>>>
>>> Just a thought=E2=80=A6 Can we devise a version of the HTS= where exact equality
>>> types are not available for the universes such that, even = with the exact
>>> equality, HTS would remain a univalent theory.
>>>
>>> Maybe only some types should be equipped with the exact eq= uality and this
>>> should be a special quality of types.
>>>
>>> Vladimir.
>>>
>>> PS If there are higher inductive types then the exact equa= lity should not
>>> be available for them either.
>>
>>
>> --
>> You received this message because you are subscribed to the Go= ogle Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an
>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> For more options, visit https://group= s.google.com/d/optout.
>>
>>
>>
>> --
>> You received this message because you are subscribed to the Go= ogle Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an
>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> For more options, visit https://group= s.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 HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.go= ogle.com/d/optout.
------=_Part_356_1443870429.1490271397334-- ------=_Part_355_242605208.1490271397333--