fun with finiteness
Suppose you have a universe of types (U, El) equipped with an operation
- : (T : U)(t : El t) -> U
such that (T - t) + 1 <=> T
We may define inductively what it is to be a Finite type in U:
T is finite if El T -> 0
T is finite if there is an example t : El T, and for any x : El T, (T - x) is finite
That's to say, you can throw away elements in any order you like, not in the order the finiteness proof likes.
I have that any such type in any such universe is isomorphic to an initial segment of the natural numbers, but I don't like initial segments of the natural nmumbers very much.
I'm now trying to establish finiteness in this sense for a universe of types which are finite but structured, wearing the wrong spectacles, the while.
re: fun with finiteness
Job done. The above universe now has the finiteness property I described.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.