Andrej Bauer

When does 1/3 happen? Or do we keep getting dyadics? I like a canonical choice of numbers.

But we do not know ahead of time how many theorems will appear between 4.2.10 and 4.2.11. So we really do need to mark theorems so that we can tell...

[Farey sequence](http://en.wikipedia.org/wiki/Farey_sequence) seems better. So in your scheme the theorems would be tagged with a "generation"?

Yes, we were talking past each other. I suppose people might find it cute to insert 4.2.10⅛ because it was "just a corollary of 4.2.10".

Also, what will you do if you want to insert something between 4.6.10 and 4.6.10.1?

At that point it's just easier to understand 4.6.10½ and 4.6.10⅔. And also, this is way cool.

I have my doubts about librarians believing in fractions.

Sorry for the delay. Using Agda 2.6.2 on MacOS, I can confirm that the problem is caused by case-insensitive file names. When I make sure that the file name matches,...

Right. In fact, already the truncation of the unit type does not work. The coequalizer of the two projections `unit × unit → unit` is the circle, not the truncation...

I can answer that once I understand what `H_con P` is :-)