Tilo Wiklund (tilowiklund)

Tilo Wiklund Evan Prodromou

voted for "other"

Tilo Wiklund

The Type classes for maths paper suggests there isn't any point in making inherited structures arguments to a typeclass, but no motivation.

Tilo Wiklund

Or is this just what's known as an Ensamble...

Tilo Wiklund

I wonder why the notion of setoid, at least in Coq, doesn't include a "subset" predicate, allowing substructures as well as quotients.

Tilo Wiklund

I guess there's a point to the "canonical names" in math-classes even when not used in specifying theorems. When printing specified ones.

Tilo Wiklund

I still find it pretty hilarious when books leave famous theorems "as en exercise to the reader".

Tilo Wiklund

It's interesting how algebraic theories map so nicely into type theory while topological notions are so much harder (for obvious reasons).

Tilo Wiklund

Basic lattice theory reminds me of basic number theory, mostly a bunch of algebraic juggling...

Tilo Wiklund

It seems most of the Coq standard library related to orders is done in a bundled fashion, guess I'll have to do at least these parts myself.

Tilo Wiklund

Generalised rewriting is pretty neat, too bad math-classes has a bunch of issues...

Tilo Wiklund

Time to understand generalised rewriting in Coq.

Tilo Wiklund

Been spending the last 24h RAIDing 10 2TB discs...

Tilo Wiklund

Maybe I should get started on formalising containers instead...

Tilo Wiklund

Seems this was what math-classes was already doing. A similar, though more light weight, was given in a paper by Sozeau and Oury.

Tilo Wiklund

I wonder if categories can be represented nicely, in Coq, by its "Hom Functor" over its type of objects.