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
My current favourite universe of finite sets extends uninformative Boolean truth
So : 2 -> Set
with actual bits
2
and then closes under dependent pairing.
These are wonky binary trees with leaves that are either bits or witnesses to decidable properties. Given that equality for values in these types is decidable, we definitely get a - operator, by a "but not you" construction. (There are other ways to get - but this one makes the weakening map a mere projection.)
Functions from these types may readily be tabulated: a function from 2 is a pair; a function from a pair is a curried function. In particular, this universe already admits a notion of dependent function type, with lambda and application: beta and eta laws are intensionally provable (but defo not judgmental, for fear of a Ripley).
Where am I heading? Containers with finitely many positions, represented as dependent pairs of a shape and a tabulated function from positions. They're traversable. They're also differentiable, but you'll run out of positions before you run out of fingers.
re: fun with finiteness
Job done. The above universe now has the finiteness property I described.
