From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sat, 29 Jul 2017 04:08:06 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> Subject: Re: [HoTT] Re: cubical type theory with UIP MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2431_521413880.1501326486921" ------=_Part_2431_521413880.1501326486921 Content-Type: multipart/alternative; boundary="----=_Part_2432_662074209.1501326486922" ------=_Part_2432_662074209.1501326486922 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Now I'm having second thoughts. Quotienting together hprops might make type equality computationally relevant. Not something you want with OTT's strict props or ETT's equality. Maybe 2-dimensional type theory would be good for the job. In this case the 2-cells would not be distinguishable by equality, but might still have computational content. On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote: > > Sorry. I got distracted because the type theory you seem to be asking for > doesn't sound cubical. Like I said, I suspect OTT could handle hprop > extensionality, if it doesn't already. Probably ETT could too. > > On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote: >> >> As I said, >> >> > The motivation would be to have a type theory with canonicity for >> > 1-categorical semantics >> >> So no, I don't want "the model" to be using cubical sets, I want >> models in all suitable 1-categories (e.g. Pi-pretopos etc.). >> >> On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri wrote: >> > Only up to homotopy? So you still want the model to be using cubical >> sets? >> > Actually, couldn't you interpret OTT into the hsets, internally to >> HoTT? >> > It'd be a hassle without a real solution to the infinite coherence >> problem, >> > but it should work, since the h-levels involved are bounded. >> > >> > On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wrote: >> >> >> >> Right: up to homotopy, all cubes would be equivalent to points (hence >> >> my question #1). >> >> >> >> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri >> wrote: >> >> > I'm confused. So you want a cubical type theory with only hsets? In >> what >> >> > sense would there be cubes, other than just points? I thoght OTT had >> >> > propositional extensionality. Though maybe that's only for strict >> props. >> >> > >> >> > >> >> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote: >> >> >> >> >> >> I am wondering about versions of cubical type theory with UIP. The >> >> >> motivation would be to have a type theory with canonicity for >> >> >> 1-categorical semantics that can prove both function extensionality >> >> >> and propositional univalence. (I am aware of Observational Type >> >> >> Theory, which I believe has UIP and proves function extensionality, >> >> >> but I don't think it proves propositional univalence -- although I >> >> >> would be happy to be wrong about that.) >> >> >> >> >> >> Presumably we obtain a cubical type theory that's compatible with >> >> >> axiomatic UIP if in CCHM cubical type theory we postulate only a >> >> >> single universe of propositions. But I wonder about some possible >> >> >> refinements, such as: >> >> >> >> >> >> 1. In this case do we still need *all* the Kan composition and >> gluing >> >> >> operations? If all types are hsets then it seems like it ought to >> be >> >> >> unnecessary to have these operations at all higher dimensions. >> >> >> >> >> >> 2. Can it be enhanced to make UIP provable, such as by adding a >> >> >> computing K eliminator? >> >> >> >> >> >> Mike >> > ------=_Part_2432_662074209.1501326486922 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Now I'm having second thoughts. Quotienting together h= props might make type equality computationally relevant. Not something you = want with OTT's strict props or ETT's equality. Maybe 2-dimensional= type theory would be good for the job. In this case the 2-cells would not = be distinguishable by equality, but might still have computational content.=

On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt Oliveri wrote:=
Sorry. I got = distracted because the type theory you seem to be asking for doesn't so= und cubical. Like I said, I suspect OTT could handle hprop extensionality, = if it doesn't already. Probably ETT could too.

On Saturday, July= 29, 2017 at 4:08:01 AM UTC-4, Michael Shulman wrote:
As I said,

> The motivation would be to have a type theory with canonicity for
> 1-categorical semantics

So no, I don't want "the model" to be using cubical sets,= I want
models in all suitable 1-categories (e.g. Pi-pretopos etc.).

On Sat, Jul 29, 2017 at 12:23 AM, Matt Oliveri <= atm...@gmail.com> wrote:
> Only up to homotopy? So you still want the model to be using cubic= al sets?
> Actually, couldn't you interpret OTT into the hsets, internall= y to HoTT?
> It'd be a hassle without a real solution to the infinite coher= ence problem,
> but it should work, since the h-levels involved are bounded.
>
> On Saturday, July 29, 2017 at 2:20:06 AM UTC-4, Michael Shulman wr= ote:
>>
>> Right: up to homotopy, all cubes would be equivalent to points= (hence
>> my question #1).
>>
>> On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gm= ail.com> wrote:
>> > I'm confused. So you want a cubical type theory with = only hsets? In what
>> > sense would there be cubes, other than just points? I tho= ght OTT had
>> > propositional extensionality. Though maybe that's onl= y for strict props.
>> >
>> >
>> > On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shu= lman wrote:
>> >>
>> >> I am wondering about versions of cubical type theory = with UIP. =C2=A0The
>> >> motivation would be to have a type theory with canoni= city for
>> >> 1-categorical semantics that can prove both function = extensionality
>> >> and propositional univalence. =C2=A0(I am aware of Ob= servational Type
>> >> Theory, which I believe has UIP and proves function e= xtensionality,
>> >> but I don't think it proves propositional univale= nce -- although I
>> >> would be happy to be wrong about that.)
>> >>
>> >> Presumably we obtain a cubical type theory that's= compatible with
>> >> axiomatic UIP if in CCHM cubical type theory we postu= late only a
>> >> single universe of propositions. =C2=A0But I wonder a= bout some possible
>> >> refinements, such as:
>> >>
>> >> 1. In this case do we still need *all* the Kan compos= ition and gluing
>> >> operations? =C2=A0If all types are hsets then it seem= s like it ought to be
>> >> unnecessary to have these operations at all higher di= mensions.
>> >>
>> >> 2. Can it be enhanced to make UIP provable, such as b= y adding a
>> >> computing K eliminator?
>> >>
>> >> Mike
------=_Part_2432_662074209.1501326486922-- ------=_Part_2431_521413880.1501326486921--