re: fun with finiteness

Job done. The above universe now has the finiteness property I described.

overly intensional piggery-jokery

It's my habit to build ordinary + and * types from

`data Two : Set where `0 `1 : Set`

record _><_ (S : Set)(T : S -> Set) -> Set where ...

S * T = S >< \ _ -> T

S + T = Two >< (S <01> T)

I also have a tendency to cook "types with stuff" in "carrier field" style, e.g.

`record Datoid : Set1 where`

field

Data : Set

eq? : (x y : Data) -> Decide ...

And then I can show nice closure properties like

`Bit : Datoid`

Data Bit = Two

...

_><D_ : (S : Datoid)(T : Data S -> Datoid) -> Datoid

Data (S ><D T) = Data S >< \ s -> Data (T s)

...

_+D_ : Datoid -> Datoid -> Datoid

S +D T = Bit ><D (S <01> T)

but I then don't get (definitionally)

`Data (S +D T) = Data S + Data T`

because no commuting conversion

`\ b -> Data ((S <01> T) b) /= (Data S <01> Data T)`

Something's gotta give... not sure what.

Of course, dense doorstep defaecation is standard mathematical practice.

Every discipline should interrogate its standards of practice from time to time.

There is a school of paper-writing which amounts to doing a very dense logical shit on your reader's doorstep and then running away.

These people want to tell us they understand things. They do not want us to understand things, or if they do, they do so only as an aspiration unenacted.

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.

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.

overly intensional piggery-jokery

Working in plain Agda, I don't have enough extensionality to prove that any two refutations (f g : X -> Zero) are equal. With extensionality, I could assume some x : X, then use either f x or g x to obtain a contradiction.

I'm trying to cook up a useful notion of Datoid (set with decidable equality). If I say "equality is either refutable or provable", I get handed nasty relevant refutations.

The shit hack is to say that a Datoid equips a set with a proof irrelevant notion of apartness which implies refutation of equality, and then makes any two elements apart or equal.

re: lurgy

I don't like being simultaneously sick and on strike. Whatever I've got, the picket doesn't want. I'll stay away in solidarity.

Regretfully, the petition to remove #LGBT content from the #UK curriculum has 197,100 signatures.

The counter petition asking for that content to remain, is rapidly gaining ground. It now has 78,919 signatures!

Pls sign the counter petition if able. British citizens & UK residents have the right to sign. Pls boost otherwise!

Link to official petition to UK Gov & Parliament: Do not remove LGBT content from the Relationships Education curriculum

re: bidirectional typing

As a bonus bonus, whenever you define an "indexed inductive family", try saying in what category each index is an object, such that the family extends to a functor.