Thank you, Ben! That is good news actually.
Thorsten
From: Ben Sherman <she...@csail.mit.edu>
Date: Sunday, 17 December 2017 at 18:08
To: Michael Shulman <shu...@sandiego.edu>
Cc: Thorsten Altenkirch <psz...@exmail.nottingham.ac.uk >, Homotopy Type Theory <homotopytypetheory@googlegroups.com >
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?
I don’t 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’t think Thorsten’s argument goes through. Here is Lean code that formalizes the argument:
structure HProp : Type (u + 1):=
(car : Type u)
(subsingleton : ∀ x y : car, x = y)
structure Sig {A : Type u} (P : A → Prop) : Type u :=
(fst : A)
(snd : P fst)
def Single {A : Type u} (a : A) : HProp :=
⟨ Sig (λ x : A, x = a)
, begin
intros, cases x, cases y,
subst snd, subst snd_1,
end
⟩
structure iffT (A B : Type u) :=
(left : A → B)
(right : B → A)
def HProp_ext : Prop :=
∀ (P Q : HProp.{u}), (iffT (HProp.car P) (HProp.car Q)) → P = Q
def true_HProp : HProp.{u} := ⟨ punit ,
begin intros, cases x, cases y, reflexivity end ⟩
lemma Single_inh {A : Type u} (a : A) : HProp_ext.{u} → Single a = true_HProp :=
begin
intros H,
apply H, constructor; intros,
constructor, constructor, reflexivity,
end
lemma Single_bool (H : HProp_ext.{0}) : Single tt = Single ff :=
begin
rw Single_inh, rw Single_inh, assumption, assumption,
end
def x (H : HProp_ext.{0}) :
HProp.car (Single ff) :=
eq.rec_on (Single_bool H) ⟨ tt, rfl ⟩
lemma snd_x (H : HProp_ext.{0}) : Sig.fst (x H) = ff := Sig.snd (x H)
lemma fst_x (H : HProp_ext.{0}) : Sig.fst (x H) = tt := begin
dsimp [x], admit,
end
The proof state at the end of the proof for `fst_x` looks like this:
⊢ (eq.rec {fst := tt, snd := _} _).fst = tt
and `reflexivity` fails to solve the goal, so I think the `eq.rec` on the left-hand side fails to reduce. Note that the equality proof that we transport over is a proof that `Single tt = Single ff`; the two sides of this equation are not definitionally 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.Altenkirch@nottingham.ac.uk > wrote:
Not really: you can prove ³PropExt -> False² in the current system and you
shouldn¹t 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 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?)
By definitional proof-irrelevance I mean that we have a ³static² universe
of propositions and the principle that any tow proofs of propositions are
definitionally equal. That is what I suggested in my LICS 99 paper.
However, it seems (following your comments) that we can¹t prove ³PropExt
-> False² in this system.
One could argue that Lean¹s type theory is defined by its implementation
but 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 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.
A prime example of that "extra power" is that with HProp you can prove
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, in
which case unique choice is false.
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?
Thorsten
Ok, once we also allow QITs we know that this goes beyond the usualtopos logic (cf. the example in your paper with Peter).
of Michael Shulman" <homotopytypetheory@
Thorsten
On 12/12/2017, 23:14, "homotopytypetheory@googlegroups.com on behalf
googlegroups.com on behalf of
shu...@sandiego.edu> wrote:
both
This is really interesting. It's true that all toposes satisfy
unique choice and proof irrelevance. I agree that oneinterpretation
is that definitional proof-irrelevance is incompatible with theso
HoTT-style *definition* of propositions as (-1)-truncated types,
that you can *prove* something is a proposition, rather thanhaving
"being a proposition" being only a judgment. But could weinstead
blame it on the unjustified omission of type annotations?Morally, a
pairing constructorfalse
(-,-) : (a:A) -> B(a) -> Sum(x:A) B(x)
ought really to be annotated with the types it acts on:
(-,-)^{(a:A). B(a)} : (a:A) -> B(a) -> Sum(x:A) B(x)
and likewise the projection
first : (Sum(x:A) B(x)) -> A
should really be
first^{(a:A). B(a)} : (Sum(x:A) B(x)) -> A.
If we put these annotations in, then your "x" is
(true,refl)^{(b:Bool). true=b}
and your two apparently contradictory terms are
first^{(b:Bool). true=b} x == true
and
second^{(b:Bool). false=b} x : first^{(b:Bool). false=b} x =
and the
And we don't have "first^{(b:Bool). false=b} x == true", because
beta-reduction requires the type annotations on the projection
pairing to match. So it's not really the same "first x" that'sequal
to true as the one that's equal to false.and
In many type theories, we can omit these annotations on pairing
projection constructors because they are uniquely inferrable.But if
we end up in a type theory where they are not uniquelyinferrable, we
are no longer justified in omitting them.That is wether something is a proposition doesn¹t depend on other
On Tue, Dec 12, 2017 at 4:21 AM, Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk > wrote:
Good point.
OK, in a topos you have a static universe of propositions.
assumptions you make.
most one inhabitant. Now wether a type is a proposition may depend on
In set-level HoTT we define Prop as the types which have at
other assumptions. (-1)-univalence i.e. propositional extensionality turns
Prop into a subobject classifier (if you have resizing otherwise you get
some sort of predicative topos).
some additional power, in particular you can proof unique choice, because
However, the dynamic interpretation of propositions gives you
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=y then this is a proposition even though A may not
be. However using projections you also get Sigma x:A.P x.
am not sure wether this is enough). Btw, set-level HoTT also gives you
Hence I guess I should have said a topos with unique choice (I
QITs which eliminate many uses of choice (e.g. the definition of the
Cauchy Reals and the partiality monad).
<streicher@mathematik.tu-
Thorsten
On 12/12/2017, 12:02, "Thomas Streicher"
darmstadt.de > wrote:
taking Prop
But very topos is a model of extensional type theory when
equivalent= Omega. All elements of Prop are proof irrelevant and
betweenpropositions are equal.
Since it is a model of extensional TT there is no difference
sense then you cannot be in a topos. This came up recently in the contextpropsoitional and judgemental equality.
Thomas
If you have proof-irrelevance in the strong definitional
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:
Single(a) : Prop and
Given a:A define Single(a) = Sigma x:A.a=x. We have
obtain
p : Single(true) <-> Single(false)
since both are inhabited. Hence by extProp
extProp p : Single(true) = Single(false)
now we can use transport on (true,refl) : Single(true) to
get (definitionally):
x = (extProp p)*(true,refl) : Single(false)
and we can show that
second x : first x = false
but since Lean computationally ignores (extProp p)* we also
(note that my ???99 paper on Extensionality in Intensional Type Theory
first x == true
My conclusion is that strong proof-irrelvance is a bad idea
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.
wrote:
Thorsten
On 12/12/2017, 10:15, "Andrea Vezzosi" <sanz...@gmail.com>
be System U and hence inconsistent.
On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk > wrote:
Hi Kristina,
I guess you are not assuming Prop:Set because that would
inhabitants of a proposition are definitionally equal. This assumption is
By proof-irrelevance I assume that you mean that any two
inconsistent with it being a tops since in any Topos you get propositional
extensionality, that is P,Q : Prop, (P <-> Q) <-> (P = Q), which is indeed
an instance of univalence.
but I thought
I don't know if it's relevant to the current discussion,
supportthe topos of sets with Prop taken to be the booleans would
classicallyboth proof irrelevance and propositional extensionality,
like omega-sets or Lambda-sets to model the impredicative theory andat least. Is there some extra assumption I am missing here?
It should be possible to use a realizability semantics
identify the propositions with PERs that are just subsets.
"homotopytypetheory@
Cheers,
Thorsten
On 11/12/2017, 04:22,
googlegroups.com on behalf of Kristina Sojakova"
<homotopytypetheory@googlegroups.com on behalf of
sojakova...@gmail.com> wrote:
mailing list but did not
Dear all,
I asked this question last year on the coq-club
Is the theory withreceive a conclusive answer so I am trying here now.
proof-irrelevanta proof-relevant impredicative universe Set,
extensionality (known to be)impredicative universe Prop, and function
Prop makes the Idconsistent? It is known that the proof-irrelevance of
makes the theorytype behave differently usual and in particular,
matter of tacking onincompatible with univalence, so it is not just a
the addresseean interpretation for Prop.
Thanks in advance for any insight,
Kristina
This message and any attachment are intended solely for
received thisand may contain confidential information. If you have
immediately delete it.message in error, please send it back to me, and
contained in this
Please do not use, copy or disclose the information
expressed by themessage or in any attachment. Any views or opinions
of theauthor of this email do not necessarily reflect the views
contents of anUniversity of Nottingham.
This message has been checked for viruses but the
damage yourattachment may still contain software viruses which could
checks. Emailcomputer system, you are advised to perform your own
monitored ascommunications with the University of Nottingham may be
addresseepermitted by UK legislation.
This message and any attachment are intended solely for the
received thisand may contain confidential information. If you have
delete it.message in error, please send it back to me, and immediately
contained in this
Please do not use, copy or disclose the information
expressed by themessage or in any attachment. Any views or opinions
theauthor of this email do not necessarily reflect the views of
of anUniversity of Nottingham.
This message has been checked for viruses but the contents
damage yourattachment may still contain software viruses which could
computer system, you are advised to perform your own checks.
monitored ascommunications with the University of Nottingham may be
addresseepermitted by UK legislation.
This message and any attachment are intended solely for the
thisand may contain confidential information. If you have received
delete it.message in error, please send it back to me, and immediately
in this
Please do not use, copy or disclose the information contained
by themessage or in any attachment. Any views or opinions expressed
theauthor of this email do not necessarily reflect the views of
anUniversity of Nottingham.
This message has been checked for viruses but the contents of
damage yourattachment may still contain software viruses which could
computer system, you are advised to perform your own checks.
monitored ascommunications with the University of Nottingham may be
Google Groups "Homotopy Type Theory" group.permitted by UK legislation.
--
You received this message because you are subscribed to the
it, send an email to HomotopyTypeTheory+To unsubscribe from this group and stop receiving emails from
unsub...@googlegroups.com .
Google Groups "Homotopy Type Theory" group.For more options, visit https://groups.google.com/d/optout .
--
You received this message because you are subscribed to the
To unsubscribe from this group and stop receiving emails fromit, send an email to HomotopyTypeTheory+
unsub...@googlegroups.com .
For more options, visit https://groups.google.com/d/it.optout .
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
Groups "Homotopy Type Theory" group.
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.
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.
--
You received this message because you are subscribed to the Google
To unsubscribe from this group and stop receiving emails from it,send an email to HomotopyTypeTheory+
unsub...@googlegroups.com .
For more options, visit https://groups.google.com/d/optout .
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.
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.
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.
--
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 HomotopyTypeTheory+unsub...@googlegroups.com .
For more options, visit https://groups.google.com/d/optout .
--
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 HomotopyTypeTheory+unsub...@googlegroups.com .
For more options, visit https://groups.google.com/d/optout .
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. 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. 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.--
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 HomotopyTypeTheory+unsub...@googlegroups.com .
For more options, visit https://groups.google.com/d/optout .