55 views

Skip to first unread message

Mar 2, 2014, 7:31:26 PM3/2/14

to HomotopyT...@googlegroups.com

I wonder whether it is already known that an interval can be obtained

as the propositional truncation of bool. Here is a formalization:

, which is based on Voevodsky's Foundations package and runs

under a patched version of coq's source code repository trunk.

The definition of the propositional truncation of his is here:

Mar 2, 2014, 7:54:19 PM3/2/14

to HomotopyT...@googlegroups.com

It is a nice observation. Martin also made that comment, he has done it

in Agda:

http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#6060

> --

> 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/groups/opt_out.

in Agda:

http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#6060

> 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/groups/opt_out.

Mar 2, 2014, 10:43:52 PM3/2/14

to Nicolai Kraus, HomotopyT...@googlegroups.com

This is the sort of fact that would be useful to record on the new wiki:

http://ncatlab.org/homotopytypetheory

Wikis are great for recording little facts like this that maybe aren't

important enough to write a whole paper about, but that it's good to

write down somewhere so that people don't have to keep re-discovering

them. Anyone want to make a page for it?

http://ncatlab.org/homotopytypetheory

Wikis are great for recording little facts like this that maybe aren't

important enough to write a whole paper about, but that it's good to

write down somewhere so that people don't have to keep re-discovering

them. Anyone want to make a page for it?

Mar 2, 2014, 11:45:26 PM3/2/14

to Nicolai Kraus, HomotopyT...@googlegroups.com

as Dan has observed, we then get functional extensionality.

surprising that propositional truncation implies function extensionality!

surprising that propositional truncation implies function extensionality!

Mar 3, 2014, 12:02:14 AM3/3/14

to Steve Awodey, Nicolai Kraus, HomotopyT...@googlegroups.com

I find both of these proofs very difficult to read. Can anyone write

out the argument in informal language?

out the argument in informal language?

Mar 3, 2014, 2:04:46 AM3/3/14

to HomotopyT...@googlegroups.com

And I advertised it in this list, and my file also observes that it

gives function extensionality (with two different proofs).

Martin

--

Martin Escardo

http://www.cs.bham.ac.uk/~mhe

gives function extensionality (with two different proofs).

Martin

Martin Escardo

http://www.cs.bham.ac.uk/~mhe

Mar 3, 2014, 5:18:48 AM3/3/14

to Michael Shulman, Steve Awodey, Nicolai Kraus, HomotopyT...@googlegroups.com

On 03/03/14 05:02, Michael Shulman wrote:

> I find both of these proofs very difficult to read. Can anyone write

> out the argument in informal language?

(judgementally for the first order equations and propositional for the

second order equations) was in this thread, back in July:

https://groups.google.com/forum/#!topic/homotopytypetheory/KyJZKbbr1SM

The proof is easy and short. The only trick is to come up with a

suitable proposition to work with.

Assume a type two with points 0,1:2, and let ||-|| denote the

(-1)-truncation.

Define I = ||2||, and let seg : |0| = |1| the path arising from the

definition of ||-|| (I call it the "truncation path").

The end-points of I are taken to be |0| and |1|, of course.

Given points x0,x1:X and a path p:x0=x1, we wish to build g:I->X such

that g|0|=x0 and g|1|=x1 (judgementally), and ap g seg = p

(propositionally).

The trouble is that X is not assumed to be a proposition, and hence

the recursion principle for ||-|| can't be used.

So work instead with paths-from x0, i.e. Sigma(x:X).x0=x, which is a

proposition.

Now define f:2->paths-from x0 by

f 0 = (x0, refl)

f 1 = (x1, p)

By the recursion principle for ||-||, f "extends" to

g':||2||->paths-from x0.

Now define g:||2||->X to be g' composed with the first projection,

which I call "endpoint" in this discussion.

You can check that g|0|=x0 and g|1|=x1 judgementally, by simply

expanding the definitions (or with Agda, as the proof refl is accepted).

The proof that ap g seg = p is equally easy. It suffices to consider

x0,x1 the same, say x, and p=refl x, in a proof by induction.

We have, in this case,

ap g' seg = refl (x,refl x),

using the fact that ||2|| is an proposition and hence an set.

Applying the first projection (called "end-point") to this path, we

get

