From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.185.80 with SMTP id k16mr9326758iti.1.1513530533786; Sun, 17 Dec 2017 09:08:53 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.47.79 with SMTP id j76ls2335853itj.9.canary-gmail; Sun, 17 Dec 2017 09:08:52 -0800 (PST) X-Received: by 10.107.15.65 with SMTP id x62mr1196225ioi.127.1513530532753; Sun, 17 Dec 2017 09:08:52 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513530532; cv=none; d=google.com; s=arc-20160816; b=pA8sdhWoDrPtfQEkB4a8fDj25T7WFURsHzd3TxXTPSa8VAwDKi8JhK2tmpOEsPXX6a 5tl1/zGZG86T/AJgHFOAciYFZ1Ir9mJwEZkgLAEklCYgZXruNXtro6jbVmtiKhORtXrq Zy/Al77hGZAj8hPf3hAIWdikW6PyCXG+5QL21D6A7TZnsLV/eIFDckm3mbx2qcagy5Xb FCOJQY7hB3YpZxfF0J4VPqX5W0aBBgh3zpkIejQpoBq6UzlgyZYiTYVZHMMPkb2NApu3 WIK04hbJb05QOy6n3hl915BnViSD05Ce0FAJZTVW4j9SFWjTykRw3UFfOOBOkzFk0Knn NjKw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:arc-authentication-results; bh=3uI8SQ3cq8CYZQeamkkZ0QUxx71eaT7eKQnis6lWlHM=; b=pCCNTmrO+WN6aMqCHxAS6pdrNuZHdUqkeI5+IWrB4M8o9JiD3VlgBw9Puw/asGe7dK UtTrS+YZqoF7C1wceyE2NqmenSnWlwaI793GplmxwasS3Jq26gVFlehTPNXVtPJsiqFI x+97ccq58jfM64z3kfE/LcqrJAD+kNM2dMVPdaj7lXGliI8wCr0NbU7sBOH4bkDYmGzk VUluMa35zpbcqpHIlzELQfRlTU0/rkP+J9L39/JDBp1gSfb/4Sb1+BHOmgdxwMcWx56E pQn77szi3V1XwUQnGb1kUaRBr4RiLUi7v3gk10/pkVcnsIdJ8M4AIgweESn2PXS6NVz6 yDfg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of she...@csail.mit.edu designates 128.30.2.210 as permitted sender) smtp.mailfrom=she...@csail.mit.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=csail.mit.edu Return-Path: Received: from outgoing-stata.csail.mit.edu (outgoing-stata.csail.mit.edu. [128.30.2.210]) by gmr-mx.google.com with ESMTP id x189si826755ite.2.2017.12.17.09.08.52 for ; Sun, 17 Dec 2017 09:08:52 -0800 (PST) Received-SPF: pass (google.com: domain of she...@csail.mit.edu designates 128.30.2.210 as permitted sender) client-ip=128.30.2.210; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of she...@csail.mit.edu designates 128.30.2.210 as permitted sender) smtp.mailfrom=she...@csail.mit.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=csail.mit.edu Received: from dhcp-18-189-47-201.dyn.mit.edu ([18.189.47.201]) by outgoing-stata.csail.mit.edu with esmtpsa (TLS1.2:DHE_RSA_AES_256_CBC_SHA256:256) (Exim 4.82) (envelope-from ) id 1eQcQk-0003fU-4H; Sun, 17 Dec 2017 12:08:50 -0500 From: Ben Sherman Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_C0A831A4-5BC7-4893-B960-4479FCBA346E" Mime-Version: 1.0 (Mac OS X Mail 11.2 \(3445.5.20\)) Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Date: Sun, 17 Dec 2017 12:08:49 -0500 In-Reply-To: Cc: Thorsten Altenkirch , Homotopy Type Theory To: Michael Shulman References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> <40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk> X-Mailer: Apple Mail (2.3445.5.20) --Apple-Mail=_C0A831A4-5BC7-4893-B960-4479FCBA346E Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 I don=E2=80=99t think that HProp extensionality is false in Lean (note that= regular Prop extensionality is an axiom that is taken to hold in Lean), or= at the least, I don=E2=80=99t think Thorsten=E2=80=99s argument goes throu= gh. Here is Lean code that formalizes the argument: structure HProp : Type (u + 1) :=3D (car : Type u) (subsingleton : =E2=88=80 x y : car, x =3D y) structure Sig {A : Type u} (P : A =E2=86=92 Prop) : Type u :=3D (fst : A) (snd : P fst) def Single {A : Type u} (a : A) : HProp :=3D =E2=9F=A8 Sig (=CE=BB x : A, x =3D a) , begin intros, cases x, cases y, subst snd, subst snd_1, end =E2=9F=A9 structure iffT (A B : Type u) :=3D (left : A =E2=86=92 B) (right : B =E2=86=92 A) def HProp_ext : Prop :=3D =E2=88=80 (P Q : HProp.{u}), (iffT (HProp.car P) (HProp.car Q)) =E2=86=92= P =3D Q def true_HProp : HProp.{u} :=3D =E2=9F=A8 punit , begin intros, cases x, cases y, reflexivity end =E2=9F=A9 lemma Single_inh {A : Type u} (a : A) : HProp_ext.{u} =E2=86=92 Single a = =3D true_HProp :=3D begin intros H, apply H, constructor; intros, constructor, constructor, reflexivity, end lemma Single_bool (H : HProp_ext.{0}) : Single tt =3D Single ff :=3D begin rw Single_inh, rw Single_inh, assumption, assumption, end def x (H : HProp_ext.{0}) : HProp.car (Single ff) :=3D eq.rec_on (Single_bool H) =E2=9F=A8 tt, rfl =E2=9F=A9 lemma snd_x (H : HProp_ext.{0}) : Sig.fst (x H) =3D ff :=3D Sig.snd (x H) lemma fst_x (H : HProp_ext.{0}) : Sig.fst (x H) =3D tt :=3D begin dsimp [x], admit, end The proof state at the end of the proof for `fst_x` looks like this: =E2=8A=A2 (eq.rec {fst :=3D tt, snd :=3D _} _).fst =3D tt and `reflexivity` fails to solve the goal, so I think the `eq.rec` on the l= eft-hand side fails to reduce. Note that the equality proof that we transpo= rt over is a proof that `Single tt =3D Single ff`; the two sides of this eq= uation are not definitionally equal, which I think explains why `eq.rec` ca= nnot reduce. > On Dec 17, 2017, at 7:55 AM, Michael Shulman wrote: >=20 > On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch > > wr= ote: >> Not really: you can prove =C2=B3PropExt -> False=C2=B2 in the current sy= stem and you >> shouldn=C2=B9t be able to do this. >=20 > Ah, I see. I didn't realize that PropExt was something you could > hypothesize inside of Lean; I thought you were proposing it as a > modification to the underlying type theory. In that case, yes, I > agree, the implementation is incorrect. (Are any Lean developers > listening?) >=20 >> By definitional proof-irrelevance I mean that we have a =C2=B3static=C2= =B2 universe >> of propositions and the principle that any tow proofs of propositions ar= e >> definitionally equal. That is what I suggested in my LICS 99 paper. >> However, it seems (following your comments) that we can=C2=B9t prove =C2= =B3PropExt >> -> False=C2=B2 in this system. >>=20 >> One could argue that Lean=C2=B9s type theory is defined by its implement= ation >> but then it may be hard to say anything about it, including wether it is >> consistent. >>=20 >>> I still wonder what exactly is the difference between a static >> )(efnitionally proof-irrelvant) Prop which seems to correspond to Omega = in >> a topos and set-level HoTT (i.e. using HProp). Hprop is also a subobject >> classifier (with some predicativity proviso) but the HoTT view gives you >> some extra power. >>=20 >> A prime example of that "extra power" is that with HProp you can prov= e >> function comprehension (unique choice). This goes along with a >> reduction in the class of models: I believe that a static Prop can >> also be modeled by the strong-subobject classifier in a quasitopos, i= n >> which case unique choice is false. >>=20 >> Ok, so you are saying that a static Prop only gives rise to a quasitopos >> which fits with the observation that we don't get unique choice in this >> case. On the other hand set level HoTT gives rise to a topos? >>=20 >> Thorsten >>=20 >>> Ok, once we also allow QITs we know that this goes beyond the usual >> topos logic (cf. the example in your paper with Peter). >>>=20 >>> Thorsten >>>=20 >>>=20 >>> On 12/12/2017, 23:14, "homotopyt...@googlegroups.com on behalf >> of Michael Shulman" > shu...@sandiego.edu> wrote: >>>=20 >>> This is really interesting. It's true that all toposes satisfy >> both >>> unique choice and proof irrelevance. I agree that one >> interpretation >>> is that definitional proof-irrelevance is incompatible with the >>> HoTT-style *definition* of propositions as (-1)-truncated types, >> so >>> that you can *prove* something is a proposition, rather than >> having >>> "being a proposition" being only a judgment. But could we >> instead >>> blame it on the unjustified omission of type annotations? >> Morally, a >>> pairing constructor >>>=20 >>> (-,-) : (a:A) -> B(a) -> Sum(x:A) B(x) >>>=20 >>> ought really to be annotated with the types it acts on: >>>=20 >>> (-,-)^{(a:A). B(a)} : (a:A) -> B(a) -> Sum(x:A) B(x) >>>=20 >>> and likewise the projection >>>=20 >>> first : (Sum(x:A) B(x)) -> A >>>=20 >>> should really be >>>=20 >>> first^{(a:A). B(a)} : (Sum(x:A) B(x)) -> A. >>>=20 >>> If we put these annotations in, then your "x" is >>>=20 >>> (true,refl)^{(b:Bool). true=3Db} >>>=20 >>> and your two apparently contradictory terms are >>>=20 >>> first^{(b:Bool). true=3Db} x =3D=3D true >>>=20 >>> and >>>=20 >>> second^{(b:Bool). false=3Db} x : first^{(b:Bool). false=3Db} x =3D >> false >>>=20 >>> And we don't have "first^{(b:Bool). false=3Db} x =3D=3D true", becau= se >>> beta-reduction requires the type annotations on the projection >> and the >>> pairing to match. So it's not really the same "first x" that's >> equal >>> to true as the one that's equal to false. >>>=20 >>> In many type theories, we can omit these annotations on pairing >> and >>> projection constructors because they are uniquely inferrable. >> But if >>> we end up in a type theory where they are not uniquely >> inferrable, we >>> are no longer justified in omitting them. >>>=20 >>>=20 >>> On Tue, Dec 12, 2017 at 4:21 AM, Thorsten Altenkirch >>> wrote: >>>> Good point. >>>>=20 >>>> OK, in a topos you have a static universe of propositions. >> That is wether something is a proposition doesn=C2=B9t depend on other >> assumptions you make. >>>>=20 >>>> In set-level HoTT we define Prop as the types which have at >> most one inhabitant. Now wether a type is a proposition may depend on >> other assumptions. (-1)-univalence i.e. propositional extensionality tur= ns >> Prop into a subobject classifier (if you have resizing otherwise you get >> some sort of predicative topos). >>>>=20 >>>> However, the dynamic interpretation of propositions gives you >> some additional power, in particular you can proof unique choice, becaus= e >> if you can prove Ex! x:A.P x , where Ex! x:A.P x is defined as Sigma x:A= .P >> x /\ Pi y:A.P y -> x=3Dy then this is a proposition even though A may no= t >> be. However using projections you also get Sigma x:A.P x. >>>>=20 >>>> Hence I guess I should have said a topos with unique choice (I >> am not sure wether this is enough). Btw, set-level HoTT also gives you >> QITs which eliminate many uses of choice (e.g. the definition of the >> Cauchy Reals and the partiality monad). >>>>=20 >>>> Thorsten >>>>=20 >>>>=20 >>>>=20 >>>>=20 >>>>=20 >>>>=20 >>>> On 12/12/2017, 12:02, "Thomas Streicher" >> wrote: >>>>=20 >>>>> But very topos is a model of extensional type theory when >> taking Prop >>>>> =3D Omega. All elements of Prop are proof irrelevant and >> equivalent >>>>> propositions are equal. >>>>>=20 >>>>> Since it is a model of extensional TT there is no difference >> between >>>>> propsoitional and judgemental equality. >>>>>=20 >>>>> Thomas >>>>>=20 >>>>>=20 >>>>>> If you have proof-irrelevance in the strong definitional >> sense then you cannot be in a topos. This came up recently in the contex= t >> of Lean which is a type-theory based interactive proof system developed = at >> microsoft and which does implement proof-irrelvance. Note that any topos >> has extProp: >>>>>>=20 >>>>>> Given a:A define Single(a) =3D Sigma x:A.a=3Dx. We have >> Single(a) : Prop and >>>>>>=20 >>>>>> p : Single(true) <-> Single(false) >>>>>>=20 >>>>>> since both are inhabited. Hence by extProp >>>>>>=20 >>>>>> extProp p : Single(true) =3D Single(false) >>>>>>=20 >>>>>> now we can use transport on (true,refl) : Single(true) to >> obtain >>>>>>=20 >>>>>> x =3D (extProp p)*(true,refl) : Single(false) >>>>>>=20 >>>>>> and we can show that >>>>>>=20 >>>>>> second x : first x =3D false >>>>>>=20 >>>>>> but since Lean computationally ignores (extProp p)* we also >> get (definitionally): >>>>>>=20 >>>>>> first x =3D=3D true >>>>>>=20 >>>>>> My conclusion is that strong proof-irrelvance is a bad idea >> (note that my ???99 paper on Extensionality in Intensional Type Theory >> used exactly this). It is more important that our core theory is >> extensional and something pragmatically close to definitional >> proof-irrelevance can be realised as some tactic based sugar. It has no >> role in a foundational calculus. >>>>>>=20 >>>>>>=20 >>>>>> Thorsten >>>>>>=20 >>>>>>=20 >>>>>>=20 >>>>>>=20 >>>>>> On 12/12/2017, 10:15, "Andrea Vezzosi" >> wrote: >>>>>>=20 >>>>>>> On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch >>>>>>> wrote: >>>>>>>> Hi Kristina, >>>>>>>>=20 >>>>>>>> I guess you are not assuming Prop:Set because that would >> be System U and hence inconsistent. >>>>>>>>=20 >>>>>>>> By proof-irrelevance I assume that you mean that any two >> inhabitants of a proposition are definitionally equal. This assumption i= s >> inconsistent with it being a tops since in any Topos you get proposition= al >> extensionality, that is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is in= deed >> an instance of univalence. >>>>>>>>=20 >>>>>>>=20 >>>>>>> I don't know if it's relevant to the current discussion, >> but I thought >>>>>>> the topos of sets with Prop taken to be the booleans would >> support >>>>>>> both proof irrelevance and propositional extensionality, >> classically >>>>>>> at least. Is there some extra assumption I am missing here? >>>>>>>=20 >>>>>>>=20 >>>>>>>> It should be possible to use a realizability semantics >> like omega-sets or Lambda-sets to model the impredicative theory and >> identify the propositions with PERs that are just subsets. >>>>>>>>=20 >>>>>>>> Cheers, >>>>>>>> Thorsten >>>>>>>>=20 >>>>>>>>=20 >>>>>>>> On 11/12/2017, 04:22, >> "homotopyt...@googlegroups.com on behalf of Kristina Sojakova" >> > sojakova...@gmail.com> wrote: >>>>>>>>=20 >>>>>>>> Dear all, >>>>>>>>=20 >>>>>>>> I asked this question last year on the coq-club >> mailing list but did not >>>>>>>> receive a conclusive answer so I am trying here now. >> Is the theory with >>>>>>>> a proof-relevant impredicative universe Set, >> proof-irrelevant >>>>>>>> impredicative universe Prop, and function >> extensionality (known to be) >>>>>>>> consistent? It is known that the proof-irrelevance of >> Prop makes the Id >>>>>>>> type behave differently usual and in particular, >> makes the theory >>>>>>>> incompatible with univalence, so it is not just a >> matter of tacking on >>>>>>>> an interpretation for Prop. >>>>>>>>=20 >>>>>>>> Thanks in advance for any insight, >>>>>>>>=20 >>>>>>>> Kristina >>>>>>>>=20 >>>>>>>>=20 >>>>>>>>=20 >>>>>>>>=20 >>>>>>>>=20 >>>>>>>>=20 >>>>>>>>=20 >>>>>>>> This message and any attachment are intended solely for >> the addressee >>>>>>>> and may contain confidential information. If you have >> received this >>>>>>>> message in error, please send it back to me, and >> immediately delete it. >>>>>>>>=20 >>>>>>>> Please do not use, copy or disclose the information >> contained in this >>>>>>>> message or in any attachment. Any views or opinions >> expressed by the >>>>>>>> author of this email do not necessarily reflect the views >> of the >>>>>>>> University of Nottingham. >>>>>>>>=20 >>>>>>>> This message has been checked for viruses but the >> contents of an >>>>>>>> attachment may still contain software viruses which could >> damage your >>>>>>>> computer system, you are advised to perform your own >> checks. Email >>>>>>>> communications with the University of Nottingham may be >> monitored as >>>>>>>> permitted by UK legislation. >>>>>>>>=20 >>>>>>=20 >>>>>>=20 >>>>>>=20 >>>>>>=20 >>>>>> This message and any attachment are intended solely for the >> addressee >>>>>> and may contain confidential information. If you have >> received this >>>>>> message in error, please send it back to me, and immediately >> delete it. >>>>>>=20 >>>>>> Please do not use, copy or disclose the information >> contained in this >>>>>> message or in any attachment. Any views or opinions >> expressed by the >>>>>> author of this email do not necessarily reflect the views of >> the >>>>>> University of Nottingham. >>>>>>=20 >>>>>> This message has been checked for viruses but the contents >> of an >>>>>> attachment may still contain software viruses which could >> damage your >>>>>> computer system, you are advised to perform your own checks. >> Email >>>>>> communications with the University of Nottingham may be >> monitored as >>>>>> permitted by UK legislation. >>>>>>=20 >>>>=20 >>>>=20 >>>>=20 >>>>=20 >>>> This message and any attachment are intended solely for the >> addressee >>>> and may contain confidential information. If you have received >> this >>>> message in error, please send it back to me, and immediately >> delete it. >>>>=20 >>>> Please do not use, copy or disclose the information contained >> in this >>>> message or in any attachment. Any views or opinions expressed >> by the >>>> author of this email do not necessarily reflect the views of >> the >>>> University of Nottingham. >>>>=20 >>>> This message has been checked for viruses but the contents of >> an >>>> attachment may still contain software viruses which could >> damage your >>>> computer system, you are advised to perform your own checks. >> Email >>>> communications with the University of Nottingham may be >> monitored as >>>> permitted by UK legislation. >>>>=20 >>>> -- >>>> You received this message because you are subscribed to the >> Google Groups "Homotopy Type Theory" group. >>>> To unsubscribe from this group and stop receiving emails from >> it, send an email to HomotopyTypeThe...@googlegroups.com. >>>> For more options, visit https://groups.google.com/d/optout. >>>=20 >>> -- >>> You received this message because you are subscribed to the >> Google Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from >> it, send an email to HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >>>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>> This message and any attachment are intended solely for the addressee >>> and may contain confidential information. If you have received this >>> message in error, please send it back to me, and immediately delete >> it. >>>=20 >>> Please do not use, copy or disclose the information contained in this >>> message or in any attachment. Any views or opinions expressed by the >>> author of this email do not necessarily reflect the views of the >>> University of Nottingham. >>>=20 >>> This message has been checked for viruses but the contents of an >>> attachment may still contain software viruses which could damage your >>> computer system, you are advised to perform your own checks. Email >>> communications with the University of Nottingham may be monitored as >>> permitted by UK legislation. >>>=20 >>> -- >>> You received this message because you are subscribed to the Google >> Groups "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, >> send an email to HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >>=20 >>=20 >>=20 >>=20 >>=20 >>=20 >>=20 >> This message and any attachment are intended solely for the addressee >> and may contain confidential information. If you have received this >> message in error, please send it back to me, and immediately delete it. >>=20 >> Please do not use, copy or disclose the information contained in this >> message or in any attachment. Any views or opinions expressed by the >> author of this email do not necessarily reflect the views of the >> University of Nottingham. >>=20 >> This message has been checked for viruses but the contents of an >> attachment may still contain software viruses which could damage your >> computer system, you are advised to perform your own checks. Email >> communications with the University of Nottingham may be monitored as >> permitted by UK legislation. >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 > --=20 > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout . --Apple-Mail=_C0A831A4-5BC7-4893-B960-4479FCBA346E Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 I don=E2=80=99t think that= HProp extensionality is false in Lean (note that regular Prop extensionali= ty is an axiom that is taken to hold in Lean), or at the least, I don=E2=80= =99t think Thorsten=E2=80=99s argument goes through. Here is Lean code that= formalizes the argument:

