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