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.
Creative Commons Attribution Share Alike 4.0 International
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 pointed type, which agrees with the type of banded types for central types.
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 pointed type, which agrees with the type of banded types for central types.