structure HProp : Type (u + 1) :=3D  (car : Type u)
  (subsingl= eton : =E2=88=80 x y : car, x =3D y)

structure Sig {A : Type u} (P : A =E2= =86=92 Prop) : Type u :=3D
  (fst : = A)
  (snd : P fst)

def = ;Single {A : Type u} (a : A) : HProp :=3D
  =E2=9F=A8 Sig (=CE=BB x : A, x =3D a)
 = ; , begin
    intros, cases x, cases y,
    subst snd, subst snd_1,
   &n= bsp;end
  =E2=9F=A9

structu= re iffT (A B : Type u) :=3D
  (= left : A =E2=86=92 B)
  (right : B =E2=86= =92 A)

def HProp_ext : Pro= p :=3D
  =E2=88=80 (P Q : HProp.{u}), (if= fT (HProp.car P) (HProp.car Q)) =E2=86=92 P =3D Q

def true_HProp : HProp.{u} :=3D = ;=E2=9F=A8 punit ,
  begin intros, cases x, ca= ses y, reflexivity end  =E2=9F=A9

le= mma Single_inh {A : Type u} (a : A) : HProp_ext.{u}&nbs= p;=E2=86=92 Single a =3D true_HProp :=3D
= begin
intros H,
apply H, constructor; intros,constructor, constructor, reflexivity,
end