ap end-point (ap g' seg) = ap end-point (refl (x,refl x)),

Now the lhs is equal to

ap (end-point o g') seg

and in turn, by the definition of g, to

ap g seg.

And the rhs is refl by the definition of ap. Putting this together, we get

ap g seg = refl

and our proof by induction is complete. Q.E.D.

Moreover, it is known that recursion on I gives induction. However, as

far as I know, it doesn't give it judgementally. Hence in the Agda

file I also include a proof that the induction principle for the

interval does hold judgementally if we take I=||2||.

Additionally, the above proof technique can be used to show that if a

function f:X->Y factors through |-|:X->||X||, then we can find a

judgemental factorization. Also in that file. Nicolai then used this

to define his mysterious pseudo-inverse of |-|:X->||X||.

To conclude, here is an observation. We discussed constancy (many

times) in this list.

Mike's definition is that f:X->Y is constant iff we are in possession

of y:Y such that f=\lambda x.y. Let's adopt this terminology. (In the

Agda file I call this "constant-valued".)

It is easy to see that f:X->Y has a factor through |-|:X->||X|| iff

||X||->constant f.

Martin

Mar 3, 2014, 7:56:53 AM3/3/14

to Martin Escardo, Michael Shulman, Steve Awodey, Nicolai Kraus, HomotopyT...@googlegroups.com

The proof I found is the same as what Martin describes. His

"paths-from" is Vladimir's "coconustot", which seems to mean

"co-cone to t".

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/groups/opt_out.

--

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/groups/opt_out.

--

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/groups/opt_out.

Martin Escardo

--

http://www.cs.bham.ac.uk/~mhe

--

You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

unsub...@googlegroups.com.

Mar 3, 2014, 9:11:12 AM3/3/14

to Martin Escardo, HomotopyT...@googlegroups.com

sorry I missed this.

as Mike said, a good reason to start collecting things on the wiki.

as Mike said, a good reason to start collecting things on the wiki.

Mar 3, 2014, 11:00:53 AM3/3/14

to Daniel R. Grayson, HomotopyT...@googlegroups.com

Dan, I thick it is important to emphasize that this construction also shows how to prove functional extensionality from propositional truncation.

V.

Mar 3, 2014, 11:04:17 AM3/3/14

to Martin Escardo, Steve Awodey, Nicolai Kraus, HomotopyT...@googlegroups.com

Thanks; this is very nice! (Your original post didn't include an

informal description of the argument either, did it? Or did I just

miss it?)

We should put this in the book; an exercise in chapter 6, I guess.

Who's going to put it on the wiki?

informal description of the argument either, did it? Or did I just

miss it?)

We should put this in the book; an exercise in chapter 6, I guess.

Who's going to put it on the wiki?

Mar 3, 2014, 11:13:59 AM3/3/14

to Martin Escardo, HomotopyT...@googlegroups.com

On Mar 3, 2014, at 2:04 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> And I advertised it in this list, and my file also observes that it gives function extensionality (with two different proofs).

V.

Mar 3, 2014, 11:25:36 AM3/3/14

to Martin Escardo, Nicolai Kraus, HomotopyT...@googlegroups.com

On Mar 3, 2014, at 5:18 AM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

Also in that file. Nicolai then used this

to define his mysterious pseudo-inverse of |-|:X->||X||.

Can you remind what this is about?

Vladimir.

Mar 3, 2014, 12:12:11 PM3/3/14

to Vladimir Voevodsky, HomotopyT...@googlegroups.com

http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html

This contains many more things, including the fact that propositional

truncation gives function extensionality, without considering the interval.

The interval begins here:

http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html#6060

Then there are facts about factorizations of functions through ||-||.

Martin

Mar 3, 2014, 12:21:54 PM3/3/14

to Vladimir Voevodsky, Nicolai Kraus, HomotopyT...@googlegroups.com

On 03/03/14 16:25, Vladimir Voevodsky wrote:

>

> On Mar 3, 2014, at 5:18 AM, Martin Escardo <m.es...@cs.bham.ac.uk

> <mailto:m.es...@cs.bham.ac.uk>> wrote:

>

>> Also in that file. Nicolai then used this

>> to define his mysterious pseudo-inverse of |-|:X->||X||.

>

> Can you remind what this is about?

It's a magic trick:
>

>> Also in that file. Nicolai then used this

>> to define his mysterious pseudo-inverse of |-|:X->||X||.

