Re: [HoTT] Re: cubical type theory with UIP

[Matt Oliveri <atm...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 7816 bytes --]

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 <atm...@gmail.com 
> <javascript:>> wrote: 
> > On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo <m.e...@cs.bham.ac.uk 
> <javascript:>> 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 <atm...@gmail.com 
> <javascript:>> 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 <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 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 <atm...@gmail.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 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
>

[-- Attachment #1.2: Type: text/html, Size: 10867 bytes --]