From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sat, 29 Jul 2017 00:29:37 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <1501295143.1889059.1056222744.2C07029A@webmail.messagingengine.com> References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1501295143.1889059.1056222744.2C07029A@webmail.messagingengine.com> Subject: Re: [HoTT] Re: cubical type theory with UIP MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2370_701755930.1501313377197" ------=_Part_2370_701755930.1501313377197 Content-Type: multipart/alternative; boundary="----=_Part_2371_10560293.1501313377197" ------=_Part_2371_10560293.1501313377197 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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. ------=_Part_2371_10560293.1501313377197 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 7bit
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.
------=_Part_2371_10560293.1501313377197-- ------=_Part_2370_701755930.1501313377197--