Impredicative set + function extensionality + proof irrelevance consistent?

[Kristina Sojakova]

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

[Jon Sterling]

Can we make sense of this by interpreting into a realizability topos?

In particular, I am under the impression that Eff (the effective topos)
models an impredicative universe of proof-relevant types, and on the
other hand its subobject classifier can be used to model a
proof-irrelevant Prop.

As a topos, Eff models extensional type theory, and thence we have the
functional extensionality law.

Best,
Jon

> --
> 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.

[Kristina Sojakova]

Hi Jon,

Thanks for the answer! In this model, what would be the interpretation
of the eq_A(a,b) : Prop type in Coq, which is logically equivalent to
Id_A(a,b) : Type but proof irrelevant?

Best,

Kristina

[Jon Sterling]

Hi Kristina,

If you are using the subobject classifier to model Prop, I think that
you can just use the ordinary equality predicate of the topos logic. The
equality predicate for a type 'A' is given by the
(generalized/Lawvere-style) existential quantification along the
diagonal "δ : X -> X * X".

I think this ought to be the same as alternatively first constructing
the identity type in the proof-relevant fragment and then reflecting it
into the subobject classifier, since toposes model extensional identity
types.

Best,
Jon

[Thorsten Altenkirch]

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.

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

--
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.

[Thomas Streicher]

It's amazing how common knoledge from late 80s can disappeear easily.
For interpreting Coq one uses Asm(A), assemblies over a pca A, Set is
interpreted as modest sets and Prop as subterminal modest sets.
It's important to take Asm(A) instead of the realizability topos for
showing that Set is internally complete in a sufficiently strong
sense. (See Ed Robinson's old LICS paper "How Complete is PER?").

Of course, these models don't validate UA but they were not meant to be.

Id takes values in Prop and is isomorphic to Leibniz equality.

See work from the 80s by Martin Hyland, myself and a few others.

Thomas

[Kristina Sojakova]

Hi Thomas,

Thank you for the answer! You wrote:

"Id takes values in Prop and is isomorphic to Leibniz equality."

That would be what coq calls "eq". But what is the interpretation of the
proof-relevant identity type "Id", which takes values in Type? For my
theory I want both.

Kristina

[Andrea Vezzosi]

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?

[Thorsten Altenkirch]

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

[Thomas Streicher]

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 Altenkirch]

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

[Jon Sterling]

On Tue, Dec 12, 2017, at 04:21 AM, Thorsten Altenkirch 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).

Thorsten,

I think that unique choice holds in every topos, at least when you state
it in the topos logic. This is in Mac Lane & Moerdijk as exercise 11 in
chapter VI, Topoi And Logic.

I'm a little confused now, but maybe this has to do with some subtle
difference between the ordinary topos-theoretic subobject classifier,
and the HoTT-style one which you get from univalence (as you describe).

Best,
Jon

[Thomas Streicher]

> I think that unique choice holds in every topos, at least when you state
> it in the topos logic. This is in Mac Lane & Moerdijk as exercise 11 in
> chapter VI, Topoi And Logic.
>
> I'm a little confused now, but maybe this has to do with some subtle
> difference between the ordinary topos-theoretic subobject classifier,
> and the HoTT-style one which you get from univalence (as you describe).

Of course, toposes all validate AUC. Since in an arbitrary topos logic
is interpreted via the topos's Omega AUC holds then as well.

Univalence is something which will not hold in most toposes and if it
does one has to interpret Id in a way that it is not a proposition.

Thomas

[Martin Escardo]

On 12/12/17 19:29, Thomas Streicher wrote:
> Univalence is something which will not hold in most toposes and if it
> does one has to interpret Id in a way that it is not a proposition.

How do you even formulate univalence for an arbitrary topos?

Martin

[Michael Shulman]

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.

[Thorsten Altenkirch]

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.

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. 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

[Gaëtan Gilbert]

