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
>