Online resource for type theory?

[Hurkyl]

New theorem, but I think you already anticipated this one.


Suppose f is a bijection between V and V^V.
Then, every function V--->V has a fixed point.


Proof is roughly the same as the previous one I gave:

Let j by a function from V to V.

Define g(x) = f(x)(x)
Let s = f^-1(j o g)

Then, g(s) = f(s)(s) = (j o g)(s) = j(g(s))

Thus, g(s) is a fixed point of j.

 

[phoenixthoth]

Just a shot in the dark, but does this property characterize the V such that V is in bijection with V^V?

In other words, if every function from V to V has a fixed point, then is V in bijection with V^V?

(This links up with my definition of a awareness, but let's discuss that there and not here.)

I will work on this, too.

 

[Hurkyl]

Note that we have a binary composition on V, given by:

VxV ---> (V^V)xV ---> V

Where the first arrow applies the isomorphism to the first argument, and the second arrow is the evaluation morphism.

In a more set theoretic presentation, for a in V, let \bar{a} be the corresponding element in V^V. Then, a \cdot b := \bar{a}(b)

Clearly, in general, this operation appears to be noncommutative and nonassociative. Such a thing is called a "magma"

http://en.wikipedia.org/wiki/Magma_(algebra)

Maybe something in there is useful.


Clearly, elements of a magma M act on that magma by left multiplication, and in this way we recover part of M^M... but not necessarily all of it, I suppose.


Actually, we have what might be a different binary operation. If V is reflexive, then we have VxV <= V. (I've changed notation -- I hate using < when the objects can be isomorphic) By definition, there's a monic VxV --> V, so this can be taken as a binary operation.

 

[Hurkyl]

It strikes me that I have not proven it impossible for V^V <= V in a topos either. I'm working on seeing if it can be true for the subobjects of 1 (i.e. the logic values).

Also, technically I have not proven it impossible for PV < V in a topos... there's certainly a monic V --> PV, but I don't know if the existence of a monic PV --> V implies V and PV are isomorphic.