From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sat, 29 Jul 2017 03:19:57 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> In-Reply-To: References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> Subject: Re: [HoTT] Re: cubical type theory with UIP MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2324_330287799.1501323597094" ------=_Part_2324_330287799.1501323597094 Content-Type: multipart/alternative; boundary="----=_Part_2325_77119810.1501323597094" ------=_Part_2325_77119810.1501323597094 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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_2325_77119810.1501323597094 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Sorry. I got distracted because the type theory you seem t= o 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 Shulma= n 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_2325_77119810.1501323597094-- ------=_Part_2324_330287799.1501323597094--