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

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

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

Hey what about if you start with intuitionistic set theory. Use the usual 
encodings of Martin-Löf types. For the universe of propositions, use the 
subsets of your favorite singleton. You get proposition extensionality. The 
way functions are defined provides function extensionality and unique 
choice. Now consider the realizers for this system and somehow clean it up 
into a type system. If the realizers are sane, you should get canonicity. 
Does that work? It's quite different from MLTT: you don't reason about 
computations. (At least not using "propositions".)

On Saturday, July 29, 2017 at 5:19:45 PM UTC-4, 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: 5900 bytes --]