>

> Can you remind what this is about?

http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%8%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/

There is a term myst such that myst |17|=17 and more generally myst

|n|=n for any numeral n. However, the type of myst is not ||nat||->nat.

Martin

Mar 3, 2014, 12:28:00 PM3/3/14

to HomotopyT...@googlegroups.com

On Mon, Mar 3, 2014 at 1:56 PM, Daniel R. Grayson <d...@math.uiuc.edu> wrote:

> The proof I found is the same as what Martin describes. His

> "paths-from" is Vladimir's "coconustot", which seems to mean

> "co-cone to t".

And I always thought there were coconuts in Vladimir's foundations.
> The proof I found is the same as what Martin describes. His

> "paths-from" is Vladimir's "coconustot", which seems to mean

> "co-cone to t".

Mar 3, 2014, 12:29:49 PM3/3/14

to Vladimir Voevodsky, Nicolai Kraus, HomotopyT...@googlegroups.com

As pointed out by Thierry, the link to Nicolai's post below doesn't work.

I don't know how to copy and paste it so that it works (the link has

unicode characters). I use Firefox and Thunderbird, which are standard

browsers and mailers, but copy and paste from one to the other doesn't

work.

The title is "The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible"

and the date is 28 October 2013 in the HoTT blog.

Martin

I don't know how to copy and paste it so that it works (the link has

unicode characters). I use Firefox and Thunderbird, which are standard

browsers and mailers, but copy and paste from one to the other doesn't

work.

The title is "The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible"

and the date is 28 October 2013 in the HoTT blog.

Martin

Mar 3, 2014, 12:31:56 PM3/3/14

to Michael Shulman, Steve Awodey, Nicolai Kraus, HomotopyT...@googlegroups.com

On 03/03/14 16:04, Michael Shulman wrote:

> Thanks; this is very nice! (Your original post didn't include an

> informal description of the argument either, did it?

Anyway, the proof below is the informalization of the Agda proof.

Or did I just

> miss it?)

>

> We should put this in the book; an exercise in chapter 6, I guess.

>

> Who's going to put it on the wiki?

Martin

Mar 3, 2014, 12:34:05 PM3/3/14

to Martin Escardo, Vladimir Voevodsky, Nicolai Kraus, HomotopyT...@googlegroups.com

Mar 3, 2014, 12:40:36 PM3/3/14

to Andrej Bauer, HomotopyT...@googlegroups.com

probably why I got the proof before Dan. Unfair advantage.

Martin

Mar 3, 2014, 1:30:53 PM3/3/14

to Martin Escardo, HomotopyT...@googlegroups.com

On Mar 3, 2014, at 12:21 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>

>

> On 03/03/14 16:25, Vladimir Voevodsky wrote:

>>

>> On Mar 3, 2014, at 5:18 AM, Martin Escardo <m.es...@cs.bham.ac.uk

>> <mailto:m.es...@cs.bham.ac.uk>> wrote:

>>

>>> Also in that file. Nicolai then used this

>>> to define his mysterious pseudo-inverse of |-|:X->||X||.

>>

>> Can you remind what this is about?

>

> It's a magic trick:

>

>

I get “Not Found” when I try to follow the link.

V.

Mar 3, 2014, 1:35:14 PM3/3/14

to Martin Escardo, Prof. Vladimir Aleksandrovich Voevodsky, Nicolai Kraus, HomotopyT...@googlegroups.com

On Mar 3, 2014, at 12:29 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> As pointed out by Thierry, the link to Nicolai's post below doesn't work.

>

> I don't know how to copy and paste it so that it works (the link has unicode characters). I use Firefox and Thunderbird, which are standard browsers and mailers, but copy and paste from one to the other doesn't work.

>

> The title is "The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible" and the date is 28 October 2013 in the HoTT blog.

V.

Mar 3, 2014, 1:56:33 PM3/3/14

to Vladimir Voevodsky, Nicolai Kraus, HomotopyT...@googlegroups.com

applications of coconuts.

Perhaps Nicolai can write a concise informal proof here.

Martin

Mar 3, 2014, 2:32:27 PM3/3/14

to Martin Escardo, Steve Awodey, Nicolai Kraus, HomotopyT...@googlegroups.com

I find it nearly impossible to read Agda code, even when I wrote it

myself. I also find it nearly impossible to read Coq code, even when

