propositional truncation implies an interval exists

[Daniel R. Grayson]

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

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

https://github.com/DanGrayson/Ktheory/blob/master/src/Interval.v

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

https://github.com/DanGrayson/Foundations2/blob/9f628a42f8af45f6e0021e7e648685e95f0b074a/hlevel1/hProp.v#L90

[Nicolai Kraus]

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.

[Michael Shulman]

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?

[Steve Awodey]

as Dan has observed, we then get functional extensionality.
surprising that propositional truncation implies function extensionality!

[Michael Shulman]

I find both of these proofs very difficult to read. Can anyone write
out the argument in informal language?

[Martin Escardo]

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

[Martin Escardo]

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?

My post showing that ||2|| has the universal property of the interval
(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

[Daniel R. Grayson]

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.

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Steve Awodey]

sorry I missed this.
as Mike said, a good reason to start collecting things on the wiki.

[Vladimir Voevodsky]

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

V.

[Michael Shulman]

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?

[Vladimir Voevodsky]

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

Do you have a Coq formalization and if so could you post a link?

V.

[Vladimir Voevodsky]

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.

[Martin Escardo]

I have an Agda formalization:

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

[Martin Escardo]

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:

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

[Andrej Bauer]

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.

[Martin Escardo]

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

[Martin Escardo]

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?

No. I thought the Agda proof is clear, but obviously I seem to be wrong.
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?

I can have a go on the wiki.

Martin

[Steve Awodey]

http://homotopytypetheory.org/2013/10/28/

[Martin Escardo]

I come from a place with lots of coconuts available, and this is
probably why I got the proof before Dan. Unfair advantage.

Martin

[Vladimir Voevodsky]

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

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

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

V.

[Vladimir Voevodsky]

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.

Thanks! I found it. It is however difficult for me to understand the informal reasoning :) and I do not know Agda. Can this be done in Coq or is it simply a consequence of a bug in Agda?

V.

[Martin Escardo]

Yes, it can be done in Coq. It's not a bug. It's just one of the
applications of coconuts.

Perhaps Nicolai can write a concise informal proof here.

Martin

[Michael Shulman]

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.

[Steve Awodey]

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

which is surely not the way he first found the proof!

: - )

[Jason Gross]

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

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

works for me.

-Jason

[Nicolai Kraus]

Sorry about the unicode in the blog post link, wordpress generates these
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

[Michael Shulman]

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

[Martin Escardo]

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.

There is no paradox *at all*. See below.

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,

Nice rendering of the essence of the "paradox".

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

Where the quotes indicate a lie of sorts.

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

And where C stands for coconut.

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

[Michael Shulman]

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
apply to dependent functions as well as non-dependent ones.

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

I'm not.

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

[Martin Escardo]

You answer far too quickly. In my message I give a more down to earth
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

[Michael Shulman]

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.

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.

[Martin Escardo]

Let's just say, then, to end in an amicable way, that, combining your
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