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

[Martin Escardo]

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

[Nicolai Kraus]

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

[Martin Escardo]

On 04/03/14 00:50, Nicolai Kraus wrote:
> 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."

I surrender.

Martin

[Daniel R. Grayson]

The mystery function myst is perhaps clarified by saying that it's a section of

the fibration in the following picture:

        0 -------------------------- 1

        1 -------------------------- 0

     |

     |

     V

        0 -------------------------- 1

in which the fibers over both endpoints are {0,1}.

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

[Dan Doel]

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

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.

I'm curious what type you're giving to F.

 

I fiddled for a bit and didn't come up with anything, so it's tricky to say the least.

[Martin Escardo]

I think it may be infinitely tricky. My paper solution doesn't type
check in Agda, and I didn't manage to fix it either after trying for a
while last night...

[Marc Bezem]

Dear All,

at the seminar we are puzzled by this:

|| bool ||   \simeq   Interval   \simeq   1

since they are all contractible. The first two seem to be `more equivalent' (as HITs?) than the last two.

What exactly is this stronger equivalence?

Also, all these animals are equal under univalence. Are the first two more equal then the others?

Marc

[Daniel R. Grayson]

Indeed, they are all contractible.

The advantage of 'interval' over '1' is that given x x' : X and m:x==x' you can

define a function f : interval -> X so that the equalities f left = x and f right = x'

hold by definition, not just propositionally.

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

[Peter LeFanu Lumsdaine]

(Have just been belatedly catching up on this thread, so it’s possible that someone’s pointed out the following already and I missed it.)

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

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.

 

[…] 

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

In the original “myst” example, isn’t it internal?

Fitting that example into the framework above, the “desired” object is a function F : |Bool| -> Bool such that F( |True| ) = True, F( |False| ) = False.

But given such F, we also know (just by “ap”) that F( |True| ) = F( |False| ); so True = False; contradiction.

–p.

 

[Guillaume Brunerie]

I'm not sure where your intuition comes from, but from the point of view of topology, the first two are very different.

To construct || Bool || you need to do the following :
Start from a discrete space {t, f}.
Add the four paths between those elements.
Add a new path between every two points in the previous space (so you glue some three-dimensional manifold-like thing)
Continue ad infinitum (in the next step you will add some 7-dimensional structure, then some 15-dimensional structure, and so on).

I don't see how this looks like an interval.

There is a way, though, to say that || Bool || is "more like" the interval than 1 : assuming some well-behaved type theory solving the problem of computability of univalence and HITs, one may expect that both || Bool || and the Interval have exactly two closed terms, whereas 1 has only one. Similarly, I guess that in the simplicial model the first two have exactly two objects and 1 has exactly one. Maybe that's what you meant?

Guillaume

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

[Michael Shulman]

In classical homotopy theory, one property shared by ||Bool|| and the
interval, but not by 1, is that of being the codomain of a cofibration
with domain Bool. That's more or less the same sense in which they've
been being compared in type theory in this thread: we can define a map
out of them which has judgmentally different behavior on the two
points.

[Martin Escardo]

Yes. Martin

[Peter LeFanu Lumsdaine]

On Fri, Mar 7, 2014 at 2:25 PM, Michael Shulman <shu...@sandiego.edu> wrote:

In classical homotopy theory, one property shared by ||Bool|| and the
interval, but not by 1, is that of being the codomain of a cofibration
with domain Bool.  That's more or less the same sense in which they've
been being compared in type theory in this thread: we can define a map
out of them which has judgmentally different behavior on the two
points.

Indeed, one can same this property the same way in the type theory.  The maps

Bool -> |Bool|

Bool -> Interval

are both cofibrations in the sense of bring left-orthogonal to “trivial fibrations”, i.e. (projections from total spaces of) families of contractible types; while |Bool| and Interval are each contractible over 1.

In other words, |Bool| and Interval both give (C,TF) factorisations of the map Bool -> 1.  On the other hand, 1 itself doesn't, since the map  Bool -> 1 is not a cofibration.

Of course, these are all external properties, invisible internally.

[Marc Bezem]

To construct || Bool || you need to do the following :
Start from a discrete space {t, f}.
Add the four paths between those elements.
Add a new path between every two points in the previous space (so you glue some three-dimensional manifold-like thing)
Continue ad infinitum (in the next step you will add some 7-dimensional structure, then some 15-dimensional structure, and so on).

I don't see how this looks like an interval.

Maybe, but the thread started with "an interval can be obtained as the propositional truncation of bool".

There is a way, though, to say that || Bool || is "more like" the interval than 1 : assuming some well-behaved type theory solving the problem of computability of univalence and HITs, one may expect that both || Bool || and the Interval have exactly two closed terms, whereas 1 has only one. Similarly, I guess that in the simplicial model the first two have exactly two objects and 1 has exactly one. Maybe that's what you meant?

That is, at least intuitively, the point. Do we know confluence and termination for TT + (some relevant) HITs ?

Marc

[Michael Shulman]

On Fri, Mar 7, 2014 at 12:02 PM, Marc Bezem <marc....@gmail.com> wrote:
>> There is a way, though, to say that || Bool || is "more like" the interval
>> than 1 : assuming some well-behaved type theory solving the problem of
>> computability of univalence and HITs, one may expect that both || Bool ||
>> and the Interval have exactly two closed terms, whereas 1 has only one.
>> Similarly, I guess that in the simplicial model the first two have exactly
>> two objects and 1 has exactly one. Maybe that's what you meant?
>
> That is, at least intuitively, the point.

I don't think that's really the point. I think the point is what
Peter and I said: ||Bool|| and the interval admit a cofibration from
Bool. In particular, that's what is needed for the proof of function
extensionality.

Mike

[Marc Bezem]

Thanks. I have to think (and study) more to understand the point of the cofibrations. Still looking for some syntactic explanation, can the following observation (also external) be relevant here:

For ||Bool|| and the Interval we have equivalences such that g(f(x))=x holds _definitionally_. Not so for 1.

[Michael Shulman]

On Fri, Mar 7, 2014 at 1:08 PM, Marc Bezem <marc....@gmail.com> wrote:
> Thanks. I have to think (and study) more to understand the point of the
> cofibrations. Still looking for some syntactic explanation

I think the second explanation I gave is syntactic: for ||Bool|| and
the interval, we can define a map out of them which has judgmentally

different behavior on the two points.

> For ||Bool|| and the Interval we have equivalences such that g(f(x))=x holds
> _definitionally_.

That's not true for all x, only for the two points x=0 and x=1.

[Vladimir Voevodsky]

Dan, does you proof require eta-reduction? V.

[Daniel R. Grayson]

Yes.  If you don't have eta reduction, just change the final definition to this

and it will work:

Definition funextsec2 X (Y:X->Type) (f g:forall x,Y x) :

           (forall x, f x==g x) -> (fun x => f x) == (fun x => g x).

, as I've just verified with coq 8.3.