Meta-conjecture about MLTT

Meta-conjecture about MLTT

[Martin Escardo]

In MLTT with equality reflection, we cannot distinguish isomorphic types.

There was some agreement regarding this in previous discussions here in 
this list in the past (I think).

But I don't think we actually saw a proof (have we?). As far as I 
understand, we only saw that natural attempts to distinguish examples of 
isomorphic types fail. There was some invokation of realizability models 
to try to justify this. But I am not (yet) convinced by the arguments I 
have seen so far.

Nevertheless, I am convinced that equality reflection in MLTT cannot be 
used to distinguish any particular pair of isomorphic types. (Prove me 
wrong.)

The meta-task is to either produce two isomorphic types in an empty 
context, together with a property that one of them provably has but the 
other doesn't, or to show that this is impossible.

I am strongly inclined to think that this is impossible: that so-called 
extensional MLTT cannot distinguish isomorphic types.

In particular, equality-reflection has nothing whatsoever to do 5with 
elementwise equality.

Of course, what makes this difficult is that MLTT with equality 
reflection is inconsistent with univalence.


Martin

Re: [HoTT] Meta-conjecture about MLTT

[Peter LeFanu Lumsdaine]

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

As you conjecture, MLTT with equality reflection can’t distinguish between
isomorphic types.

Precisely, let MLTT[X] be the extension of MLTT by a single closed base
type X.

Suppose \C is a model of MLTT — presented as a CwA with appropriate extra
logical structure — and A, B are two isomorphic types in it, over the empty
context.  So A, B induce two interpretations of MLTT[X] in \C.

Then there’s a CwA \C^\iso, with the category of isomorphisms in \C, and
with a type over an iso Г1 <~> Г2 being a pair of types A1, A2 over Г1, Г2
that correspond under reindexing along the isomorphism.

Now I claim this carries suitable structure to again model MLTT[X], and
furthermore (importantly) such that the two projection maps \C^\iso —> \C
both preserve all the logical structure.  For most logical type-formers
(Pi’s, Sigma’s, etc), the structure is by showing that these type-formers
are provably functorial in isomorphisms.  (This uses the equality
reflection.)  For the universe(s), this just uses the identity iso on the
universe(s) of \C.  The base type X, we model by the given isomorphism A
<~> B.

So this induces an interpretation of MLTT[X] in \C^\iso, whose two
projections to \C are the two original interpretations in \C.

In particular, if P is any type in MLTT[X] — i.e. a property of an
arbitrary type definable in MLTT — then its interpretation in \C^\iso is an
isomorphism P[A] <~> P[B].  I think this is a reasonable positive answer to
your question?

I don’t remember anywhere this construction appears in the literature, but
I’ve always assumed that it has been noted before.  (Actually, I’d be very
glad to hear a reference if anyone remembers seeing this somewhere, even if
only in folklore not in print.)  Without identity reflection, it no longer
works — since one doesn’t know that the logical structure in \C respects
isomorphisms between types — but essentially the same approach works once
one replaces isomorphisms by equivalences.  This is in the work of Chris
Kapulkin’s and mine that I presented in Bonn in February, which we hope to
have written up very soon…

Best,
–Peter.


On Sun, Sep 11, 2016 at 10:47 PM, 'Martin Escardo' via Homotopy Type Theory
<HomotopyT...@googlegroups.com> wrote:

> In MLTT with equality reflection, we cannot distinguish isomorphic types.
>
> There was some agreement regarding this in previous discussions here in
> this list in the past (I think).
>
> But I don't think we actually saw a proof (have we?). As far as I
> understand, we only saw that natural attempts to distinguish examples of
> isomorphic types fail. There was some invokation of realizability models to
> try to justify this. But I am not (yet) convinced by the arguments I have
> seen so far.
>
> Nevertheless, I am convinced that equality reflection in MLTT cannot be
> used to distinguish any particular pair of isomorphic types. (Prove me
> wrong.)
>
> The meta-task is to either produce two isomorphic types in an empty
> context, together with a property that one of them provably has but the
> other doesn't, or to show that this is impossible.
>
> I am strongly inclined to think that this is impossible: that so-called
> extensional MLTT cannot distinguish isomorphic types.
>
> In particular, equality-reflection has nothing whatsoever to do 5with
> elementwise equality.
>
> Of course, what makes this difficult is that MLTT with equality reflection
> is inconsistent with univalence.
>
>
> Martin
>
>
> --
> 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.
>

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

