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 
> <javascript:>> 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
>