Andrej Bauer

A concrete one might be vectors of size n, but that requires induction on n. If we can assume the natural numbers, then an obvious one is `Fin n =...

@vladimirias, what would you suggest as an acceptable introductory example of a dependent type involving a universe?

You're going to get all sorts of nasty line (non)breaks, but if you really would like to try, setting `\OPTfontsize` to `12pt` will do it. For `14pt` we'd need to...

In the meanwhile we prepared `hott-ebook.pdf` with small margins. Please use that until someone figures out how to typeset math for ebooks.

I will buy you a beer if you can do this.

Would it make sense to have a separate branch for this? How much will we have to "pollute" the source to get epub working?

For that sort of thing we probably don't care whether it really is a math environment. It just has to look kind of the same.

I am inclined to start this off as a fork first, and then pull it in when we can be sure it's working. I imagine you already have a fork....

This loks very promising! On my ipad in iboks there seem to be missing math fonts.

It is using German gothic letters instead of mathsf, weird. I am still amazed at how quickly you got this far.