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