search

UniMath / SymmetryBook

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
371 stars 22 forks source link

2.12.8-10 #165

Closed marcbezem closed 10 months ago

marcbezem commented 1 year ago

2.12.8. Line 11 "In fact we will assume ... definitionally." is a bit weird, in particular combined with 3 lines down "not definitionally".

2.12.9. I change the wording a bit since I think -(-n) \jdeq n for all n in N^- can be misunderstood.

2.12.10. I added this exercise to implement a free-wheeling \equiv

marcbezem commented 1 year ago

See 5e7f1c5