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

[Jon Sterling <j...@jonmsterling.com>]

On Fri, Jul 28, 2017, at 06: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.

I think 'propositional extensionality' in OTT was for objects which were
propositions *by definition*, as opposed to h-props in HoTT (which is
something that you prove about a type, and doesn't merely follow from
the intension of the type).

Best,
Jon

> 
> 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
> >
> 
> -- 
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.