SymmetryBook
SymmetryBook copied to clipboard
UniMath
This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
There must be a better word than "merely" we can use. In ordinary English, "merely" means "only", and that doesn't work with our use of it. Consider : X and...
"merely"
After our discussion of \eq and \eqto, I think this make no sense at all: How can we have a English adjectival phrase encoded by a type that is not...
In this text: the predicate `isnType` is undefined. Also, it would look better if the `n` occurred as a subscript, instead of inline.
I struggled with this question when modifying intro.tex, with the object being the square and the ambient type (not exactly the type of the square) the plane or the oriented...
$\mathrm{ad}$ is used here: https://github.com/UniMath/SymmetryBook/blob/33011ebf1fc139cc6f17ab45b5f8db7ae4b4a00a/group.tex#L2356 But is not defined. I guess it means conjugation?
We could include a further discussion of deloopings of abelian groups (and homomorphisms) between them, after David Wärn (https://arxiv.org/abs/2301.03685) and bandings (https://arxiv.org/abs/2301.02636). In particular, the type of torsors of a...
* Exercise 2.22.14 omits `p` in the final equation and has tuple brackets in the wrong order. * Lemma 2.23.6 has `n` in two different meanings which is somewhat confusing,...