>We have Single(a) : Prop

How do we have this without truncating (which means we don't have
projections)?

Gaëtan Gilbert

[Thorsten Altenkirch]

I guess you are concerned that while singleton is contractible in HoTT, this is not true if we use an equality which is always propositional

However, since I am talking about set-level HoTT, I am assuming A:Set (that is HSet). Btw, I meant Single(a) : HProp (since there is the other static Prop as well).

But I think Mike’s comment nails it.

Thorsten

[Michael Shulman]

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?

> 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.

[Thomas Streicher]

Hi Thorsten,

my analysis of your proof of true = false in Lean is as follows.

I don't see that (\Sigma x:A) a = x is an element of Prop though it
certainly is isomorphic to an element in Prop, namely true. But leaving
this aside I analyse the situation as follows.

Your argument essentially is as follows. Since Single(true) and
Single(false) are isomorphic they are equal (essentially by UA applied
to subsingletons). Now you have c in Single(true) and d in Single(false)
whose first projections are true and false respectively.

From this you conclude that that true and false are equal since c and
d are equal. But they aren't since they belong to different types.

This style of argument allows you prove that all types are
propositions as follows. Suppose a and a' are elements of A. Then
Single(a) and Single(a') are equivalent propositions and thus
equal. Then also their first projections are equal and thus a = a'.

I fully agree with Mike's analysis that projections have to be typed.
But, moreover, we must not neglect equality proofs when replacing
equals by equals.

Moreover, toposes will not validate univalence. As pointed out to me
by Martin Escardo you can't even formulate it because in arbitrary
toposes you don't have universe (not to speak of univalent ones).

Thomas

PS Your observation doesn't really increase my believe in the gain of
certainty when formalizing proofs :-)

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

On 15/12/2017, 17:00, "homotopyt...@googlegroups.com on behalf of
Thomas Streicher" <homotopyt...@googlegroups.com on behalf of

stre...@mathematik.tu-darmstadt.de> wrote:

>Moreover, toposes will not validate univalence. As pointed out to me
>by Martin Escardo you can't even formulate it because in arbitrary
>toposes you don't have universe (not to speak of univalent ones).

I was only talking about the special case of (-1)-univalence or
propositional extensionality that is for P,Q : Prop

(P <-> Q) -> (P = Q)

Thorsten

[Thomas Streicher]

> >Moreover, toposes will not validate univalence. As pointed out to me
> >by Martin Escardo you can't even formulate it because in arbitrary
> >toposes you don't have universe (not to speak of univalent ones).
>
> I was only talking about the special case of (-1)-univalence or
> propositional extensionality that is for P,Q : Prop
>
> (P <-> Q) -> (P = Q)

This would be ok but you assume also that Single(True) and
Single(false) are propositions but they are just both ISOMORPHIC to 1
in Omega = Prop. That's where you apply UA for (sub)singletons UNCONSCIOUSLY.

The inconsistency proof you have given is a slightly distorted version
of the following ridiculous argument: {a} and {b} are isomorphic thus
equal for which reason a = b.

Thomas

[Thorsten Altenkirch]

On 17/12/2017, 10:21, "Thomas Streicher"

<stre...@mathematik.tu-darmstadt.de> wrote:

>> >Moreover, toposes will not validate univalence. As pointed out to me
>> >by Martin Escardo you can't even formulate it because in arbitrary
>> >toposes you don't have universe (not to speak of univalent ones).
>>
>> I was only talking about the special case of (-1)-univalence or
>> propositional extensionality that is for P,Q : Prop
>>
>> (P <-> Q) -> (P = Q)
>
>This would be ok but you assume also that Single(True) and
>Single(false) are propositions but they are just both ISOMORPHIC to 1
>in Omega = Prop. That's where you apply UA for (sub)singletons
>UNCONSCIOUSLY.

I wasn't defending the inconsistency derivation I posted earlier, as Mike
pointed out it, it ignores type annotations.

