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 ³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.
For more options, visit https://groups.google.com/d/optout.