lemma Single_bool (H : HProp_ext.{0}) : S= ingle tt =3D Single ff :=3D
begin
rw Single_inh, rw Single_inh, assumption, assumption,
end
def x (H : HProp_ext.{0}) :
  HProp.car (Single ff) :=3D
  eq.rec_on= (Single_bool H) =E2=9F=A8 tt, rfl =E2=9F=A9

l= emma snd_x (H : HProp_ext.{0}) : Sig.fst (x H) =3D ff&n= bsp;:=3D Sig.snd (x H)

lemma fst_x&n= bsp;(H : HProp_ext.{0}) : Sig.fst (x H) =3D tt :=3D beg= in
dsimp [x], admit,
end
<= br class=3D"">
The proof state at the end of the proof= for `fst_x` looks like this:

=E2=8A=A2 (eq.rec {fst :=3D tt, snd :=3D _} _).fst =3D tt

and `reflexivity` fai= ls to solve the goal, so I think the `eq.rec` on the left-hand side fails t= o reduce. Note that the equality proof that we transport over is a proof th= at `Single tt =3D Single ff`; the two sides of this equation are not defini= tionally equal, which I think explains why `eq.rec` cannot reduce.

On Dec 17, 2017, at 7:55 AM, Michael Shulman <shu...@sandiego.edu> wrote:

On Sat, Dec 16, 2017 at 7:21 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
Not really: you can prove =C2=B3PropE= xt -> False=C2=B2 in the current system and you
shouldn=C2= =B9t be able to do this.

Ah= , I see.  I didn't realize that PropExt was something you could=
hypothesize inside of Lean; I thought you were proposi= ng it as a
modification to the underlying type t= heory.  In that case, yes, I
agree, the imp= lementation is incorrect.  (Are any Lean developers
listening?)

By definitional proof-irrelevance I mean that we have a =C2=B3static=C2= =B2 universe
of propositions and the principle that any tow p= roofs of propositions are
definitionally equal. That is what = I suggested in my LICS 99 paper.
However, it seems (following= your comments) that we can=C2=B9t prove =C2=B3PropExt
-> = False=C2=B2 in this system.

One could argue th= at Lean=C2=B9s type theory is defined by its implementation
b= ut then it may be hard to say anything about it, including wether it is
consistent.

I still wonder what exactly is the difference between a stati= c
)(efnitionally proof-irrelvant) Prop which see= ms to correspond to Omega in
a topos and set-level HoTT (i.e.= using HProp). Hprop is also a subobject
classifier (with som= e predicativity proviso) but the HoTT view gives you
some ext= ra power.

   A prime example of= that "extra power" is that with HProp you can prove
 &n= bsp; function comprehension (unique choice).  This goes along wit= h a
   reduction in the class of models: I bel= ieve that a static Prop can
   also be modeled= by the strong-subobject classifier in a quasitopos, in
 = ;  which case unique choice is false.