I wrote it myself. The only way I can make sense of someone else's

Coq code is by stepping through it interactively, but Agda doesn't

give me that option (nor does Coq when you prove the whole thing with

"exact" the way Dan did).

FYI, it's possible for people writing a blog post to choose the

"permalink" URL. Since unicode characters seem to cause problems for

some people, it might be advisable for future blog posters to omit

them from the URL.

myself. I also find it nearly impossible to read Coq code, even when

I wrote it myself. The only way I can make sense of someone else's

Coq code is by stepping through it interactively, but Agda doesn't

give me that option (nor does Coq when you prove the whole thing with

"exact" the way Dan did).

FYI, it's possible for people writing a blog post to choose the

"permalink" URL. Since unicode characters seem to cause problems for

some people, it might be advisable for future blog posters to omit

them from the URL.

Mar 3, 2014, 2:41:30 PM3/3/14

to Michael Shulman, Daniel R. Grayson, Martin Escardo, Nicolai Kraus, HomotopyT...@googlegroups.com

On Mar 3, 2014, at 2:32 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> I find it nearly impossible to read Agda code, even when I wrote it

> myself. I also find it nearly impossible to read Coq code, even when

> I wrote it myself. The only way I can make sense of someone else's

> Coq code is by stepping through it interactively, but Agda doesn't

> give me that option (nor does Coq when you prove the whole thing with

> "exact" the way Dan did).

: - )

Mar 3, 2014, 2:47:57 PM3/3/14

to Vladimir Voevodsky, Martin Escardo, Nicolai Kraus, HomotopyT...@googlegroups.com

I posted about a variant of it using the interval at http://homotopytypetheory.org/2014/02/24/composition-is-not-what-you-think-it-is-why-nearly-invertible-isnt/, which links to a Coq version of the code that I develop there (https://gist.github.com/JasonGross/9158899).

Btw, the link

works for me.

-Jason

Mar 3, 2014, 3:02:11 PM3/3/14

to HomotopyT...@googlegroups.com

links automatically from the titles and I forgot to change it (maybe the

title should be unicode-free as well).

Ok, I can try to write a concise version of this, but I don't really

know how to do it "informally" since the whole construction is based on

*syntactical* computation properties of the theory.

Anyway, the construction that Martin mentioned goes like this. I write

"N" for the natural numbers type. Following the discussion, if X is a

type and x a point, I write "coconustot X x" for "Sigma (y:X) (y=x)" as

in Vladimir's library. Also, I write "Type*" for the type of pointed

types (an inhabitant of Type* is a pair (A,a), where A is a type and a:A

a point).

Define

f : N -> coconustot Type* (N,0)

f (n) := ((N,n) , u)

where u : (N,n) = (N,0) is a proof constructed from univalence.

coconustot Type* (N,0) is contractible, so we may apply the recursion

principle of ||-|| (propositional truncation) and we get

f' : ||N|| -> coconustot Type* (N,0).

If we compose f' with the first projection, we get

f'' : ||N|| -> Type*

(the second component of the Sigma-type was only there to ensure

contractibility).

f had a contractible codomain, but now we have extracted a function

which does not have a contractible codomain any more.

Define

E : ||N|| -> Type

E (x) := first (f''(x))

myst : (x:||N||) -> E(x)

myst (x) := second (f''(x)).

The trick is that, because of the judgmental beta-rule for the

truncation, the expression

E(|n|)

reduces (is judgmentally equal) to N, for any n:N. (This is not the case

for E(x) with x:||N||.)

Thus, we have

myst o |_| : N -> N

and this composition satisfies

myst(|n|) = n

for all n judgmentally. This makes "myst o |_|" equal to the identity

function on N (it does not mean that we have factored the identity

function through |_|, but it looks as if we had).

Nicolai

Mar 3, 2014, 3:22:15 PM3/3/14

to Nicolai Kraus, HomotopyT...@googlegroups.com

Jason has pointed out (essentially) that we don't need truncation, or

even univalence really, for a similar paradox.

Theorem: for any type A and point a:A, there is a contractible type C,

a type family P : C -> U, a function f : (a=a) -> C, and a dependent

function g : forall (c:C), P(c) such that for any p:a=a we have

P(f(p)) == (a=a) judgmentally and g(f(p)) == p judgmentally, hence "g

o f = id_{a=a}".