However, I don't understand your point. Surely UA for subsingletons is
exactly propositional extensionality.

>The inconsistency proof you have given is a slightly distorted version
>of the following ridiculous argument: {a} and {b} are isomorphic thus
>equal for which reason a = b.

Indeed, but we are not in set theory. In set level HoTT Single(True) =
Single(False) but True != False.

Whenever we can prove that a type is A propositional, that is all
x,y:A.x=y it is a subsingleton and we can construct a corresponding
element of Prop (aka Omega). Hence a topos corresponds to set-level HoTT
(ignoring predicativity issues for the moment).

In a language like Lean with a static universe of propositions this is not
the case. Only certain subsingletons get classified. I don't really
understand the relation but it seems that you get a quasitopos. And indeed
in this language you don't have unique choice (which was the cause of my
confusion).

The issue was this: in a type theory with a static universe of
propositions you can add definitional proof-irrelevance, that is any two
proofs of a proposition are definitionally equal. The derivation I posted
earlier seemed to imply that you cannot have definitional
proof-irrelevance and a be in a topos. Luckily this turns out to be
incorrect and it is just due to the way proof irrelevance is implemented
in Lean (which is just wrong imho).

[Michael Shulman]

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?)

[Ben Sherman]

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.

[Thorsten Altenkirch]

Thank you, Ben! That is good news actually.

Thorsten

[Floris van Doorn]

Just to clear some things up in this conversation:

- The Lean kernel is consistent with any form of propositional extensionality, as far as I know.

- The kernel for the current version of Lean, Lean 3, is not designed for HoTT and inconsistent with univalence. However, it does *not* ignore any transport of an equality. The bottom universe in Lean is the universe of propositions, Prop (not to be confused with hProp). What does hold is that there is definitional proof irrelevance for proofs of a proposition, i.e. if P : Prop and p, q : P then p is definitionally equal to q. This means that if we have a proof p : A = A for some type A, then transporting along p is the identity function (because p = refl, definitionally). However, if p : A = B, then transporting along p is not the identity function (which would be type incorrect to state).

- Lean has an evaluator in a virtual machine, which is used to evaluate programs and tactics efficiently outside the kernel. This evaluator is not trusted, and cannot be used when writing any proof in Lean. This evaluator removes all type information and propositions for efficiency, and can evaluate expressions to the wrong answer when axioms are added to the type theory (even if the axioms are consistent). For example, if we add the following lines to Ben's example

```

constant H : HProp_ext

#eval Sig.fst (x H)

```

we see that the evaluator incorrectly evaluates this expression to tt (true). Needless to say, the evaluator was not designed for this, but instead to evaluate tactics like the following quickly.

```

if n < 1000000 then apply tactic1 else apply tactic2

```

I hope this clears up any confusion.

Best,

Floris

Thorsten


On 12/12/2017, 23:14, "homotopytypetheory@googlegroups.com on behalf

of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of

"homotopytypetheory@googlegroups.com on behalf of Kristina Sojakova"
<homotopytypetheory@googlegroups.com on behalf of

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.

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.

[Matt Oliveri]

Hello. I'd like to see if I have the situation straight:

For presenting a topos as a type system, there are expected to be (at least) two styles: having a type of "static" propositions, or using hprops.

With hprops, you can prove unique choice, so it's always topos-like (pretopos?).

With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier.

If you don't necessarily have unique choice or equivalent, you're dealing with a quasitopos, which is a more general thing.

With static props and unique choice, subsingletons generally aren't already propositions, but they all correspond to a proposition stating that the subsingleton is inhabited. Unique choice obtains the element of a subsingleton known to be inhabited.

The usual way to present a topos as a type system is with a non-dependent type system like IHOL. This will not be able to express hprops, so static props is the way. Proofs will not be objects, so proof-irrelevance doesn't come up.

The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.)