Ok, so you are saying that a static Prop only gives rise to a quasitopos<= br class=3D"">which fits with the observation that we don't get unique choi= ce in this
case. On the other hand set level HoTT gives rise = to a topos?

Thorsten

Ok, once we also allow QITs we k= now that this goes beyond the usual
topos logic = (cf. the example in your paper with Peter).

Thorsten

<= br class=3D"">On 12/12/2017, 23:14, "homotopyt...@googlegroups.com on behalf
of Michael Shulman" <homotopyt...@googlegroups.com on behalf of<= br class=3D"">shu...@sand= iego.edu> wrote:
=
   This is really interesting.  It's tru= e that all toposes satisfy
both
   unique choice and proo= f irrelevance.  I agree that one
interpreta= tion
   i= s that definitional proof-irrelevance is incompatible with the
   HoTT-style *definition* of propositions as (-1)-truncat= ed types,
so
   that you can *prove* something is a propo= sition, rather than
having
   "being a proposition" being= only a judgment.  But could we
instead
   blame it = on the unjustified omission of type annotations?
Morally, a
  =  pairing constructor

   (-= ,-) : (a:A) -> B(a) -> Sum(x:A) B(x)

&nb= sp;  ought really to be annotated with the types it acts on:

   (-,-)^{(a:A). B(a)} : (a:A) ->= ; B(a) -> Sum(x:A) B(x)

   a= nd likewise the projection

   f= irst : (Sum(x:A) B(x)) -> A

  &nb= sp;should really be

   first^{(= a:A). B(a)} : (Sum(x:A) B(x)) -> A.

 &= nbsp; If we put these annotations in, then your "x" is