Proof: Let C := { x:A & a=x } and f(p) := (a,p), while P(c) := (a =

pr1(c)) and g(c) = pr2(c).

(Of course, we need univalence in order for (a=a) to ever be

noncontractible; otherwise the result is less interesting.)

Mike

even univalence really, for a similar paradox.

Theorem: for any type A and point a:A, there is a contractible type C,

a type family P : C -> U, a function f : (a=a) -> C, and a dependent

function g : forall (c:C), P(c) such that for any p:a=a we have

P(f(p)) == (a=a) judgmentally and g(f(p)) == p judgmentally, hence "g

o f = id_{a=a}".

Proof: Let C := { x:A & a=x } and f(p) := (a,p), while P(c) := (a =

pr1(c)) and g(c) = pr2(c).

(Of course, we need univalence in order for (a=a) to ever be

noncontractible; otherwise the result is less interesting.)

Mike

Mar 3, 2014, 4:49:28 PM3/3/14

to Michael Shulman, Nicolai Kraus, HomotopyT...@googlegroups.com

On 03/03/14 20:22, Michael Shulman wrote:

> Jason has pointed out (essentially) that we don't need truncation, or

> even univalence really, for a similar paradox.

But first:

> Theorem: for any type A and point a:A, there is a contractible type C,

> a type family P : C -> U, a function f : (a=a) -> C, and a dependent

> function g : forall (c:C), P(c) such that for any p:a=a we have

> P(f(p)) == (a=a) judgmentally and g(f(p)) == p judgmentally,

> hence "g o f = id_{a=a}".

> Proof: Let C := { x:A & a=x } and f(p) := (a,p), while P(c) := (a =

> pr1(c)) and g(c) = pr2(c).

I am against referring to this sort of thing as a paradox.

In the case of Nicolai's myst, the deception happens by creating a

term myst, with a non-trivial type *different* from ||nat||->nat, for

which myst|17| happens to type check and be judgementally equal to 17.

I came across a similar situation back in Feb 2012, which I want to

briefly report and discuss here.

Thorsten A. and collaborators asked whether it is the case that for

any two provably distinct closed terms x0, x1 of some closed type X,

there are closed terms p : X -> 2 and d : not(p x0 = p x1). Note the

syntactical (or meta-theoretic) character of the statement, referring

to provability and closed terms.

One can construct a counter-example, which I reported here at that time:

http://www.cs.bham.ac.uk/~mhe/agda/FailureOfTotalSeparatedness.html

My argument is not syntactical or meta-theoretical, but I recover the

meta-theoretical question at the end.

I construct a type X with points

x0, x1 : X,

x0 /= x1,

such that

if there is p:X->2 with p(x0)/=p(x1) then WLPO holds.

Here WLPO is the weak limited principle of omniscience (whatever that

is). This is a proof in type theory, rather than about type

theory. However, because WLPO is known to be not provable (a statement

about type theory), we answer Thorsten et al's question negatively.

Now, as it happens, there is a term P (which has a complicated

type, certainly different from X->2) such that

P x0 = 0

P x1 = 1.

This term was dutifully defined at that time:

http://www.cs.bham.ac.uk/~mhe/agda/FailureOfTotalSeparatedness.html#2542

The point is that this term P does not have type X->2, even if when we

use it with argument x0:X or x1:X we do get a result of type 2.

This "naive" term is very much like Nicolai's "myst" term. It seems to