In a dependent type system, a type of static props may or may not be a universe.

If it's not, proofs still aren't objects and proof-irrelevance still doesn't come up.

But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.)

In that case, with equality reflection, you automatically get judgmental proof-irrelevance. This does not necessarily mean that proofs are computationally irrelevant. With unique choice, they cannot be, or else you lose canonicity.

All OK?

[Michael Shulman]

That seems about right to me, except that I don't know whether a
static universe of props without unique choice *actually* gives a
quasitopos. It gives you a class of subobjects that have a classifer,
which looks kind of like a quasitopos, but can we prove that they are
actually the strong/regular monos as in a quasitopos? And a
quasitopos also has finite colimits; do HITs make sense with a static
Prop?

[Thorsten Altenkirch]

I agree with most of your summary. Some comments and questions.

 

From: <homotopyt...@googlegroups.com> on behalf of Matt Oliveri <atm...@gmail.com>
Date: Monday, 18 December 2017 at 07:41
To: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

 

Hello. I'd like to see if I have the situation straight:

For presenting a topos as a type system, there are expected to be (at least) two styles: having a type of "static" propositions, or using hprops.

With hprops, you can prove unique choice, so it's always topos-like (pretopos?).

 

Yes, indeed. The remaining issue is the question of impredicativity. If you want to stay predicative you may want to add quotients or QITs. Interestingly it seems that QITs are more expressive then quotients (which can be encoded impredicatively).

With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier.

 

Yes, indeed. However, adding postulates to Type Theory is just a stop gap measure because you still don’t have a computational interpretation. While we have a computational interpretation for most of HoTT, namely cubical type theory ala Coquand et al, one might hope that there is a simpler way to deal with the set level fragment of HoTT.

If you don't necessarily have unique choice or equivalent, you're dealing with a quasitopos, which is a more general thing.

 

Basically you reflect some subobjects but not all. I don’t yet understand how the definition of a quasitops relates to static universes of propositios.

With static props and unique choice, subsingletons generally aren't already propositions, but they all correspond to a proposition stating that the subsingleton is inhabited. Unique choice obtains the element of a subsingleton known to be inhabited.

The usual way to present a topos as a type system is with a non-dependent type system like IHOL. This will not be able to express hprops, so static props is the way. Proofs will not be objects, so proof-irrelevance doesn't come up.

 

Indeed or to put it the other way: set level HoTT is a novel way to present a topos. And as I said above, QITs are an interesting extension which in some instances avoids appealing to the axiom of choice.

The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.)

In a dependent type system, a type of static props may or may not be a universe.

 

What do you mean by “is a universe” here?

If it's not, proofs still aren't objects and proof-irrelevance still doesn't come up.

But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.)

In that case, with equality reflection, you automatically get judgmental proof-irrelevance.

 

For equality but not for propositions in general.

 

This does not necessarily mean that proofs are computationally irrelevant.

 

Now I am confused: what is the difference between judgmental and computational irrelevance?

 

With unique choice, they cannot be, or else you lose canonicity.

Since I didn’t understand the previous sentences I am not sure about this conclusion. It sounds right, though.

 

Thorsten

All OK?

--
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.

[Matt Oliveri]

On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote:

With static props, you can't prove unique choice, but it may be consistent as an additional primitive, or you can ensure in some other way that you have a subobject classifier.

 

Yes, indeed. However, adding postulates to Type Theory is just a stop gap measure because you still don’t have a computational interpretation. While we have a computational interpretation for most of HoTT, namely cubical type theory ala Coquand et al, one might hope that there is a simpler way to deal with the set level fragment of HoTT.

I suspect one could also come up with a type system with a computational interpretation that has static props and unique choice. I was counting this possibility too as an additional primitive.

