From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 31 Jul 2017 10:36:37 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Cc: m.es...@cs.bham.ac.uk Message-Id: In-Reply-To: References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> Subject: Re: [HoTT] Re: cubical type theory with UIP MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_4181_406860282.1501522597227" ------=_Part_4181_406860282.1501522597227 Content-Type: multipart/alternative; boundary="----=_Part_4182_2047408322.1501522597227" ------=_Part_4182_2047408322.1501522597227 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Can you point me to an example of a not-fully-satisfactory cut elimination theorem for FOL= and say what's wrong with it, so I can better appreciate the problem? On Monday, July 31, 2017 at 11:51:18 AM UTC-4, Michael Shulman wrote: > > As I've said twice already, what I want to do with this system is use > it as an internal language for 1-toposes. So to me, that is the > answer to Martin's question (2). I'm not quite sure what Martin means > by his question (1), since he's just described a type theory, but the > original question I asked was whether cubical methods can be used to > describe a version of such a type theory with canonicity. > > Another motivation is that as far as I know, there is not a really > satisfactory version of sequent calculus for first-order logic with > equality (e.g. not having a fully satisfactory cut-elimination > theorem). If cubical methods are a good way to treat equality > "computationally", I wonder whether a "cubical sequent calculus" would > be able to deal with equality better. > > I'm not quite sure what a "strict proposition" is, but if you mean > having a type of propositions that doesn't include all of them, then > the reason that's not enough for me is that frequently in univalent > type theory we encounter types that we *prove* to be propositions even > though they are not "given as such", such as "being contractible" and > "being a proposition", and this is responsible for a significant > amount of the unique flavor and usefulness of univalent type theory. > > For semantic reasons I wouldn't want to use intuitionistic set theory, > because it doesn't naturally occur as the internal language of > categories. You can perform contortions to model it therein, but that > involves interpreting it into type theory rather than the other way > around. I don't know what you mean by "somehow clean it up into a > type system", but if you can do that cleaning up and obtain a type > theory (a "formal type theory" in Bob Harper's sense, not a > "computational type theory", i.e. one that is inductively generated by > rules rather than assigning types to untyped terms in an "intended > semantics"), then I'd like to see it. > > Mike > > On Sun, Jul 30, 2017 at 8:49 PM, Matt Oliveri > wrote: > > On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo > wrote: > >> I am interested in this question. > >> > >> Univalent type theory gives something we don't have in e.g. the > calculus > >> of constructions, such as unique choice, or function extensionality or > >> propositional extensionality. > >> > >> A very attractive type theory, before we start to consider higher > >> dimensional types that are not sets, is an intensional Martin-Loef type > >> theory in with universes of propositions and of sets, with > propositional > >> truncation, function extensionality, propositional extensionality, > >> quotients, Sigma and Exists. > >> > >> (1) What is this type theory? (Whatever it is, it is a common extension > >> of some spartan intensional Martin-Loef type theory and the internal > >> language of the free elementary topos.) > >> > >> (2) What are its models? In particular (as Mike asks), which fragment > of > >> the cubical model does it correspond to? > >> > >> Martin > > > > I'm curious what you guys are thinking of doing with this kind of > > system, and why extensional equality of strict propositions is not > > enough. Is it just that using strict propositions is bad style for > > structuralists? Or maybe I just mistakenly assumed strict > > propositional extensionality is not enough. > > > > (Any computational content of proofs of strict propositions is not > > internalized. So with constructive functions, strict propositions do > > not provide unique choice.) > > > >> On 29/07/17 22:19, Michael Shulman wrote: > >>> But it seems to me that cubical type theory could solve these problems > >>> in a nicer way, which is why I asked. > >>> > >>> On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri > wrote: > >>>> 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_4182_2047408322.1501522597227 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Can you point me to an example of a not-fully-satisfactory= cut elimination theorem for FOL=3D and say what's wrong with it, so I = can better appreciate the problem?

On Monday, July 31, 2017 at 11:51= :18 AM UTC-4, Michael Shulman wrote:
As I've said twice already, what I want to do with this system is= use
it as an internal language for 1-toposes. =C2=A0So to me, that is the
answer to Martin's question (2). =C2=A0I'm not quite sure what = Martin means
by his question (1), since he's just described a type theory, but t= he
original question I asked was whether cubical methods can be used to
describe a version of such a type theory with canonicity.

Another motivation is that as far as I know, there is not a really
satisfactory version of sequent calculus for first-order logic with
equality (e.g. not having a fully satisfactory cut-elimination
theorem). =C2=A0If cubical methods are a good way to treat equality
"computationally", I wonder whether a "cubical sequent c= alculus" would
be able to deal with equality better.

I'm not quite sure what a "strict proposition" is, but if= you mean
having a type of propositions that doesn't include all of them, the= n
the reason that's not enough for me is that frequently in univalent
type theory we encounter types that we *prove* to be propositions even
though they are not "given as such", such as "being cont= ractible" and
"being a proposition", and this is responsible for a signific= ant
amount of the unique flavor and usefulness of univalent type theory.