answer a certain question (which we know can't be answered), but is

actually doing something completely different. There is no paradox at

all. Just deception. (A nice one, which I enjoyed when Nicolai told

me.)

Martin

Mar 3, 2014, 4:56:59 PM3/3/14

to Martin Escardo, Nicolai Kraus, HomotopyT...@googlegroups.com

On Mon, Mar 3, 2014 at 1:49 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

>> hence "g o f = id_{a=a}".

>

> Where the quotes indicate a lie of sorts.

It's not a lie; it just depends on having defined the symbol "o" to
>> hence "g o f = id_{a=a}".

>

> Where the quotes indicate a lie of sorts.

apply to dependent functions as well as non-dependent ones.

> I am against referring to this sort of thing as a paradox.

It's not a paradox in the sense of Cantor's paradox or Russell's

paradox, that yields an actual contradiction unless we modify the

theory. But it is a paradox in the sense of Skolem's paradox, Zeno's

paradox, the Banach-Tarski paradox, etc.: a statement that is

counterintuitive and even seems contradictory, until we learn to

correct our intuitions to match what the theory actually says rather

than what we think it says.

Mike

Mar 3, 2014, 5:08:14 PM3/3/14

to Michael Shulman, Nicolai Kraus, HomotopyT...@googlegroups.com

example of this situation.

In your message before this, you said, rightly, that you don't need

truncation or univalence to get this "paradox".

In my reply, I said that you don't even need coconuts to get such a

"paradox", which I called naiveness at

http://www.cs.bham.ac.uk/~mhe/agda/FailureOfTotalSeparatedness.html#2542

The essence of all these (non-)paradoxes is this: You are in a

situation that you want a function f:X->Y with a certain desirable

behaviour, let's say A(f x) for all x's you are interested in.

Then you prove that no such function exists.

Next, you come up with a term F (certainly not of type X->Y) such that

A(F x) holds for the very same x's you were interested in.

Paradox!

Of course not. This is the nature of dependent types.

It is easy to construct examples like this.

Martin

Mar 3, 2014, 5:23:01 PM3/3/14

to Martin Escardo, Nicolai Kraus, HomotopyT...@googlegroups.com

On Mon, Mar 3, 2014 at 2:08 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

> Paradox!

>

> Of course not. This is the nature of dependent types.

Exactly the same response can be given to the other examples I cited.
> Paradox!

>

> Of course not. This is the nature of dependent types.

Is Skolem's paradox a paradox? Of course not; this is the nature of

first-order logic.

Is Zeno's paradox a paradox? Of course not; this is the nature of

infinite sums.

Is the Banach-Tarski paradox a paradox? Of course not; this is the

nature of nonmeasurable sets.

But in all cases, we still use the word "paradox", because to someone

not yet fully familiar with "the nature of" the subject in question,

the result *seems* contradictory.

Mar 3, 2014, 5:30:08 PM3/3/14

to Michael Shulman, Nicolai Kraus, HomotopyT...@googlegroups.com

reasoning with mine, dependent types are paradoxical.

No need to agree or disagree with this joke, I hope, modulo the fact

that there is a grain of truth in every joke, as the saying goes.

Martin

Mar 3, 2014, 7:01:24 PM3/3/14

to Michael Shulman, Nicolai Kraus, HomotopyT...@googlegroups.com

I want to justify this:

On 03/03/14 22:08, Martin Escardo wrote:

> The essence of all these (non-)paradoxes is this: You are in a

> situation that you want a function f:X->Y with a certain desirable

> behaviour, let's say A(f x) for all x's you are interested in.

>

> Then you prove that no such function exists.

>

> Next, you come up with a term F (certainly not of type X->Y) such that

> A(F x) holds for the very same x's you were interested in.

>

> Paradox!

>

> Of course not. This is the nature of dependent types.

>

> It is easy to construct examples like this.

I am not sure "easy" is the right word. :-) But actually, after the

example I give below, I challenge people to come up with truly trivial

examples. It should be possible.

* The point of the example to be given below is that no subtleties

* about equality arising from HIT's, univalence, function

* extensionality, coconuts etc. are present in the argument.

* None of that is needed. Vanilla type theory suffices.

It must be pointed out that, in all cases I know of (including all

examples discussed in this list by others and me), the above step "no

such function exists" is actually external (or, at best, internalized

as a taboo).

Here, then, is an example of a (non-)paradox that doesn't rely on

coconuts, truncation or univalence, formulated informally.

Start with a type X and a point a:X.

Then define

Y = Sigma(x:X). (x = a) -> 2.

Intuition: Y is the same as X, but with the point a:X "exploded" into

two copies a0,a1:Y. All other points of X have a unique life in Y. To

make this good, define

e : X -> 2 -> Y

e x n = (x, \lambda p.n).

Then the double life of a:X in Y is defined by

a0 = e a 0,

a1 = e a 1.

With some effort, you can show that

a0 /= a1.

(Sounds obvious, until you try.)

Next, for any x:X, we have

x /= a -> e x 0 = e x 1.

(Routine.) This means that such an x has a single life in Y.

Now you can show that

if we have f:Y->2 such that f a0 /= f a1,

then for all x:X, not(x=a) or not(not(x=a)).

