From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sat, 29 Jul 2017 00:23:39 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: 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_2296_2016041409.1501313019951" ------=_Part_2296_2016041409.1501313019951 Content-Type: multipart/alternative; boundary="----=_Part_2297_496121890.1501313019952" ------=_Part_2297_496121890.1501313019952 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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_2297_496121890.1501313019952 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Only up to homotopy? So you still want the model to be usi= ng cubical sets? Actually, couldn't you interpret OTT into the hsets, i= nternally to HoTT? It'd be a hassle without a real solution to the infi= nite 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 Sh= ulman wrote:
Right: up to homot= opy, all cubes would be equivalent to points (hence
my question #1).

On Fri, Jul 28, 2017 at 6:47 PM, Matt Oliveri <atm...@gmail.com> w= rote:
> I'm confused. So you want a cubical type theory with only hset= s? In what
> sense would there be cubes, other than just points? I thoght OTT h= ad
> propositional extensionality. Though maybe that's only for str= ict props.
>
>
> On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrot= e:
>>
>> I am wondering about versions of cubical type theory with UIP.= =C2=A0The
>> motivation would be to have a type theory with canonicity for
>> 1-categorical semantics that can prove both function extension= ality
>> and propositional univalence. =C2=A0(I am aware of Observation= al Type
>> Theory, which I believe has UIP and proves function extensiona= lity,
>> but I don't think it proves propositional univalence -- al= though I
>> would be happy to be wrong about that.)
>>
>> Presumably we obtain a cubical type theory that's compatib= le with
>> axiomatic UIP if in CCHM cubical type theory we postulate only= a
>> single universe of propositions. =C2=A0But I wonder about some= possible
>> refinements, such as:
>>
>> 1. In this case do we still need *all* the Kan composition and= gluing
>> operations? =C2=A0If 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_2297_496121890.1501313019952-- ------=_Part_2296_2016041409.1501313019951--