Re: [HoTT] Meta-conjecture about MLTT

[Martin Escardo]

Nice.

Would you agree with the following imprecise understanding of your 
construction:

Given any interpretation of the theory, any type can be substituted by 
an isomorphic copy to again get an interpretation, (even) in the 
presence of equality reflection.

Or is more going on in your construction?

Martin

Martin En 11/09/16 23:08, Peter LeFanu Lumsdaine wrote:
> As you conjecture, MLTT with equality reflection can’t distinguish
> between isomorphic types.
>
> Precisely, let MLTT[X] be the extension of MLTT by a single closed base
> type X.
>
> Suppose \C is a model of MLTT — presented as a CwA with appropriate
> extra logical structure — and A, B are two isomorphic types in it, over
> the empty context.  So A, B induce two interpretations of MLTT[X] in \C.
>
> Then there’s a CwA \C^\iso, with the category of isomorphisms in \C, and
> with a type over an iso Г1 <~> Г2 being a pair of types A1, A2 over Г1,
> Г2 that correspond under reindexing along the isomorphism.
>
> Now I claim this carries suitable structure to again model MLTT[X], and
> furthermore (importantly) such that the two projection maps \C^\iso —>
> \C both preserve all the logical structure.  For most logical
> type-formers (Pi’s, Sigma’s, etc), the structure is by showing that
> these type-formers are provably functorial in isomorphisms.  (This uses
> the equality reflection.)  For the universe(s), this just uses the
> identity iso on the universe(s) of \C.  The base type X, we model by the
> given isomorphism A <~> B.
>
> So this induces an interpretation of MLTT[X] in \C^\iso, whose two
> projections to \C are the two original interpretations in \C.
>
> In particular, if P is any type in MLTT[X] — i.e. a property of an
> arbitrary type definable in MLTT — then its interpretation in \C^\iso is
> an isomorphism P[A] <~> P[B].  I think this is a reasonable positive
> answer to your question?
>
> I don’t remember anywhere this construction appears in the literature,
> but I’ve always assumed that it has been noted before.  (Actually, I’d
> be very glad to hear a reference if anyone remembers seeing this
> somewhere, even if only in folklore not in print.)  Without identity
> reflection, it no longer works — since one doesn’t know that the logical
> structure in \C respects isomorphisms between types — but essentially
> the same approach works once one replaces isomorphisms by equivalences.
> This is in the work of Chris Kapulkin’s and mine that I presented in
> Bonn in February, which we hope to have written up very soon…
>
> Best,
> –Peter.
>
>
> On Sun, Sep 11, 2016 at 10:47 PM, 'Martin Escardo' via Homotopy Type
> Theory <HomotopyT...@googlegroups.com
> <mailto:HomotopyT...@googlegroups.com>> wrote:
>
>     In MLTT with equality reflection, we cannot distinguish isomorphic
>     types.
>
>     There was some agreement regarding this in previous discussions here
>     in this list in the past (I think).
>
>     But I don't think we actually saw a proof (have we?). As far as I
>     understand, we only saw that natural attempts to distinguish
>     examples of isomorphic types fail. There was some invokation of
>     realizability models to try to justify this. But I am not (yet)
>     convinced by the arguments I have seen so far.
>
>     Nevertheless, I am convinced that equality reflection in MLTT cannot
>     be used to distinguish any particular pair of isomorphic types.
>     (Prove me wrong.)
>
>     The meta-task is to either produce two isomorphic types in an empty
>     context, together with a property that one of them provably has but
>     the other doesn't, or to show that this is impossible.
>
>     I am strongly inclined to think that this is impossible: that
>     so-called extensional MLTT cannot distinguish isomorphic types.
>
>     In particular, equality-reflection has nothing whatsoever to do
>     5with elementwise equality.
>
>     Of course, what makes this difficult is that MLTT with equality
>     reflection is inconsistent with univalence.
>
>
>     Martin
>
>
>     --
>     You received this message because you are subscribed to the Google
>     Groups "Homotopy Type Theory" group.
>     To unsubscribe from this group and stop receiving emails from it,
>     send an email to HomotopyTypeThe...@googlegroups.com
>     <mailto:HomotopyTypeTheo...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>
>

Re: Meta-conjecture about MLTT

[Andrew Polonsky]

