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