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
In 2.16 we introduce connected components and call them subtypes, but subtypes aren't introduced until 2.20. We also speak of two components being the "same", and we write an equation connecting two subtypes, but we don't know that the type of subtypes is a set.
One possible solution: move the material about connected components to 2.20, where it can serve as a good example of subtypes.
In 2.16 we introduce connected components and call them subtypes, but subtypes aren't introduced until 2.20. We also speak of two components being the "same", and we write an equation connecting two subtypes, but we don't know that the type of subtypes is a set.
One possible solution: move the material about connected components to 2.20, where it can serve as a good example of subtypes.