<= br class=3D"">   (true,refl)^{(b:Bool). true=3Db}

   and your two apparently contradictor= y terms are

   first^{(b:Bool).= true=3Db} x =3D=3D true

   and=

   second^{(b:Bool). false=3Db= } x : first^{(b:Bool). false=3Db} x =3D
false

  = ; And we don't have "first^{(b:Bool). false=3Db} x =3D=3D true", becau= se
   beta-reduction requires the type annotat= ions on the projection
and the
   pairing to match.  = ;So it's not really the same "first x" that's
eq= ual
   to= true as the one that's equal to false.

 =   In many type theories, we can omit these annotations on pairing=
and
   projection constructors because they are uniquely= inferrable.
But if
   we end up in a type theory where t= hey are not uniquely
inferrable, we
   are no longer just= ified in omitting them.


 &= nbsp; On Tue, Dec 12, 2017 at 4:21 AM, Thorsten Altenkirch
   <Thorsten....@nottingham.ac.uk> wrote:
Good point.

OK,= in a topos you have a static universe of propositions.
That is wether something is a proposition doesn=C2=B9t= depend on other
assumptions you make.

In set-level HoTT we define Prop as the types which have at
most one inhabitant. Now wether a type is a= proposition may depend on
other assumptions. (-1)-univalence= i.e. propositional extensionality turns
Prop into a subobjec= t classifier (if you have resizing otherwise you get
some sor= t of predicative topos).

