Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
To: Michael Shulman <shu...@sandiego.edu>
Cc: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?
Date: Sat, 16 Dec 2017 15:21:07 +0000	[thread overview]
Message-ID: <40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk> (raw)
In-Reply-To: <CAOvivQxCPHoxRVztybM5d_os3zqTh744Kxc41999KSFy6rrmyg@mail.gmail.com>

On 14/12/2017, 18:52, "Michael Shulman" <shu...@sandiego.edu> wrote:

    On Thu, Dec 14, 2017 at 4:32 AM, Thorsten Altenkirch
    <Thorsten....@nottingham.ac.uk> wrote:
    > Excellent observation! So basically the implementation of Lean is
incorrect because we shouldn¹t be able to derive true = false from the
assumption of propositional extensionality if we take account of the type
annotations.
    >
    > The example arose from the question whether we can add propositional
extensionality to Lean. That s we define HProp = Sigma P:Type.Pi
x,y.P.x=y. Note that the equality we use here is the static Prop valued
equality. Now I suggested to add propositional extensionality for HProp as
an axiom to Lean but it seemed to lead to the problem.
    
    Well, if I understand you correctly, it sounds like the implementation
    of Lean isn't *currently* incorrect -- omitting such type annotations
    is a perfectly fine optimization for implementations of most type
    theories.  It's just that it would have to be modified in order to
    *remain* correct under the addition of propositional extensionality
    for HProp.  Right?

Not really: you can prove ³PropExt -> False² in the current system and you
shouldn¹t be able to do this.

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.


  reply	other threads:[~2017-12-16 15:21 UTC|newest]

Thread overview: 54+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-12-11  4:22 Kristina Sojakova
2017-12-11 11:42 ` [HoTT] " Jon Sterling
2017-12-11 12:15   ` Kristina Sojakova
2017-12-11 12:43     ` Jon Sterling
2017-12-11 14:28       ` Thomas Streicher
2017-12-11 14:32         ` Kristina Sojakova
2017-12-11 14:23 ` Thorsten Altenkirch
2017-12-12 10:15   ` Andrea Vezzosi
2017-12-12 11:03     ` Thorsten Altenkirch
2017-12-12 12:02       ` Thomas Streicher
2017-12-12 12:21         ` Thorsten Altenkirch
2017-12-12 13:17           ` Jon Sterling
2017-12-12 19:29             ` Thomas Streicher
2017-12-12 19:52               ` Martin Escardo
2017-12-12 23:14           ` Michael Shulman
2017-12-14 12:32             ` Thorsten Altenkirch
2017-12-14 18:52               ` Michael Shulman
2017-12-16 15:21                 ` Thorsten Altenkirch [this message]
2017-12-17 12:55                   ` Michael Shulman
2017-12-17 17:08                     ` Ben Sherman
2017-12-17 17:16                       ` Thorsten Altenkirch
2017-12-17 22:43                         ` Floris van Doorn
2017-12-15 17:00           ` Thomas Streicher
2017-12-17  8:47             ` Thorsten Altenkirch
2017-12-17 10:21               ` Thomas Streicher
2017-12-17 11:39                 ` Thorsten Altenkirch
2017-12-18  7:41                   ` Matt Oliveri
2017-12-18 10:00                     ` Michael Shulman
2017-12-18 11:55                       ` Matt Oliveri
2017-12-18 16:24                         ` Michael Shulman
2017-12-18 20:08                           ` Matt Oliveri
2017-12-18 10:10                     ` Thorsten Altenkirch
2017-12-18 11:17                       ` Matt Oliveri
2017-12-18 12:09                       ` Matt Oliveri
2017-12-18 11:52                   ` Thomas Streicher
2017-12-19 11:26                     ` Thorsten Altenkirch
2017-12-19 13:52                       ` Andrej Bauer
2017-12-19 14:44                         ` Thorsten Altenkirch
2017-12-19 15:31                           ` Thomas Streicher
2017-12-19 16:10                             ` Thorsten Altenkirch
2017-12-19 16:31                               ` Thomas Streicher
2017-12-19 16:37                                 ` Thorsten Altenkirch
2017-12-20 11:00                                   ` Thomas Streicher
2017-12-20 11:16                                     ` Thorsten Altenkirch
2017-12-20 11:41                                       ` Thomas Streicher
2017-12-21  0:42                                         ` Matt Oliveri
2017-12-22 11:18                                           ` Thorsten Altenkirch
2017-12-22 21:20                                             ` Martín Hötzel Escardó
2017-12-22 21:36                                               ` Martín Hötzel Escardó
2017-12-23  0:25                                               ` Matt Oliveri
2017-12-19 16:41                         ` Steve Awodey
2017-12-20  0:14                           ` Andrej Bauer
2017-12-20  3:55                             ` Steve Awodey
     [not found]       ` <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net>
2017-12-14 13:28         ` Thorsten Altenkirch

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=40D87932-BBF0-4CCF-A8D1-32E7A7BBFE5C@exmail.nottingham.ac.uk \
    --to="thorsten...."@nottingham.ac.uk \
    --cc="homotopyt..."@googlegroups.com \
    --cc="shu..."@sandiego.edu \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).