[-- Attachment #1.1: Type: text/plain, Size: 400 bytes --]


>
> The meta-task is to either produce two isomorphic types in an empty 
> context, together with a property that one of them provably has but the 
> other doesn't, or to show that this is impossible. 
>

What do you mean by a "property", exactly?

If you mean a type family, e.g.,

    X : U |-  P(X) : Type

then a counterexample is

A = Nat x Bool
B = Bool x Nat
P(X) = Id(U;X,A)

Cheers,
Andrew

[-- Attachment #1.2: Type: text/html, Size: 746 bytes --]

Re: [HoTT] Re: Meta-conjecture about MLTT

[Jason Gross]

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

I suspect "one of them provably has but the other doesn't" should mean "one
of them provably has but the other provably does not have".

On Sun, Sep 11, 2016 at 10:20 PM Andrew Polonsky <andrew....@gmail.com>
wrote:

> The meta-task is to either produce two isomorphic types in an empty
>> context, together with a property that one of them provably has but the
>> other doesn't, or to show that this is impossible.
>>
>
> What do you mean by a "property", exactly?
>
> If you mean a type family, e.g.,
>
>     X : U |-  P(X) : Type
>
> then a counterexample is
>
> A = Nat x Bool
> B = Bool x Nat
> P(X) = Id(U;X,A)
>
> Cheers,
> Andrew
>
> --
> 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.
>

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

Re: [HoTT] Meta-conjecture about MLTT

[Thomas Streicher]

Peter,

I think that doesn't work. Your example is just a presheaf topos and
thus a model of extensional type theory. Interpreting equality on the
universe as diagonal will not identify all isomorphic types.

I am afraid Martin's question is a tricky one. In models of
extensional type theory as we all know isomorphic types typically are
not equal. But Martin asks about the initial model and such questions
are tricky. But, maybe glueing (aka sconing) helps?

Thomas


> As you conjecture, MLTT with equality reflection can???t distinguish between
> isomorphic types.
> 
> Precisely, let MLTT[X] be the extension of MLTT by a single closed base
> type X.
> 
> Suppose \C is a model of MLTT ??? presented as a CwA with appropriate extra
> logical structure ??? and A, B are two isomorphic types in it, over the empty
> context.  So A, B induce two interpretations of MLTT[X] in \C.
> 
> Then there???s a CwA \C^\iso, with the category of isomorphisms in \C, and
> with a type over an iso ??1 <~> ??2 being a pair of types A1, A2 over ??1, ??2
> that correspond under reindexing along the isomorphism.
> 
> Now I claim this carries suitable structure to again model MLTT[X], and
> furthermore (importantly) such that the two projection maps \C^\iso ???> \C
> both preserve all the logical structure.  For most logical type-formers
> (Pi???s, Sigma???s, etc), the structure is by showing that these type-formers
> are provably functorial in isomorphisms.  (This uses the equality
> reflection.)  For the universe(s), this just uses the identity iso on the
> universe(s) of \C.  The base type X, we model by the given isomorphism A
> <~> B.
> 
> So this induces an interpretation of MLTT[X] in \C^\iso, whose two
> projections to \C are the two original interpretations in \C.
> 
> In particular, if P is any type in MLTT[X] ??? i.e. a property of an
> arbitrary type definable in MLTT ??? then its interpretation in \C^\iso is an
> isomorphism P[A] <~> P[B].  I think this is a reasonable positive answer to
> your question?
> 
> I don???t remember anywhere this construction appears in the literature, but
> I???ve always assumed that it has been noted before.  (Actually, I???d be very
> glad to hear a reference if anyone remembers seeing this somewhere, even if
> only in folklore not in print.)  Without identity reflection, it no longer
> works ??? since one doesn???t know that the logical structure in \C respects
> isomorphisms between types ??? but essentially the same approach works once
> one replaces isomorphisms by equivalences.  This is in the work of Chris
> Kapulkin???s and mine that I presented in Bonn in February, which we hope to
> have written up very soon???
> 
> Best,
> ???Peter.
> 
> 
> On Sun, Sep 11, 2016 at 10:47 PM, 'Martin Escardo' via Homotopy Type Theory
> <HomotopyT...@googlegroups.com> wrote:
> 
> > In MLTT with equality reflection, we cannot distinguish isomorphic types.
> >
> > There was some agreement regarding this in previous discussions here in
> > this list in the past (I think).
> >
> > But I don't think we actually saw a proof (have we?). As far as I
> > understand, we only saw that natural attempts to distinguish examples of
> > isomorphic types fail. There was some invokation of realizability models to
> > try to justify this. But I am not (yet) convinced by the arguments I have
> > seen so far.
> >
> > Nevertheless, I am convinced that equality reflection in MLTT cannot be
> > used to distinguish any particular pair of isomorphic types. (Prove me
> > wrong.)
> >
> > The meta-task is to either produce two isomorphic types in an empty
> > context, together with a property that one of them provably has but the
> > other doesn't, or to show that this is impossible.
> >
> > I am strongly inclined to think that this is impossible: that so-called
> > extensional MLTT cannot distinguish isomorphic types.
> >
> > In particular, equality-reflection has nothing whatsoever to do 5with
> > elementwise equality.
> >
> > Of course, what makes this difficult is that MLTT with equality reflection
> > is inconsistent with univalence.
> >
> >
> > Martin
> >
> >
> >
> 

Re: [HoTT] Re: Meta-conjecture about MLTT

[Andrew Polonsky]

> I suspect "one of them provably has but the other doesn't" should mean "one
> of them provably has but the other provably does not have".

Type theory with reflection rule usually contains the rule equating
all proofs of equality:

       p : Id(A;x,y)
---------------------------
  p == refl : Id(A;x,y)

If this is admitted, then the following modified example works:

A = Id(U;Bool,Bool)
B = Iso(Bool,Bool)
P(X) = Id(U;A,X)

Clearly, P(A).  Suppose P(B).  By equality reflection, A == B : U.
But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x == refl.
Since this holds for arbitrary x, we have x==y for arbitrary x,y :
Iso(Bool,Bool), a contradiction.

Generally, I think any proof that equality reflection is inconsistent
with univalence could be adapted to yield a counterexample as above.

Cheers,
Andrew

Re: [HoTT] Re: Meta-conjecture about MLTT

[Andrew Polonsky]

[-- Attachment #1.1: Type: text/plain, Size: 1072 bytes --]

Hm, the two types are not provably isomorphic... Ok, this is a tricky 
question indeed!

On Monday, September 12, 2016 at 11:55:45 AM UTC+2, Andrew Polonsky wrote:
>
> > I suspect "one of them provably has but the other doesn't" should mean 
> "one 
> > of them provably has but the other provably does not have". 
>
> Type theory with reflection rule usually contains the rule equating 
> all proofs of equality: 
>
>        p : Id(A;x,y) 
> --------------------------- 
>   p == refl : Id(A;x,y) 
>
> If this is admitted, then the following modified example works: 
>
> A = Id(U;Bool,Bool) 
> B = Iso(Bool,Bool) 
> P(X) = Id(U;A,X) 
>
> Clearly, P(A).  Suppose P(B).  By equality reflection, A == B : U. 
> But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x == 
> refl. 
> Since this holds for arbitrary x, we have x==y for arbitrary x,y : 
> Iso(Bool,Bool), a contradiction. 
>
> Generally, I think any proof that equality reflection is inconsistent 
> with univalence could be adapted to yield a counterexample as above. 
>
> Cheers, 
> Andrew 
>

[-- Attachment #1.2: Type: text/html, Size: 1319 bytes --]

Re: [HoTT] Re: Meta-conjecture about MLTT

[Peter LeFanu Lumsdaine]

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

On Mon, Sep 12, 2016 at 7:20 AM, Andrew Polonsky <andrew....@gmail.com>
wrote:

> The meta-task is to either produce two isomorphic types in an empty
>> context, together with a property that one of them provably has but the
>> other doesn't, or to show that this is impossible.
>>
>
> What do you mean by a "property", exactly?
>

There’s also a difference in what you mean by a “type”, which is I think
the key difference between the argument I gave, and Andrew’s counterexample
(and others’).

The counterexamples show that there can be properties of *small* types,
i.e. type families [ X : U |— P(X) Type ], which can distinguish isomorphic
(small) types.

The construction I described shows that no property of *all* types — i.e.
no type [ . |— P(X) Type ], where X is a new base type, so any closed type
can be substituted for X — can distinguish isomorphic types.

–p.

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

Re: [HoTT] Re: Meta-conjecture about MLTT

[Nicolai Kraus]

On 12/09/16 10:55, Andrew Polonsky wrote:
> Type theory with reflection rule usually contains the rule equating
> all proofs of equality:
>
>         p : Id(A;x,y)
> ---------------------------
>    p == refl : Id(A;x,y)
>
> If this is admitted,

This is a consequence of the equality reflection rule, isn't it?
-- Nicolai

> then the following modified example works:
>
> A = Id(U;Bool,Bool)
> B = Iso(Bool,Bool)
> P(X) = Id(U;A,X)
>
> Clearly, P(A).  Suppose P(B).  By equality reflection, A == B : U.
> But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x == refl.
> Since this holds for arbitrary x, we have x==y for arbitrary x,y :
> Iso(Bool,Bool), a contradiction.
>
> Generally, I think any proof that equality reflection is inconsistent
> with univalence could be adapted to yield a counterexample as above.
>
> Cheers,
> Andrew
>

Re: [HoTT] Meta-conjecture about MLTT

[Nicolai Kraus]

On 11/09/16 21:47, 'Martin Escardo' via Homotopy Type Theory wrote:
> The meta-task is to either produce two isomorphic types in an empty 
> context, together with a property that one of them provably has but 
> the other doesn't, or to show that this is impossible.
> [...]
> Of course, what makes this difficult is that MLTT with equality 
> reflection is inconsistent with univalence.

A strengthened version of your question would be:

"Is MLTT with equality reflection and the axiom ua : Iso(A,B) -> Id(A,B) 
consistent?"

I would expect this to be the case. The reason why full univalence is 
inconsistent is that it contradicts K, but I would be surprised if the 
*function* ua was already a problem. (Similarly, I guess you can have 
univalence in an equality-reflection theory without universes and HITs.)
-- Nicolai

Re: [HoTT] Meta-conjecture about MLTT

[Andrej Bauer]

Let me try.

Consider the model of MLTT in the skeleton of sets, i.e., types are
interpreted as cardinal numbers and functions are the set-theoretic
functions between cardinals. The identity type is just what you'd
expect in a set-theoretic model (in fact, there is *no* choice about
i). There are no problems of coherence anywhere.

This model validates equality reflection. If MLTT+reflection
distinguished isomorphic types, then there would exist in this model
two isomorphic types which are not equal, but since we started with a
skeleton this will not do.

It is a bit amusing that the model also validates things like Id(U,
Nat -> Nat, Nat -> Bool) and is thus quite educational.

It is a model, right?

With kind regards,

Andrej

Re: [HoTT] Meta-conjecture about MLTT

[Thomas Streicher]

I am afraid this skeleton model is not split and spliiting it it wan't
be a skeleton anymore.

Thomas


On Mon, Sep 12, 2016 at 01:02:24PM +0200, Andrej Bauer wrote:
> Let me try.
> 
> Consider the model of MLTT in the skeleton of sets, i.e., types are
> interpreted as cardinal numbers and functions are the set-theoretic
> functions between cardinals. The identity type is just what you'd
> expect in a set-theoretic model (in fact, there is *no* choice about
> i). There are no problems of coherence anywhere.
> 
> This model validates equality reflection. If MLTT+reflection
> distinguished isomorphic types, then there would exist in this model
> two isomorphic types which are not equal, but since we started with a
> skeleton this will not do.
> 
> It is a bit amusing that the model also validates things like Id(U,
> Nat -> Nat, Nat -> Bool) and is thus quite educational.
> 
> It is a model, right?
> 
> With kind regards,
> 
> Andrej
> 

Re: [HoTT] Meta-conjecture about MLTT

[Andrew Polonsky]

Perhaps one does not need to take a skeleton.

A dependent type x:U |- P(X) : Type gives rise, in the *standard*
set-theoretic model, to a family of sets indexed by [[U]].

Since the standard type constructor preserve isomorphism, two fibers
[[P(A)]] and [[P(B)]] will be isomorphic if A and B are.

Saying "A provably has property P" translates into "[[P(A)]] is
inhabited by a definable element".

In principle, one could conceive that [[P(B)]] has no definable
elements, even if the two are isomorphic.

But saying that "B provably does not have property P" translates into
"[[P(B)]] is empty", which cannot be the case.

Cheers,
Andrew

On Mon, Sep 12, 2016 at 1:14 PM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> I am afraid this skeleton model is not split and spliiting it it wan't
> be a skeleton anymore.
>
> Thomas
>
>
> On Mon, Sep 12, 2016 at 01:02:24PM +0200, Andrej Bauer wrote:
>> Let me try.
>>
>> Consider the model of MLTT in the skeleton of sets, i.e., types are
>> interpreted as cardinal numbers and functions are the set-theoretic
>> functions between cardinals. The identity type is just what you'd
>> expect in a set-theoretic model (in fact, there is *no* choice about
>> i). There are no problems of coherence anywhere.
>>
>> This model validates equality reflection. If MLTT+reflection
>> distinguished isomorphic types, then there would exist in this model
>> two isomorphic types which are not equal, but since we started with a
>> skeleton this will not do.
>>
>> It is a bit amusing that the model also validates things like Id(U,
>> Nat -> Nat, Nat -> Bool) and is thus quite educational.
>>
>> It is a model, right?
>>
>> With kind regards,
>>
>> Andrej
>>
>
> --
> You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/_cgjnmRvcUU/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] Meta-conjecture about MLTT

[Thomas Streicher]

the fibres will just be equivalent in general
but for Fam(Set) they are isomorphic

On Mon, Sep 12, 2016 at 01:23:09PM +0200, Andrew Polonsky wrote:
> Perhaps one does not need to take a skeleton.
> 
> A dependent type x:U |- P(X) : Type gives rise, in the *standard*
> set-theoretic model, to a family of sets indexed by [[U]].
> 
> Since the standard type constructor preserve isomorphism, two fibers
> [[P(A)]] and [[P(B)]] will be isomorphic if A and B are.
> 
> Saying "A provably has property P" translates into "[[P(A)]] is
> inhabited by a definable element".
> 
> In principle, one could conceive that [[P(B)]] has no definable
> elements, even if the two are isomorphic.
> 
> But saying that "B provably does not have property P" translates into
> "[[P(B)]] is empty", which cannot be the case.
> 
> Cheers,
> Andrew
> 
> On Mon, Sep 12, 2016 at 1:14 PM, Thomas Streicher
> <stre...@mathematik.tu-darmstadt.de> wrote:
> > I am afraid this skeleton model is not split and spliiting it it wan't
> > be a skeleton anymore.
> >
> > Thomas
> >
> >
> > On Mon, Sep 12, 2016 at 01:02:24PM +0200, Andrej Bauer wrote:
> >> Let me try.
> >>
> >> Consider the model of MLTT in the skeleton of sets, i.e., types are
> >> interpreted as cardinal numbers and functions are the set-theoretic
> >> functions between cardinals. The identity type is just what you'd
> >> expect in a set-theoretic model (in fact, there is *no* choice about
> >> i). There are no problems of coherence anywhere.
> >>
> >> This model validates equality reflection. If MLTT+reflection
> >> distinguished isomorphic types, then there would exist in this model
> >> two isomorphic types which are not equal, but since we started with a
> >> skeleton this will not do.
> >>
> >> It is a bit amusing that the model also validates things like Id(U,
> >> Nat -> Nat, Nat -> Bool) and is thus quite educational.
> >>
> >> It is a model, right?
> >>
> >> With kind regards,
> >>
> >> Andrej
> >>
> >

Re: [HoTT] Meta-conjecture about MLTT

[Thomas Streicher]

> The meta-task is to either produce two isomorphic types in an empty context,
> together with a property that one of them provably has but the other
> doesn't, or to show that this is impossible.

This seems to be hard but in my eyes is not the right question. What
Andrew has shown is that there are definable isomorphic types A and B
in a universe U and a predicate P on this universe where P(A) is
inhabited but P(B)° isnot. Actually, this argument is generic since
one may take P(X)  = IdU;A,X).

It's like in programming language semantics. One thing is to
distinguish by maps to 2 and another is to distinguis by maps to \Sigma.
Inhabited plays the role of \top and not inhabited plays the role of \bot.

Thomas

Re: [HoTT] Meta-conjecture about MLTT

[Martin Escardo]

On 12/09/16 13:47, Thomas Streicher wrote:
>> The meta-task is to either produce two isomorphic types in an empty context,
>> together with a property that one of them provably has but the other
>> doesn't, or to show that this is impossible.
> 
> This seems to be hard but in my eyes is not the right question. What
> Andrew has shown is that there are definable isomorphic types A and B
> in a universe U and a predicate P on this universe where P(A) is
> inhabited but P(B)° isnot. Actually, this argument is generic since
> one may take P(X)  = IdU;A,X).
> 
> It's like in programming language semantics. One thing is to
> distinguish by maps to 2 and another is to distinguis by maps to \Sigma.
> Inhabited plays the role of \top and not inhabited plays the role of \bot.
> 
> Thomas
> 

Thanks to all who contributed to the discussion (in the list and
off-list - but the off-list remarks made it in to the list independently
by other contributors).

My formulation of the question was ambiguous, with different answers
depending on how we make it precise, and with an unknown answer for one
particular way of making it precise.

Best,
Martin