For semantic reasons I wouldn't want to use intuitionistic set theo= ry,
because it doesn't naturally occur as the internal language of
categories. =C2=A0You can perform contortions to model it therein, but = that
involves interpreting it into type theory rather than the other way
around. =C2=A0I don't know what you mean by "somehow clean it = up into a
type system", but if you can do that cleaning up and obtain a type
theory (a "formal type theory" in Bob Harper's sense, not= a
"computational type theory", i.e. one that is inductively gen= erated by
rules rather than assigning types to untyped terms in an "intended
semantics"), then I'd like to see it.

Mike

On Sun, Jul 30, 2017 at 8:49 PM, Matt Oliveri <atm...@gmail.com> w= rote:
> On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo <m.e...@cs.bham.ac.u= k> wrote:
>> I am interested in this question.
>>
>> Univalent type theory gives something we don't have in e.g= . the calculus
>> of constructions, such as unique choice, or function extension= ality or
>> propositional extensionality.
>>
>> A very attractive type theory, before we start to consider hig= her
>> dimensional types that are not sets, is an intensional Martin-= Loef type
>> theory in with universes of propositions and of sets, with pro= positional
>> truncation, function extensionality, propositional extensional= ity,
>> quotients, Sigma and Exists.
>>
>> (1) What is this type theory? (Whatever it is, it is a common = extension
>> of some spartan intensional Martin-Loef type theory and the in= ternal
>> language of the free elementary topos.)
>>
>> (2) What are its models? In particular (as Mike asks), which f= ragment of
>> the cubical model does it correspond to?
>>
>> Martin
>
> I'm curious what you guys are thinking of doing with this kind= of
> system, and why extensional equality of strict propositions is not
> enough. Is it just that using strict propositions is bad style for
> structuralists? Or maybe I just mistakenly assumed strict
> propositional extensionality is not enough.
>
> (Any computational content of proofs of strict propositions is not
> internalized. So with constructive functions, strict propositions = do
> not provide unique choice.)
>
>> On 29/07/17 22:19, Michael Shulman wrote:
>>> But it seems to me that cubical type theory could solve th= ese problems
>>> in a nicer way, which is why I asked.
>>>
>>> On Sat, Jul 29, 2017 at 4:08 AM, Matt Oliveri <atm...@gmail= .com> wrote:
>>>> Now I'm having second thoughts. Quotienting togeth= er hprops might make type
>>>> equality computationally relevant. Not something you w= ant 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 disting= uishable by equality,
>>>> but might still have computational content.
>>>>
>>>>
>>>> On Saturday, July 29, 2017 at 6:19:57 AM UTC-4, Matt O= liveri wrote:
>>>>>
>>>>> Sorry. I got distracted because the type theory yo= u seem to be asking for
>>>>> doesn't sound cubical. Like I said, I suspect = OTT could handle hprop
>>>>> extensionality, if it doesn't already. Probabl= y ETT could too.
>>>>>
>>>>> On Saturday, July 29, 2017 at 4:08:01 AM UTC-4, Mi= chael Shulman wrote:
>>>>>>
>>>>>> As I said,
>>>>>>
>>>>>>> The motivation would be to have a type the= ory 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-p= retopos 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 cubical
>>>>>>> sets?
>>>>>>> Actually, couldn't you interpret OTT i= nto the hsets, internally to
>>>>>>> HoTT?
>>>>>>> It'd be a hassle without a real soluti= on to the infinite coherence
>>>>>>> problem,
>>>>>>> but it should work, since the h-levels inv= olved are bounded.
>>>>>>>
>>>>>>> On Saturday, July 29, 2017 at 2:20:06 AM U= TC-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 <atm...@gmail.com>
>>>>>>>> wrote:
>>>>>>>>> I'm confused. So you want a cu= bical type theory with only hsets? In
>>>>>>>>> what
>>>>>>>>> sense would there be cubes, other = than just points? I thoght OTT had
>>>>>>>>> propositional extensionality. Thou= gh maybe that's only for strict
>>>>>>>>> props.
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> On Sunday, July 23, 2017 at 6:54:3= 9 PM UTC-4, Michael Shulman wrote:
>>>>>>>>>>
>>>>>>>>>> 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 c= an prove both function extensionality
>>>>>>>>>> and propositional univalence. = =C2=A0(I am aware of Observational Type
>>>>>>>>>> Theory, which I believe has UI= P and proves function extensionality,
>>>>>>>>>> but I don't think it prove= s propositional univalence -- although I
>>>>>>>>>> would be happy to be wrong abo= ut that.)
>>>>>>>>>>
>>>>>>>>>> Presumably we obtain a cubical= type theory that's compatible with
>>>>>>>>>> axiomatic UIP if in CCHM cubic= al type theory we postulate only a
>>>>>>>>>> single universe of proposition= s. =C2=A0But I wonder about some possible
>>>>>>>>>> refinements, such as:
>>>>>>>>>>
>>>>>>>>>> 1. In this case do we still ne= ed *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 oper= ations at all higher dimensions.
>>>>>>>>>>
>>>>>>>>>> 2. Can it be enhanced to make = UIP provable, such as by adding a
>>>>>>>>>> computing K eliminator?
>>>>>>>>>>
>>>>>>>>>> Mike
------=_Part_4182_2047408322.1501522597227-- ------=_Part_4181_406860282.1501522597227--