From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 20 Dec 2017 16:42:16 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <318cbeff-e7f2-4c45-b3c4-f392a94dd09d@googlegroups.com> In-Reply-To: <20171220114104.GG8054@mathematik.tu-darmstadt.de> References: <20171218115228.GB29410@mathematik.tu-darmstadt.de> <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> <20171219153118.GA9218@mathematik.tu-darmstadt.de> <20171219163139.GB13875@mathematik.tu-darmstadt.de> <20171220110052.GC8054@mathematik.tu-darmstadt.de> <5B8F4A6C-DD7C-4A14-812C-4AEA35C41BEA@exmail.nottingham.ac.uk> <20171220114104.GG8054@mathematik.tu-darmstadt.de> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_3210_1805281399.1513816936833" ------=_Part_3210_1805281399.1513816936833 Content-Type: multipart/alternative; boundary="----=_Part_3211_637711593.1513816936833" ------=_Part_3211_637711593.1513816936833 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Hi Thorsten and Thomas, It still looks to me like you're talking about different things and having a misunderstanding. By "propositional extensionality", Thorsten seems to mean the special case of univalence that applies to hprops. (Which he's simply calling propositions.) But it sounds like Thomas is counting "propositional extensionality" as a separate principle from univalence, for a type of static props. I think the system Thorsten has in mind presents a (pre)topos as a univalent type system, where hprops are used *instead of* a type of static props. But maybe not, and I'm misunderstanding. On Wednesday, December 20, 2017 at 6:41:14 AM UTC-5, Thomas Streicher wrote: > > Hi Thorsten, > > > we have already established that my argument was incorrect (for the > > reasons you state) and I was misinformed about the behaviour of > > Lean. > > I know, I just wanted to spot where the problem precisely is. > > > >Another gap in Thorsten's argument is the following. Though Single(a) > and > > >Single(a') are isomorphic in order to conclude that they are > propositionally > > >equal they would have to be elements of a univalent universe BUT I > don't see > > >where such a universe should come from in the general topos case! > > > I don???t understand this point. In a type theoretic implementation of a > topos Single(a) and Single(a???) would be propositionally equal due to > propositional extensionality. The only additional assumption I need to make > is that the universe of proposition is strict, e.g. we have that El(A -> B) > is definitionally equal to EL(A) -> El(B). This seems to be quite natural > from the point of type theory where universes are usually strict and > moreover this is true in any univalent category giving rise to a topos. > > Well, Single(a) and Single(a') were propsitionally equal if they were > elements of a univalent universe U but where should this come from if > you start from an elementary topos in a univalent metatheory. > > Thomas > ------=_Part_3211_637711593.1513816936833 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hi Thorsten and Thomas,

It still looks to me like y= ou're talking about different things and having a misunderstanding.
= By "propositional extensionality", Thorsten seems to mean the spe= cial case of univalence that applies to hprops. (Which he's simply call= ing propositions.) But it sounds like Thomas is counting "propositiona= l extensionality" as a separate principle from univalence, for a type = of static props. I think the system Thorsten has in mind presents a (pre)to= pos as a univalent type system, where hprops are used *instead of* a type o= f static props.

But maybe not, and I'm misunderstanding.

= On Wednesday, December 20, 2017 at 6:41:14 AM UTC-5, Thomas Streicher wrote= :
Hi Thorsten,

> we have already established that my argument was incorrect (for th= e
> reasons you state) and I was misinformed about the behaviour of
> Lean.

I know, I just wanted to spot where the problem precisely is.

> >Another gap in Thorsten's argument is the following. Thoug= h Single(a) and
> >Single(a') are isomorphic in order to conclude that they a= re propositionally
> >equal they would have to be elements of a univalent universe B= UT I don't see
> >where such a universe should come from in the general topos ca= se!

> I don???t understand this point. In a type theoretic implementatio= n of a topos Single(a) and Single(a???) would be propositionally equal due = to propositional extensionality. The only additional assumption I need to m= ake is that the universe of proposition is strict, e.g. we have that El(A -= > B) is definitionally equal to =C2=A0EL(A) -> El(B). This seems to b= e quite natural from the point of type theory where universes are usually s= trict and moreover this is true in any univalent category giving rise to a = topos.=20

Well, Single(a) and Single(a') were propsitionally equal if they we= re
elements of a univalent universe U but where should this come from if
you start from an elementary topos in a univalent metatheory.

Thomas
------=_Part_3211_637711593.1513816936833-- ------=_Part_3210_1805281399.1513816936833--