(The insight is the construction of Y and the formulation of

this. After this, the proof can probably be regarded as routine.)

Now there are types X with a point a:X such that not(x=a) is not

provably decidable (such as X=(nat->nat)). Hence, for such types, no

such function f:Y->2 is definable. (Of course you cannot prove that no

such function exists.)

However, we have

second-projection a0 refl = 0

second-projection a1 refl = 1

and so if we define

F blah = second-projection blah refl

then

F a0 = 0

F a1 = 1

which seems to contradict that there is no definable f:Y->2 such that

f a0 = 0

f a1 = 1.

The paradox is resolved by noticing that F (with lots of implicit

parameters omitted in its definition) doesn't have type Y->2.

In fact, it is a subtle matter to work out what (dependent) type the

variable blah has in the definition of F.

The dependent function F does have a suitable dependent type, but it is

not Y->2, despite the fact that for our particular a0,a1:Y, we do have

that F a0, F a1 : 2.

* To repeat, the point of this example is that no subtleties about

* equality arising from HIT's, univalence, function extensionality,

* coconuts etc. are present in this argument.

Here instead we use the fact that some types don't have decidable

negate equality. This makes sense in vanilla type theory.

This message is an informal rendering of

www.cs.bham.ac.uk/~mhe/agda/FailureOfTotalSeparatednessBis.html, which

a variation of the file previously linked (except that this assumes

that X is a set, which actually is not needed after all - exercise!).

Martin

On 03/03/14 22:08, Martin Escardo wrote:

> The essence of all these (non-)paradoxes is this: You are in a

> situation that you want a function f:X->Y with a certain desirable

> behaviour, let's say A(f x) for all x's you are interested in.

>

> Then you prove that no such function exists.

>

> Next, you come up with a term F (certainly not of type X->Y) such that

> A(F x) holds for the very same x's you were interested in.

>

> Paradox!

>

> Of course not. This is the nature of dependent types.

>

> It is easy to construct examples like this.

example I give below, I challenge people to come up with truly trivial

examples. It should be possible.

* The point of the example to be given below is that no subtleties

* about equality arising from HIT's, univalence, function

* extensionality, coconuts etc. are present in the argument.

* None of that is needed. Vanilla type theory suffices.

It must be pointed out that, in all cases I know of (including all

examples discussed in this list by others and me), the above step "no

such function exists" is actually external (or, at best, internalized

as a taboo).

Here, then, is an example of a (non-)paradox that doesn't rely on

coconuts, truncation or univalence, formulated informally.

Start with a type X and a point a:X.

Then define

Y = Sigma(x:X). (x = a) -> 2.

Intuition: Y is the same as X, but with the point a:X "exploded" into

two copies a0,a1:Y. All other points of X have a unique life in Y. To

make this good, define

e : X -> 2 -> Y

e x n = (x, \lambda p.n).

Then the double life of a:X in Y is defined by

a0 = e a 0,

a1 = e a 1.

With some effort, you can show that

a0 /= a1.

(Sounds obvious, until you try.)

Next, for any x:X, we have

x /= a -> e x 0 = e x 1.

(Routine.) This means that such an x has a single life in Y.

Now you can show that

if we have f:Y->2 such that f a0 /= f a1,

then for all x:X, not(x=a) or not(not(x=a)).

(The insight is the construction of Y and the formulation of

this. After this, the proof can probably be regarded as routine.)

Now there are types X with a point a:X such that not(x=a) is not

provably decidable (such as X=(nat->nat)). Hence, for such types, no

such function f:Y->2 is definable. (Of course you cannot prove that no

such function exists.)

However, we have

second-projection a0 refl = 0

second-projection a1 refl = 1

and so if we define

F blah = second-projection blah refl

then

F a0 = 0

F a1 = 1

which seems to contradict that there is no definable f:Y->2 such that

f a0 = 0

f a1 = 1.

The paradox is resolved by noticing that F (with lots of implicit

parameters omitted in its definition) doesn't have type Y->2.

In fact, it is a subtle matter to work out what (dependent) type the

variable blah has in the definition of F.

The dependent function F does have a suitable dependent type, but it is

not Y->2, despite the fact that for our particular a0,a1:Y, we do have

that F a0, F a1 : 2.

* To repeat, the point of this example is that no subtleties about

* equality arising from HIT's, univalence, function extensionality,

* coconuts etc. are present in this argument.