The static props approach can also be used in a dependent type system, along with unique choice or equivalent. (To say nothing of whether that's a natural kind of system.)

In a dependent type system, a type of static props may or may not be a universe.

 

What do you mean by “is a universe” here?

Just that the type of props would be one of the built-in universes, either Russell or Tarski-style.

But if it is, you should at least have typal proof-irrelevance. (That is, stated using equality types.)

In that case, with equality reflection, you automatically get judgmental proof-irrelevance.

 

For equality but not for propositions in general.

I'm saying if you have typal proof-irrelevance and equality reflection, you get judgmental proof-irrelevance by reflecting the equalities between proofs given by typal proof-irrelevance.

 

This does not necessarily mean that proofs are computationally irrelevant.

 

Now I am confused: what is the difference between judgmental and computational irrelevance?

By computationally-irrelevant proofs, I mean that terms of propositions are never needed when evaluating closed terms of non-proposition types. Like, Coq has a type of static propositions: the universe Prop. And the proofs are supposed to be computationally irrelevant. This is relied upon to erase them with program extraction. From the earlier messages about Lean, it sounds like Lean's proofs are also intended to be computationally irrelevant.

With equality reflection, irrelevance according to judgmental equality can be totally different from computational relevance. (Though it seems like a confusing and unhelpful possibility. When judgments are undecidable anyway, computationally irrelevant proofs can simply be removed from the term language entirely.)

[Matt Oliveri]

Oh right. Static propositions alone doesn't seem to guarantee a quasitopos either.

I thought HITs make sense with static props. After all, the type of propositions isn't even involved, formally.

[Matt Oliveri]

I don't understand these things you wrote:

On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote:

Interestingly it seems that QITs are more expressive then quotients (which can be encoded impredicatively).

And as I said above, QITs are an interesting extension which in some instances avoids appealing to the axiom of choice.

Like, in a constructive, predicative system without any choice principles, and where quotients are not expressed as QITs, is there an expressiveness difference? (I'm thinking of Computational Type Theory, for example.)

[Thomas Streicher]

> >The inconsistency proof you have given is a slightly distorted version
> >of the following ridiculous argument: {a} and {b} are isomorphic thus
> >equal for which reason a = b.
>
> Indeed, but we are not in set theory. In set level HoTT Single(True) =
> Single(False) but True != False.

This is not a question of set theory. In a topos we have propositional
extensionality in the sense that

\forall p,q:Omega. (p <-> q) -> p = q

but what we don't have is that Single(a) \in \Omega for a \in A.

Thomas

[Michael Shulman]

HITs involve equality, so if equality is a static prop, then it is involved.

[Matt Oliveri]

Well that's true. For some reason, I was thinking equality would still be an ordinary type, but I guess that would be silly.

So what do you require, for HITs to "make sense", with equality being a static prop family? That they can provide finite colimits? Don't they do this, analogously to homotopy colimits in HoTT?

[Thorsten Altenkirch]

I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a).

Thorsten

--
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.

[Andrej Bauer]

> I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a).

I beleive a lot of the confusion in this discussion would go away if
we translated some of what Thomas is saying into a more syntactic
setup. We have to be a bit careful about what "corresponds to" means.

To say that Ω classifies truth values, or h-propositions, means that:

1. There is a type Ω.

2. There is a type family El(p) indexed by p : Ω.