However, the dynamic i= nterpretation of propositions gives you
some additional power, in particular you can proof unique choice, beca= use
if you can prove Ex! x:A.P x , where Ex! x:A.P x is defin= ed as Sigma x:A.P
x /\ Pi y:A.P y -> x=3Dy then this is a = proposition even though A may not
be. However using projectio= ns you also get Sigma x:A.P x.

Hence I guess I = should have said a topos with unique choice (I
<= /blockquote>am not sure wether this is enough). Btw, set-level HoTT also gi= ves you
QITs which eliminate many uses of choice (e.g. the de= finition of the
Cauchy Reals and the partiality monad).

Thorsten






On 12/12/2017,= 12:02, "Thomas Streicher"
<stre...@mathem= atik.tu-darmstadt.de> wrote:

But very topos is a model of extensional type the= ory when
taking Prop
=3D Omega. All elements of= Prop are proof irrelevant and
equivalent
propo= sitions are equal.

Since it is a model of exte= nsional TT there is no difference
<= /blockquote>between
props= oitional and judgemental equality.

Thomas


If you have proof-irrelevance in the strong definitional
sense then you cannot be = in a topos. This came up recently in the context
of Lean whic= h is a type-theory based interactive proof system developed at
microsoft and which does implement proof-irrelvance. Note that any topos<= br class=3D"">has extProp:

Given a:A define Sing= le(a) =3D Sigma x:A.a=3Dx. We have
=
Single(a) : Prop and

p= : Single(true) <-> Single(false)

since = both are inhabited. Hence by extProp

extProp p= : Single(true) =3D Single(false)

now we can u= se transport on (true,refl) : Single(true) to
obtain

x = =3D (extProp p)*(true,refl) : Single(false)

an= d we can show that

second x : first x =3D fals= e

but since Lean computationally ignores (extP= rop p)* we also
get (definitionally):

first x =3D=3D tr= ue

My conclusion is that strong proof-irrelvan= ce is a bad idea
(note that my ???99 paper on Extensionality in Intensional Type The= ory
used exactly this). It is more important that our core th= eory is
extensional and something pragmatically close to defi= nitional
proof-irrelevance can be realised as some tactic bas= ed sugar. It has no
role in a foundational calculus.


Thorsten

<= br class=3D"">

On 12/12/2017, 10:15, "Andrea V= ezzosi" <sanz...@gmail.c= om>
wrote:

On= Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch
<Thorsten....@nottingh= am.ac.uk> wrote:
= Hi Kristina,

I guess you are not assuming Prop= :Set because that would
be System U and hence inconsistent= .

By proof-irrelevance I assume that you mean tha= t any two
inhabitants of a proposition are definitionally = equal. This assumption is
inconsistent with it being a tops s= ince in any Topos you get propositional
extensionality, that = is P,Q : Prop, (P <-> Q) <-> (P =3D Q), which is indeed
an instance of univalence.

I don't know if it's relevant to the current discussion,
b= ut I thought
the topos of = sets with Prop taken to be the booleans would
support
both proof irrelevance and propositional ex= tensionality,
classically
at least. Is there some extra assumption I am missing here?


It= should be possible to use a realizability semantics
like = omega-sets or Lambda-sets to model the impredicative theory and
identify the propositions with PERs that are just subsets.
=
<= blockquote type=3D"cite" class=3D"">
Cheers,
Thorsten

On 11/12/2017, 04:22,
=
"homotopyt...@googlegroups.com on = behalf of Kristina Sojakova"
<homotopyt...@googlegroups.com on behalf= of
sojak= ova...@gmail.com> wrote:

   = ;Dear all,

   I asked this ques= tion last year on the coq-club
mailing list but did not
   receive a conclusive answer so I am trying here = now.
Is the theory with
   a pro= of-relevant impredicative universe Set,
proof-irrelevant
   impredicative universe Prop, and function
