From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 1 Aug 2017 14:27:42 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <8e016296-dcb6-4596-af91-255f564fad2b@googlegroups.com> In-Reply-To: References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> Subject: Re: [HoTT] Re: cubical type theory with UIP MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_5579_538061125.1501622862568" ------=_Part_5579_538061125.1501622862568 Content-Type: multipart/alternative; boundary="----=_Part_5580_461782216.1501622862568" ------=_Part_5580_461782216.1501622862568 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On Monday, July 31, 2017 at 11:51:18 AM UTC-4, Michael Shulman wrote: > > I'm not quite sure what a "strict proposition" is, but if you mean > having a type of propositions that doesn't include all of them, then > the reason that's not enough for me is that frequently in univalent > type theory we encounter types that we *prove* to be propositions even > though they are not "given as such", such as "being contractible" and > "being a proposition", and this is responsible for a significant > amount of the unique flavor and usefulness of univalent type theory. > > For semantic reasons I wouldn't want to use intuitionistic set theory, > because it doesn't naturally occur as the internal language of > categories. You can perform contortions to model it therein, but that > involves interpreting it into type theory rather than the other way > around. I don't know what you mean by "somehow clean it up into a > type system", but if you can do that cleaning up and obtain a type > theory (a "formal type theory" in Bob Harper's sense, not a > "computational type theory", i.e. one that is inductively generated by > rules rather than assigning types to untyped terms in an "intended > semantics"), then I'd like to see it. > I'm thinking it would look a lot like OTT, but with unique choice for strict props. Not all subsingletons are strict props, so they would not be subject to propositional extensionality. So this is apparently not what you want. However, I'm not very confident about all that. I wouldn't be that surprised if it worked out differently. (In particular, something OTT-like, but with unique choice may not even make sense.) But I don't think it'll be what you want, in any case. I've lost interest in that approach. ------=_Part_5580_461782216.1501622862568 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Monday, July 31, 2017 at 11:51:18 AM UTC-4, Michael Shu= lman wrote:
I'm not quite s= ure what a "strict proposition" is, but if you mean
having a type of propositions that doesn't include all of them, the= n
the reason that's not enough for me is that frequently in univalent
type theory we encounter types that we *prove* to be propositions even
though they are not "given as such", such as "being cont= ractible" and
"being a proposition", and this is responsible for a signific= ant
amount of the unique flavor and usefulness of univalent type theory.

For semantic reasons I wouldn't want to use intuitionistic set theo= ry,
because it doesn't naturally occur as the internal language of
categories. =C2=A0You can perform contortions to model it therein, but = that
involves interpreting it into type theory rather than the other way
around. =C2=A0I don't know what you mean by "somehow clean it = up into a
type system", but if you can do that cleaning up and obtain a type
theory (a "formal type theory" in Bob Harper's sense, not= a
"computational type theory", i.e. one that is inductively gen= erated by
rules rather than assigning types to untyped terms in an "intended
semantics"), then I'd like to see it.
I'm thinking it would look a lot like OTT, but with unique choice for = strict props. Not all subsingletons are strict props, so they would not be = subject to propositional extensionality. So this is apparently not what you= want.

However, I'm not very confident about all that. I wouldn&= #39;t be that surprised if it worked out differently. (In particular, somet= hing OTT-like, but with unique choice may not even make sense.) But I don&#= 39;t think it'll be what you want, in any case. I've lost interest = in that approach.
------=_Part_5580_461782216.1501622862568-- ------=_Part_5579_538061125.1501622862568--