On Friday, July 28, 2017 at 10:25:44 PM UTC-4, Jonathan Sterling wrote:

On Fri, Jul 28, 2017, at 06:47 PM, Matt Oliveri 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.

I think 'propositional extensionality' in OTT was for objects which were
propositions *by definition*, as opposed to h-props in HoTT (which is
something that you prove about a type, and doesn't merely follow from
the intension of the type).

Right, that's what I meant by strict props. If so, it still seems like it should work to redefine equality for types such that hprops are quotiented based on logical equivalence, and equality of other types is left alone.