<= /blockquote>extensionality (known to be)
   consi= stent? It is known that the proof-irrelevance of
Prop make= s the Id
   type behave differently usual and in= particular,
makes the theory
   = ;incompatible with univalence, so it is not just a
matter = of tacking on
   an interpretation for Prop.

   Thanks in advance for any insigh= t,

   Kristina





This message and any attachment are intended so= lely for
=
the addressee
and may contain confiden= tial information. If you have
received this
=
<= blockquote type=3D"cite" class=3D"">
mes= sage in error, please send it back to me, and
immediately = delete it.

Please do not use, copy or disclose th= e information
contained in this
message or in a= ny attachment.  Any views or opinions
expressed by th= e
author of this email do not necessarily reflect the views
=
of the
University of Nottingham.

This message has been checked for viruses but the
=
contents of an
attachment may still contain software viruses = which could
damage your
computer system, you ar= e advised to perform your own
checks. Email
=
<= blockquote type=3D"cite" class=3D"">
com= munications with the University of Nottingham may be
monit= ored as
permitted by UK legislation.





This message and any attachment are intended solely for th= e
address= ee
and may contain confidential information. If you have
received this
message in error, please send it back to me, and immediately
delete it.

Please do not use, copy or disclose the informati= on
contai= ned in this
message or in any attachment.  Any views or op= inions
ex= pressed by the
author of this email do not necessarily reflect = the views of
the
University of Nottingham.

This message has been checked for viruses but the contents
<= /blockquote>
of an
attach= ment may still contain software viruses which could
damage your
computer= system, you are advised to perform your own checks.
Email
communication= s with the University of Nottingham may be
monitored as
permitted by UK = legislation.





This message and any a= ttachment are intended solely for the
addressee
and may contain confidential information. If you = have received
this
mes= sage in error, please send it back to me, and immediately
delete it.

Please do not= use, copy or disclose the information contained
in this
message or in any attachment.  Any = views or opinions expressed
by the<= br class=3D"">
author of this email do not necessarily reflect the views of
the
University of Not= tingham.

This message has been checked for vir= uses but the contents of
an
attachment may still contain software viruses which could
damage your
computer system, you = are advised to perform your own checks.
Email
communications with the University of Nottingham ma= y be
monitored as
perm= itted by UK legislation.

--
You = received this message because you are subscribed to the
Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from
it, send an email to HomotopyTypeThe...@googlegroup= s.com.
For more options, visit https://groups.google.com/d/optout.

   --
&n= bsp;  You received this message because you are subscribed to the=
Google Groups "Homotopy Type Theory" group.
   To unsubs= cribe from this group and stop receiving emails from
it, send an email to HomotopyTypeThe...@googlegroups.com.
   For more options, visit= https://groups.g= oogle.com/d/optout.






This message and any a= ttachment are intended solely for the addressee
and may conta= in confidential information. If you have received this
messag= e in error, please send it back to me, and immediately delete
it.

Please do not use, copy or disclose the information contained in t= his
message or in any attachment.  Any views or opinions= expressed by the
author of this email do not necessarily ref= lect the views of the
University of Nottingham.

This message has been checked for viruses but the contents = of an
attachment may still contain software viruses which cou= ld damage your
computer system, you are advised to perform yo= ur own checks. Email
communications with the University of No= ttingham may be monitored as
permitted by UK legislation.

--
You received this message becaus= e you are subscribed to the Google
Groups "Homot= opy Type Theory" group.
= To unsubscribe from this group and stop receiving emails from it,
send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.co= m/d/optout.






Th= is message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this<= br class=3D"">message in error, please send it back to me, and immediately = delete it.

Please do not use, copy or disclose= the information contained in this
message or in any attachme= nt.  Any views or opinions expressed by the
author of th= is email do not necessarily reflect the views of the
Universi= ty of Nottingham.

This message has been checke= d for viruses but the contents of an
attachment may still con= tain software viruses which could damage your
computer system= , you are advised to perform your own checks. Email
communica= tions with the University of Nottingham may be monitored as
p= ermitted by UK legislation.

--
Y= ou received this message because you are subscribed to the Google Groups "H= omotopy Type Theory" group.
To unsubscribe from this group an= d stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.co= m.
For more options, visit https://groups.google.com/d/optout.

-- 
You received this message be= cause you are subscribed to the Google Groups "Homotopy Type Theory" group.=
To unsubscribe from this group and stop receivi= ng emails from it, send an email to&n= bsp;HomotopyTypeThe...@googlegroups= .com.
For mo= re options, visit = https://groups.google.com/d/optout.

<= /html> --Apple-Mail=_C0A831A4-5BC7-4893-B960-4479FCBA346E--