Here instead we use the fact that some types don't have decidable

negate equality. This makes sense in vanilla type theory.

This message is an informal rendering of

www.cs.bham.ac.uk/~mhe/agda/FailureOfTotalSeparatednessBis.html, which

a variation of the file previously linked (except that this assumes

that X is a set, which actually is not needed after all - exercise!).

Martin

Mar 3, 2014, 7:50:13 PM3/3/14

to Michael Shulman, HomotopyT...@googlegroups.com

On 03/03/14 20:22, Michael Shulman wrote:

Jason has pointed out (essentially) that we don't need truncation, or even univalence really, for a similar paradox. Theorem: for any type A and point a:A, there is a contractible type C, a type family P : C -> U, a function f : (a=a) -> C, and a dependent function g : forall (c:C), P(c) such that for any p:a=a we have P(f(p)) == (a=a) judgmentally and g(f(p)) == p judgmentally, hence "g o f = id_{a=a}". Proof: Let C := { x:A & a=x } and f(p) := (a,p), while P(c) := (a = pr1(c)) and g(c) = pr2(c). (Of course, we need univalence in order for (a=a) to ever be noncontractible; otherwise the result is less interesting.)

I want to comment quickly. In my original post, I said I had two
main classes of examples of homogeneous/transitive types. Recall
that a type A is homogeneous/transitive (I now prefer the latter
name) if it satisfies

forall a,b:A. (A,a) = (A,b).

My two classes of examples were types with decidable equality and path spaces. I then chose to use natural numbers for the main example (and thus emphasized the first class). However, I think that what you / Jason outline is (more or less)

1. the second class, namely the path spaces "class of examples"

2. the construction *without* the step where I take the truncation

Concerning 2: I could have skipped that step with the truncation and just said:

The identity function on any inhabited transitive types seems to factor through a contractible type.

(proved by exactly the argument of my blog post minus the part where I use the truncation recursor). I guess it is a matter of taste whether you like that version better than "the identity seems to factor through ||X||".

Concerning 1: Note that path spaces are transitive even *without* univalence:

Just do two times induction on the claim

forall a,b,c:X, p:a=b, q:a=c, (a=b,p) = (a=c,q)

to prove it; and then, take the corresponding special case to get

(a=b,p) = (a=b,q).

Or, for any pointed type X and n>0, we have

forall p,q. (Omega^n X , p) = (Omega^n X , q);

that is, every loop space is transitive. The most immediate argument is to use that "composition with an equality is an equivalence", which requires univalence, but we can do it without univalence.

On the other hand, I can see that you have simplified the construction a bit for the case of path spaces (because you can take coconuts in the type instead of coconuts in the type of pointed types).

About the term "paradox", I agree with Mike, because the first sentence about that on Wikipedia is:

"A**paradox** is a statement that apparently contradicts
itself and yet might be true."

Best,

Nicolai

forall a,b:A. (A,a) = (A,b).

My two classes of examples were types with decidable equality and path spaces. I then chose to use natural numbers for the main example (and thus emphasized the first class). However, I think that what you / Jason outline is (more or less)

1. the second class, namely the path spaces "class of examples"

2. the construction *without* the step where I take the truncation

Concerning 2: I could have skipped that step with the truncation and just said:

The identity function on any inhabited transitive types seems to factor through a contractible type.

(proved by exactly the argument of my blog post minus the part where I use the truncation recursor). I guess it is a matter of taste whether you like that version better than "the identity seems to factor through ||X||".

Concerning 1: Note that path spaces are transitive even *without* univalence:

Just do two times induction on the claim

forall a,b,c:X, p:a=b, q:a=c, (a=b,p) = (a=c,q)

to prove it; and then, take the corresponding special case to get

(a=b,p) = (a=b,q).

Or, for any pointed type X and n>0, we have

forall p,q. (Omega^n X , p) = (Omega^n X , q);

that is, every loop space is transitive. The most immediate argument is to use that "composition with an equality is an equivalence", which requires univalence, but we can do it without univalence.

On the other hand, I can see that you have simplified the construction a bit for the case of path spaces (because you can take coconuts in the type instead of coconuts in the type of pointed types).

About the term "paradox", I agree with Mike, because the first sentence about that on Wikipedia is:

"A

Best,

Nicolai

Mar 3, 2014, 8:00:51 PM3/3/14