propositional truncation implies an interval exists

55 views

Daniel R. Grayson

Mar 2, 2014, 7:31:26 PM3/2/14
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:

Nicolai Kraus

Mar 2, 2014, 7:54:19 PM3/2/14
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
> For more options, visit https://groups.google.com/groups/opt_out.

Michael Shulman

Mar 2, 2014, 10:43:52 PM3/2/14
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

Mar 2, 2014, 11:45:26 PM3/2/14
as Dan has observed, we then get functional extensionality.
surprising that propositional truncation implies function extensionality!

Michael Shulman

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?

Martin Escardo

Mar 3, 2014, 2:04:46 AM3/3/14
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

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?

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:

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

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.

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

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

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

Mar 3, 2014, 9:11:12 AM3/3/14
sorry I missed this.
as Mike said, a good reason to start collecting things on the wiki.

Mar 3, 2014, 11:00:53 AM3/3/14
Dan, I thick it is important to emphasize that this construction also shows how to prove functional extensionality from propositional truncation.

V.

Michael Shulman

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?

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

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.

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?

Martin Escardo

Mar 3, 2014, 12:12:11 PM3/3/14
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

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

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

Mar 3, 2014, 12:28:00 PM3/3/14
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

Mar 3, 2014, 12:29:49 PM3/3/14
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

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?

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

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

Martin Escardo

Mar 3, 2014, 12:40:36 PM3/3/14
I come from a place with lots of coconuts available, and this is
probably why I got the proof before Dan. Unfair advantage.

Martin

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

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

V.

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

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

Mar 3, 2014, 1:56:33 PM3/3/14
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

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.

Steve Awodey

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

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

: - )

Jason Gross

Mar 3, 2014, 2:47:57 PM3/3/14
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).

works for me.

-Jason

Nicolai Kraus

Mar 3, 2014, 3:02:11 PM3/3/14
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

Mar 3, 2014, 3:22:15 PM3/3/14
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

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.

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

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

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
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
theory. But it is a paradox in the sense of Skolem's paradox, Zeno's
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

Mar 3, 2014, 5:08:14 PM3/3/14
to Michael Shulman, Nicolai Kraus, HomotopyT...@googlegroups.com
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.

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

It is easy to construct examples like this.

Martin

Michael Shulman

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

Martin Escardo

Mar 3, 2014, 5:30:08 PM3/3/14
to Michael Shulman, Nicolai Kraus, HomotopyT...@googlegroups.com
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

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

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

Mar 3, 2014, 7:50:13 PM3/3/14
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