3. For every p : Ω the type El(p) is an h-prop (there's a term witnessing this).

4. For every h-prop P -- which is a type, not an element of Ω! --
there is p : Ω such that P is equivalent to El(p). (Again we need a
term witnessing the equivalence.)

Now, it may happen that h-props P and Q are both equivalent to El(r)
even though they are not equal.

Furthermore, there can be class-many subobjects of 1 in a topos, for
instance in sets there are class-many singletons. Of course, a whole
lot of them will be isomorphic and very many "correspond to" the
element ⊤ : Ω. But at least on this mailing list we're not in the
business of sweeping isomorphisms under the rug.

With kind regards,

Andrej

[Thorsten Altenkirch]

Thank you, Andrej.

Indeed, while in usual Type Theory a universe (U, El) with a unit type is presented as

one : U
El one == 1

(where == is definitional equality) semantically we only have

α : El one ~ 1

(where ~ is isomorphism).

I was just applying the same abuse of language to Ω, that is there is

“Single(a)” : Ω
El (“Single(a)”) == Single(a)

Where I should have said:

β : El (“Single(a)”) ~ Single(a)

However, if the category in question is univalent then isomorphic objects are equal and the abuse of language is justified.

Thorsten

[Thomas Streicher]

> Furthermore, there can be class-many subobjects of 1 in a topos, for
> instance in sets there are class-many singletons. Of course, a whole
> lot of them will be isomorphic and very many "correspond to" the

> element ??? : ??. But at least on this mailing list we're not in the

> business of sweeping isomorphisms under the rug.

Thanks, Andrej, for trying to clean up the discussion!

Thorsten hads not daid how to inetrpret equality. In an arbitrary
topos there is no other choice than interpeting equality by fibrewise
diagonals. So we have extensional equality!

I am afraid there want exist too many univalent categories. They all
would be rigid which is very inconstructive.

Thomas

[Thorsten Altenkirch]

Ah, you suffer from using set theory as a meta language. (

There are lots if univalent categories. In HoTT.

Thorsten

On 19/12/2017, 15:31, "homotopyt...@googlegroups.com on behalf of Thomas Streicher" <homotopyt...@googlegroups.com on behalf of stre...@mathematik.tu-darmstadt.de> wrote:

I am afraid there want exist too many univalent categories. They all
would be rigid which is very inconstructive.

[Thomas Streicher]

> Ah, you suffer from using set theory as a meta language. (
>
> There are lots if univalent categories. In HoTT.

That clears it up!

Thomas

PS I am not fixed to set theory. Could as well be a suffiently strong
extensional type theory. But, of course, set theory is fine for me as
a metalanguage.

[Thorsten Altenkirch]

I think there is a trade off: you can be destructive and use choice but stick to sets or you are constructive and use HoTT. But having no choice and using sets is sad.

T.

[Steve Awodey]

So far so good, but the last remark is a bit too cryptic.
If this is supposed to be subobject classification in the sense of an elementary topos,
then the p’s that “correspond to" isomorphic h-props still need to be identified.
That’s univalence for Omega, of course, which does indeed hold in a topos.

Otherwise, you are talking about a looser notion of “classification” of h-props.

Steve


>
> With kind regards,
>
> Andrej

[Andrej Bauer]

> If this is supposed to be subobject classification in the sense of an elementary topos,
> then the p’s that “correspond to" isomorphic h-props still need to be identified.
> That’s univalence for Omega, of course, which does indeed hold in a topos.

Isn't Thomas's point that the p's that correspond to isomorphic
h-props are *equal*, and that there is only one reasonable notion of
equality in a topos, which is extensional equality?

With kind regards,

Andrej

[Steve Awodey]

Yes, that’s fine, but it wasn’t part of your reformulation (at least not explicitly).
Steve

Sent from mobile - sorry fr typos.

[Thomas Streicher]

Now at first sight it looks as if doing toposes in a univalent
metatheory makes them inconsistent in the sense that all toposes are
trivial.

But, luckily, that is not the case. If a and a' are in A then (a,refl(a))
and (a',refl(a')) are in Single(a) and Single(a') respectively. These
types are certainly isomorphic but not judgementally equal. You can project
(a,refl(a)) on a and (a',refl(a')) to a' by applying DIFFERENT first
projection functions pi and pi' respectively. But you cannot apply pi'
to (a,refl(a)) before having it transformed into an object of Single(a')
along an iso between Single(a) and Single(a'). Thorsten has claimed
that this were possible in LEAN but it shouldn't!

Here is an excerpt from Thorsten's original mail

> 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
>

he clearly says that "since Lean computationally ignores (extProp p)*"

but that is balatantly wrong since it mixes judgemental and propositional
equality.

And there we are back to what I originally said. Of course, {a} and {a'} are
isomorphic and thus equal as elements of P(A) if we postulate UA for P(A).
Thus we shouldn't!

Another gap in Thorsten's argument is the following. Though Single(a) and
Single(a') are isomorphic in order to conclude that they are propositionally
equal they would have to be elements of a univalent universe BUT I don't see
where such a universe should come from in the general topos case!

Thomas

[Thorsten Altenkirch]

Hi Thomas,

we have already established that my argument was incorrect (for the reasons you state) and I was misinformed about the behaviour of Lean.

>
>Another gap in Thorsten's argument is the following. Though Single(a) and
>Single(a') are isomorphic in order to conclude that they are propositionally
>equal they would have to be elements of a univalent universe BUT I don't see
>where such a universe should come from in the general topos case!

I don’t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a’) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos.

Thorsten

[Thomas Streicher]

Hi Thorsten,

> we have already established that my argument was incorrect (for the
> reasons you state) and I was misinformed about the behaviour of
> Lean.

I know, I just wanted to spot where the problem precisely is.

> >Another gap in Thorsten's argument is the following. Though Single(a) and
> >Single(a') are isomorphic in order to conclude that they are propositionally
> >equal they would have to be elements of a univalent universe BUT I don't see
> >where such a universe should come from in the general topos case!

> I don???t understand this point. In a type theoretic implementation of a topos Single(a) and Single(a???) would be propositionally equal due to propositional extensionality. The only additional assumption I need to make is that the universe of proposition is strict, e.g. we have that El(A -> B) is definitionally equal to EL(A) -> El(B). This seems to be quite natural from the point of type theory where universes are usually strict and moreover this is true in any univalent category giving rise to a topos.

Well, Single(a) and Single(a') were propsitionally equal if they were
elements of a univalent universe U but where should this come from if
you start from an elementary topos in a univalent metatheory.

Thomas

[Matt Oliveri]

Hi Thorsten and Thomas,

It still looks to me like you're talking about different things and having a misunderstanding.
By "propositional extensionality", Thorsten seems to mean the special case of univalence that applies to hprops. (Which he's simply calling propositions.) But it sounds like Thomas is counting "propositional extensionality" as a separate principle from univalence, for a type of static props. I think the system Thorsten has in mind presents a (pre)topos as a univalent type system, where hprops are used *instead of* a type of static props.

But maybe not, and I'm misunderstanding.

[Thorsten Altenkirch]

Hi Matt,

Yes, this is what I wanted to say. To put it in a different way: in Type Theory we can approximate Omega by HProp. And indeed, every subobject of 1 is represented as an element of HProp. There are 2 mismatches: HProp is large but Omega is small (this corresponds to impredicativity or resizing). The other is propositional extensionality which is an instance of univalence.

We can view topoi as a first approximation of HoTT. When we replace a subobject classifier by an object classifier, that is classifying all maps and not just propositions we obtain univalent universes. However, two provisos are necessary: 1. we cannot classify all maps otherwise we end up with a system with Type : Type and 2. we have to move to an (omega,1)-category because univalence is forced upon us as an equality and this doesn’t work if all types are sets. That is a higher predicative topos fixes the historic shortcomings of topos theory.

By moving to a predicative setting we give up the encodings of colimits (e.g. coequalizers) using the subobject classifier. Indeed, this is just the impredicative encoding of quotient types. Instead we need to explictly add them but we can do this in a way which goes beyond topos theory (even in the propositional setting) namely as QITs (propositional) or HITs (in the higher case).

Thorsten

From: <homotopyt...@googlegroups.com> on behalf of Matt Oliveri <atm...@gmail.com>
Date: Thursday, 21 December 2017 at 00:42
To: Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?

--

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.

[Martín Hötzel Escardó]

There may be some confusion about univalence and equality of subsets

of a type. 

Univalence is compatible with the fact that two subsets A,B of a type

X are equal iff they have the same elements.

In fact, univalence implies that.

Define Prop=Σ(P : U),isProp P where isProp(P:U) = Π(x,y:P),x=y. This

is a large type (it lives in the same universe as U, rather than in

U). You may wish to make this small (like in UniMath), or not, but

this is orthogonal to this discussion.

Then define the powerset of a type X by ℙ X = X → Prop.

(As in topos theory.)

Then for A : ℙ X and x : X we write x ∈ A to mean A x.

(As in the internal language of a topos.)

Then, assuming univalence, we have (theorem of intensional MLTT+UA):

  (A=B) = ∀(x:X), x ∈ A ⇔ x ∈ B.

(Because the middle equality is that of two sets, we don't need to

worry about which specific equality we pick - there is at most

one. This again relies on univalence.)

Without assuming univalence, we can't prove (or disprove) this

equality. Not in intensional MLTT, or even in so-called extensional

MLTT (= intensional MLTT + equality reflection). This is because in

order to prove this equality, we need both functional and

propositional extensionality. Extensional MLTT has the former but not

the latter. Univalent MLTT has both.

Here, the quantifier ∀ is a function of type (X → Prop) → Prop and the

logical connective _⇔_ is a function Prop → Prop → Prop (or Prop ×

Prop → Prop, it doesn't matter).

Now, from a subset A : ℙ X, we get a type A' and an embedding A' → X.

(The construction works like this: we have A : X → Prop, and a

projection Prop → U. Then the type A' is the sum (Σ) of composite

function. The embedding is the first projection.)

It is definitely not the case that if A'=B' for A,B : ℙ X then A=B.

Example: X=ℕ, A=isEven and B=isOdd. Then A ≠ B but A'=B' (because A'

and B' are isomorphic sets).

However, we do have that

  ℙ X ≃ Σ (A' : U), Σ (e : A' → X), isEmbedding e,

where (isEmbedding e) means that the fibers of e are propositions.

Then the elements (Σ isEven, (_ , _)) and (Σ isOdd, (_ , _)) of the

rhs type, for uniquely determined "_", are different, even though the

types Σ isEven and Σ isOdd are equal.

All the misunderstandings in the previous messages are caused by

looking at the particular type X=1 without enough care.

And I think this is what Thomas is pointing out.

Best,

Martin

[Martín Hötzel Escardó]

Correction (that you already spotted, of course):

On Friday, 22 December 2017 21:20:21 UTC, Martín Hötzel Escardó wrote:

Then, assuming univalence, we have (theorem of intensional MLTT+UA):

  (A=B) = ∀(x:X), x ∈ A ⇔ x ∈ B.

(Because the middle equality is that of two sets, we don't need to

worry about which specific equality we pick - there is at most

one. This again relies on univalence.)

It is an equality of two *propositions*, of course, which is what I meant to say.

M.

 

[Matt Oliveri]

On Friday, December 22, 2017 at 4:20:21 PM UTC-5, Martín Hötzel Escardó wrote:

There may be some confusion about univalence and equality of subsets

of a type. 

[...]

Now, from a subset A : ℙ X, we get a type A' and an embedding A' → X.

(The construction works like this: we have A : X → Prop, and a

projection Prop → U. Then the type A' is the sum (Σ) of composite

function. The embedding is the first projection.)

It is definitely not the case that if A'=B' for A,B : ℙ X then A=B.

[...]

All the misunderstandings in the previous messages are caused by

looking at the particular type X=1 without enough care.

And I think this is what Thomas is pointing out.

Huh? Your isEven/isOdd example is fine, but there, X ≠ 1. Is it not the case that if A'=B' for A,B : ℙ 1 then A=B? (Note the specialization to 1.)