Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

[Ben Sherman <she...@csail.mit.edu>]

[-- Attachment #1: Type: text/plain, Size: 17886 bytes --]

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....@nottingham.ac.uk <mailto:Thorsten....@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 usual
>> topos logic (cf. the example in your paper with Peter).
>>> 
>>> Thorsten
>>> 
>>> 
>>> On 12/12/2017, 23:14, "homotopyt...@googlegroups.com on behalf
>> of Michael Shulman" <homotopyt...@googlegroups.com on behalf of
>> shu...@sandiego.edu> wrote:
>>> 
>>>    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
>>> 
>>>    (-,-) : (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 =
>> false
>>> 
>>>    And we don't have "first^{(b:Bool). false=b} x == true", because
>>>    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.
>>> 
>>>    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.
>>> 
>>> 
>>>    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¹t 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 subobject classifier (if you have resizing otherwise you get
>> some sort of predicative topos).
>>>> 
>>>> However, the dynamic interpretation of propositions gives you
>> some additional power, in particular you can proof unique choice, because
>> 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.
>>>> 
>>>> 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).
>>>> 
>>>> Thorsten
>>>> 
>>>> 
>>>> 
>>>> 
>>>> 
>>>> 
>>>> On 12/12/2017, 12:02, "Thomas Streicher"
>> <stre...@mathematik.tu-darmstadt.de> wrote:
>>>> 
>>>>> But very topos is a model of extensional type theory when
>> taking Prop
>>>>> = Omega. All elements of Prop are proof irrelevant and
>> equivalent
>>>>> propositions are equal.
>>>>> 
>>>>> Since it is a model of extensional TT there is no difference
>> between
>>>>> propsoitional 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 which is a type-theory based interactive proof system developed at
>> microsoft and which does implement proof-irrelvance. Note that any topos
>> has extProp:
>>>>>> 
>>>>>> Given a:A define Single(a) = Sigma x:A.a=x. We have
>> Single(a) : Prop and
>>>>>> 
>>>>>> 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
>> obtain
>>>>>> 
>>>>>> 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
>> get (definitionally):
>>>>>> 
>>>>>> first x == true
>>>>>> 
>>>>>> 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.
>>>>>> 
>>>>>> 
>>>>>> Thorsten
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> On 12/12/2017, 10:15, "Andrea Vezzosi" <sanz...@gmail.com>
>> wrote:
>>>>>> 
>>>>>>> On Mon, Dec 11, 2017 at 3:23 PM, Thorsten Altenkirch
>>>>>>> <Thorsten....@nottingham.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 that any two
>> inhabitants of a proposition are definitionally equal. This assumption is
>> 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.
>>>>>>>> 
>>>>>>> 
>>>>>>> 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?
>>>>>>> 
>>>>>>> 
>>>>>>>> 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.
>>>>>>>> 
>>>>>>>> Cheers,
>>>>>>>> Thorsten
>>>>>>>> 
>>>>>>>> 
>>>>>>>> On 11/12/2017, 04:22,
>> "homotopyt...@googlegroups.com on behalf of Kristina Sojakova"
>> <homotopyt...@googlegroups.com on behalf of
>> sojakova...@gmail.com> wrote:
>>>>>>>> 
>>>>>>>>    Dear all,
>>>>>>>> 
>>>>>>>>    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.
>>>>>>>> 
>>>>>>>>    Thanks in advance for any insight,
>>>>>>>> 
>>>>>>>>    Kristina
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 
>>>>>>>> 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.
>>>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 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.
>>>>>> 
>>>> 
>>>> 
>>>> 
>>>> 
>>>> 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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 46969 bytes --]