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.
Also in that file. Nicolai then used this
to define his mysterious pseudo-inverse of |-|:X->||X||.
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.)
--
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.
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.
--
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.
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).
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.
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.
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?